:: Groups
:: by Wojciech A. Trybulec
::
:: Received July 3, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1: now :: thesis: ( ( for h, g, f being Element of multMagma(# REAL,addreal #) holds (h * g) * f = h * (g * f) ) & ex e being Element of multMagma(# REAL,addreal #) st
for h being Element of multMagma(# REAL,addreal #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) ) )
set G = multMagma(# REAL,addreal #);
thus for h, g, f being Element of multMagma(# REAL,addreal #) holds (h * g) * f = h * (g * f) :: thesis: ex e being Element of multMagma(# REAL,addreal #) st
for h being Element of multMagma(# REAL,addreal #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )
proof
let h, g, f be Element of multMagma(# REAL,addreal #); :: thesis: (h * g) * f = h * (g * f)
reconsider A = h, B = g, C = f as Real ;
A1: g * f = B + C by BINOP_2:def 9;
h * g = A + B by BINOP_2:def 9;
hence (h * g) * f = (A + B) + C by BINOP_2:def 9
.= A + (B + C)
.= h * (g * f) by A1, BINOP_2:def 9 ;
:: thesis: verum
end;
reconsider e = 0 as Element of multMagma(# REAL,addreal #) ;
take e = e; :: thesis: for h being Element of multMagma(# REAL,addreal #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )

let h be Element of multMagma(# REAL,addreal #); :: thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )

reconsider A = h as Real ;
thus h * e = A + 0 by BINOP_2:def 9
.= h ; :: thesis: ( e * h = h & ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e ) )

thus e * h = 0 + A by BINOP_2:def 9
.= h ; :: thesis: ex g being Element of multMagma(# REAL,addreal #) st
( h * g = e & g * h = e )

reconsider g = - A as Element of multMagma(# REAL,addreal #) ;
take g = g; :: thesis: ( h * g = e & g * h = e )
thus h * g = A + (- A) by BINOP_2:def 9
.= e ; :: thesis: g * h = e
thus g * h = (- A) + A by BINOP_2:def 9
.= e ; :: thesis: verum
end;

definition
let IT be multMagma ;
attr IT is unital means :Def1: :: GROUP_1:def 1
ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h );
attr IT is Group-like means :Def2: :: GROUP_1:def 2
ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h & ex g being Element of IT st
( h * g = e & g * h = e ) );
attr IT is associative means :Def3: :: GROUP_1:def 3
for x, y, z being Element of IT holds (x * y) * z = x * (y * z);
end;

:: deftheorem Def1 defines unital GROUP_1:def 1 :
for IT being multMagma holds
( IT is unital iff ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h ) );

:: deftheorem Def2 defines Group-like GROUP_1:def 2 :
for IT being multMagma holds
( IT is Group-like iff ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h & ex g being Element of IT st
( h * g = e & g * h = e ) ) );

:: deftheorem Def3 defines associative GROUP_1:def 3 :
for IT being multMagma holds
( IT is associative iff for x, y, z being Element of IT holds (x * y) * z = x * (y * z) );

registration
cluster Group-like -> unital for multMagma ;
coherence
for b1 being multMagma st b1 is Group-like holds
b1 is unital
proof end;
end;

registration
cluster non empty strict Group-like associative for multMagma ;
existence
ex b1 being multMagma st
( b1 is strict & b1 is Group-like & b1 is associative & not b1 is empty )
proof end;
end;

definition
mode Group is non empty Group-like associative multMagma ;
end;

theorem :: GROUP_1:1
for S being non empty multMagma st ( for r, s, t being Element of S holds (r * s) * t = r * (s * t) ) & ex t being Element of S st
for s1 being Element of S holds
( s1 * t = s1 & t * s1 = s1 & ex s2 being Element of S st
( s1 * s2 = t & s2 * s1 = t ) ) holds
S is Group by Def2, Def3;

theorem :: GROUP_1:2
for S being non empty multMagma st ( for r, s, t being Element of S holds (r * s) * t = r * (s * t) ) & ( for r, s being Element of S holds
( ex t being Element of S st r * t = s & ex t being Element of S st t * r = s ) ) holds
( S is associative & S is Group-like )
proof end;

theorem Th3: :: GROUP_1:3
( multMagma(# REAL,addreal #) is associative & multMagma(# REAL,addreal #) is Group-like )
proof end;

definition
let G be multMagma ;
assume A1: G is unital ;
func 1_ G -> Element of G means :Def4: :: GROUP_1:def 4
for h being Element of G holds
( h * it = h & it * h = h );
existence
ex b1 being Element of G st
for h being Element of G holds
( h * b1 = h & b1 * h = h )
by A1, Def1;
uniqueness
for b1, b2 being Element of G st ( for h being Element of G holds
( h * b1 = h & b1 * h = h ) ) & ( for h being Element of G holds
( h * b2 = h & b2 * h = h ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines 1_ GROUP_1:def 4 :
for G being multMagma st G is unital holds
for b2 being Element of G holds
( b2 = 1_ G iff for h being Element of G holds
( h * b2 = h & b2 * h = h ) );

theorem :: GROUP_1:4
for G being non empty Group-like multMagma
for e being Element of G st ( for h being Element of G holds
( h * e = h & e * h = h ) ) holds
e = 1_ G by Def4;

definition
let G be Group;
let h be Element of G;
func h " -> Element of G means :Def5: :: GROUP_1:def 5
( h * it = 1_ G & it * h = 1_ G );
existence
ex b1 being Element of G st
( h * b1 = 1_ G & b1 * h = 1_ G )
proof end;
uniqueness
for b1, b2 being Element of G st h * b1 = 1_ G & b1 * h = 1_ G & h * b2 = 1_ G & b2 * h = 1_ G holds
b1 = b2
proof end;
involutiveness
for b1, b2 being Element of G st b2 * b1 = 1_ G & b1 * b2 = 1_ G holds
( b1 * b2 = 1_ G & b2 * b1 = 1_ G )
;
end;

:: deftheorem Def5 defines " GROUP_1:def 5 :
for G being Group
for h, b3 being Element of G holds
( b3 = h " iff ( h * b3 = 1_ G & b3 * h = 1_ G ) );

theorem :: GROUP_1:5
for G being Group
for h, g being Element of G st h * g = 1_ G & g * h = 1_ G holds
g = h " by Def5;

theorem Th6: :: GROUP_1:6
for G being Group
for h, g, f being Element of G st ( h * g = h * f or g * h = f * h ) holds
g = f
proof end;

theorem :: GROUP_1:7
for G being Group
for h, g being Element of G st ( h * g = h or g * h = h ) holds
g = 1_ G
proof end;

theorem Th8: :: GROUP_1:8
for G being Group holds (1_ G) " = 1_ G
proof end;

theorem :: GROUP_1:9
for G being Group
for h, g being Element of G st h " = g " holds
h = g
proof end;

theorem :: GROUP_1:10
for G being Group
for h being Element of G st h " = 1_ G holds
h = 1_ G
proof end;

theorem :: GROUP_1:11
canceled;

theorem Th12: :: GROUP_1:12
for G being Group
for h, g being Element of G st h * g = 1_ G holds
( h = g " & g = h " )
proof end;

theorem Th13: :: GROUP_1:13
for G being Group
for h, f, g being Element of G holds
( h * f = g iff f = (h ") * g )
proof end;

theorem Th14: :: GROUP_1:14
for G being Group
for f, h, g being Element of G holds
( f * h = g iff f = g * (h ") )
proof end;

theorem :: GROUP_1:15
for G being Group
for g, h being Element of G ex f being Element of G st g * f = h
proof end;

theorem :: GROUP_1:16
for G being Group
for g, h being Element of G ex f being Element of G st f * g = h
proof end;

theorem Th17: :: GROUP_1:17
for G being Group
for h, g being Element of G holds (h * g) " = (g ") * (h ")
proof end;

theorem Th18: :: GROUP_1:18
for G being Group
for g, h being Element of G holds
( g * h = h * g iff (g * h) " = (g ") * (h ") )
proof end;

theorem Th19: :: GROUP_1:19
for G being Group
for g, h being Element of G holds
( g * h = h * g iff (g ") * (h ") = (h ") * (g ") )
proof end;

theorem Th20: :: GROUP_1:20
for G being Group
for g, h being Element of G holds
( g * h = h * g iff g * (h ") = (h ") * g )
proof end;

definition
let G be Group;
func inverse_op G -> UnOp of G means :Def6: :: GROUP_1:def 6
for h being Element of G holds it . h = h " ;
existence
ex b1 being UnOp of G st
for h being Element of G holds b1 . h = h "
proof end;
uniqueness
for b1, b2 being UnOp of G st ( for h being Element of G holds b1 . h = h " ) & ( for h being Element of G holds b2 . h = h " ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines inverse_op GROUP_1:def 6 :
for G being Group
for b2 being UnOp of G holds
( b2 = inverse_op G iff for h being Element of G holds b2 . h = h " );

registration
let G be non empty associative multMagma ;
cluster the multF of G -> associative ;
coherence
the multF of G is associative
proof end;
end;

theorem Th21: :: GROUP_1:21
for G being non empty unital multMagma holds 1_ G is_a_unity_wrt the multF of G
proof end;

theorem Th22: :: GROUP_1:22
for G being non empty unital multMagma holds the_unity_wrt the multF of G = 1_ G
proof end;

registration
let G be non empty unital multMagma ;
cluster the multF of G -> having_a_unity ;
coherence
the multF of G is having_a_unity
proof end;
end;

theorem Th23: :: GROUP_1:23
for G being Group holds inverse_op G is_an_inverseOp_wrt the multF of G
proof end;

registration
let G be Group;
cluster the multF of G -> having_an_inverseOp ;
coherence
the multF of G is having_an_inverseOp
proof end;
end;

theorem :: GROUP_1:24
for G being Group holds the_inverseOp_wrt the multF of G = inverse_op G
proof end;

definition
let G be non empty multMagma ;
func power G -> Function of [: the carrier of G,NAT:], the carrier of G means :Def7: :: GROUP_1:def 7
for h being Element of G holds
( it . (h,0) = 1_ G & ( for n being Element of NAT holds it . (h,(n + 1)) = (it . (h,n)) * h ) );
existence
ex b1 being Function of [: the carrier of G,NAT:], the carrier of G st
for h being Element of G holds
( b1 . (h,0) = 1_ G & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) )
proof end;
uniqueness
for b1, b2 being Function of [: the carrier of G,NAT:], the carrier of G st ( for h being Element of G holds
( b1 . (h,0) = 1_ G & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) ) & ( for h being Element of G holds
( b2 . (h,0) = 1_ G & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines power GROUP_1:def 7 :
for G being non empty multMagma
for b2 being Function of [: the carrier of G,NAT:], the carrier of G holds
( b2 = power G iff for h being Element of G holds
( b2 . (h,0) = 1_ G & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) );

definition
let G be Group;
let i be Integer;
let h be Element of G;
func h |^ i -> Element of G equals :Def8: :: GROUP_1:def 8
(power G) . (h,(abs i)) if 0 <= i
otherwise ((power G) . (h,(abs i))) " ;
correctness
coherence
( ( 0 <= i implies (power G) . (h,(abs i)) is Element of G ) & ( not 0 <= i implies ((power G) . (h,(abs i))) " is Element of G ) )
;
consistency
for b1 being Element of G holds verum
;
;
end;

:: deftheorem Def8 defines |^ GROUP_1:def 8 :
for G being Group
for i being Integer
for h being Element of G holds
( ( 0 <= i implies h |^ i = (power G) . (h,(abs i)) ) & ( not 0 <= i implies h |^ i = ((power G) . (h,(abs i))) " ) );

definition
let G be Group;
let n be Nat;
let h be Element of G;
redefine func h |^ n equals :: GROUP_1:def 9
(power G) . (h,n);
compatibility
for b1 being Element of G holds
( b1 = h |^ n iff b1 = (power G) . (h,n) )
proof end;
end;

:: deftheorem defines |^ GROUP_1:def 9 :
for G being Group
for n being Nat
for h being Element of G holds h |^ n = (power G) . (h,n);

Lm2: for n being Nat
for G being Group
for h being Element of G holds h |^ (n + 1) = (h |^ n) * h

proof end;

Lm3: for G being Group
for h being Element of G holds h |^ 0 = 1_ G

by Def7;

Lm4: for n being Nat
for G being Group holds (1_ G) |^ n = 1_ G

proof end;

theorem :: GROUP_1:25
for G being Group
for h being Element of G holds h |^ 0 = 1_ G by Def7;

theorem Th26: :: GROUP_1:26
for G being Group
for h being Element of G holds h |^ 1 = h
proof end;

theorem Th27: :: GROUP_1:27
for G being Group
for h being Element of G holds h |^ 2 = h * h
proof end;

theorem :: GROUP_1:28
for G being Group
for h being Element of G holds h |^ 3 = (h * h) * h
proof end;

theorem :: GROUP_1:29
for G being Group
for h being Element of G holds
( h |^ 2 = 1_ G iff h " = h )
proof end;

Lm5: for n, m being Nat
for G being Group
for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)

proof end;

Lm6: for n being Nat
for G being Group
for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )

proof end;

Lm7: for n, m being Nat
for G being Group
for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m

proof end;

Lm8: for n being Nat
for G being Group
for h being Element of G holds (h ") |^ n = (h |^ n) "

proof end;

Lm9: for n being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ n) = (h |^ n) * g

proof end;

Lm10: for n, m being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)

proof end;

Lm11: for n being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ n = (g |^ n) * (h |^ n)

proof end;

theorem Th30: :: GROUP_1:30
for i being Integer
for G being Group
for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "
proof end;

theorem :: GROUP_1:31
for i being Integer
for G being Group holds (1_ G) |^ i = 1_ G
proof end;

theorem Th32: :: GROUP_1:32
for G being Group
for h being Element of G holds h |^ (- 1) = h "
proof end;

Lm12: for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) "

proof end;

Lm13: for j being Integer holds
( j >= 1 or j = 0 or j < 0 )

proof end;

Lm14: for j being Integer
for G being Group
for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))

proof end;

Lm15: for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )

proof end;

Lm16: for j being Integer
for G being Group
for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)

proof end;

theorem Th33: :: GROUP_1:33
for i, j being Integer
for G being Group
for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)
proof end;

theorem :: GROUP_1:34
for i being Integer
for G being Group
for h being Element of G holds
( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
proof end;

Lm17: for i being Integer
for G being Group
for h being Element of G holds (h ") |^ i = (h |^ i) "

proof end;

theorem :: GROUP_1:35
for i, j being Integer
for G being Group
for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j
proof end;

theorem :: GROUP_1:36
for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) " by Lm12;

theorem :: GROUP_1:37
for i being Integer
for G being Group
for h being Element of G holds (h ") |^ i = (h |^ i) " by Lm17;

theorem Th38: :: GROUP_1:38
for i being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ i = (g |^ i) * (h |^ i)
proof end;

theorem Th39: :: GROUP_1:39
for i, j being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
proof end;

theorem :: GROUP_1:40
for i being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ i) = (h |^ i) * g
proof end;

definition
let G be Group;
let h be Element of G;
attr h is being_of_order_0 means :Def10: :: GROUP_1:def 10
for n being Nat st h |^ n = 1_ G holds
n = 0 ;
end;

:: deftheorem Def10 defines being_of_order_0 GROUP_1:def 10 :
for G being Group
for h being Element of G holds
( h is being_of_order_0 iff for n being Nat st h |^ n = 1_ G holds
n = 0 );

registration
let G be Group;
cluster 1_ G -> non being_of_order_0 ;
coherence
not 1_ G is being_of_order_0
proof end;
end;

definition
let G be Group;
let h be Element of G;
func ord h -> Element of NAT means :Def11: :: GROUP_1:def 11
it = 0 if h is being_of_order_0
otherwise ( h |^ it = 1_ G & it <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
it <= m ) );
existence
( ( h is being_of_order_0 implies ex b1 being Element of NAT st b1 = 0 ) & ( not h is being_of_order_0 implies ex b1 being Element of NAT st
( h |^ b1 = 1_ G & b1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b1 <= m ) ) ) )
proof end;
uniqueness
for b1, b2 being Element of NAT holds
( ( h is being_of_order_0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not h is being_of_order_0 & h |^ b1 = 1_ G & b1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b1 <= m ) & h |^ b2 = 1_ G & b2 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b2 <= m ) implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Element of NAT holds verum
;
;
end;

:: deftheorem Def11 defines ord GROUP_1:def 11 :
for G being Group
for h being Element of G
for b3 being Element of NAT holds
( ( h is being_of_order_0 implies ( b3 = ord h iff b3 = 0 ) ) & ( not h is being_of_order_0 implies ( b3 = ord h iff ( h |^ b3 = 1_ G & b3 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b3 <= m ) ) ) ) );

theorem Th41: :: GROUP_1:41
for G being Group
for h being Element of G holds h |^ (ord h) = 1_ G
proof end;

theorem :: GROUP_1:42
for G being Group holds ord (1_ G) = 1
proof end;

theorem :: GROUP_1:43
for G being Group
for h being Element of G st ord h = 1 holds
h = 1_ G
proof end;

theorem :: GROUP_1:44
for n being Nat
for G being Group
for h being Element of G st h |^ n = 1_ G holds
ord h divides n
proof end;

definition
let G be finite 1-sorted ;
:: original: card
redefine func card G -> Element of NAT ;
coherence
card G is Element of NAT
proof end;
end;

theorem :: GROUP_1:45
for G being non empty finite 1-sorted holds card G >= 1
proof end;

definition
let IT be multMagma ;
attr IT is commutative means :Def12: :: GROUP_1:def 12
for x, y being Element of IT holds x * y = y * x;
end;

:: deftheorem Def12 defines commutative GROUP_1:def 12 :
for IT being multMagma holds
( IT is commutative iff for x, y being Element of IT holds x * y = y * x );

registration
cluster non empty strict unital Group-like associative commutative for multMagma ;
existence
ex b1 being Group st
( b1 is strict & b1 is commutative )
proof end;
end;

definition
let FS be non empty commutative multMagma ;
let x, y be Element of FS;
:: original: *
redefine func x * y -> Element of the carrier of FS;
commutativity
for x, y being Element of FS holds x * y = y * x
by Def12;
end;

theorem :: GROUP_1:46
multMagma(# REAL,addreal #) is commutative Group
proof end;

theorem :: GROUP_1:47
for A being commutative Group
for a, b being Element of A holds (a * b) " = (a ") * (b ") by Th17;

theorem :: GROUP_1:48
for i being Integer
for A being commutative Group
for a, b being Element of A holds (a * b) |^ i = (a |^ i) * (b |^ i) by Th38;

theorem :: GROUP_1:49
for A being commutative Group holds
( addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is Abelian & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is add-associative & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_complementable )
proof end;

begin

:: from COMPTRIG, 2006.08.12, A.T.
theorem Th50: :: GROUP_1:50
for L being non empty unital multMagma
for x being Element of L holds (power L) . (x,1) = x
proof end;

theorem :: GROUP_1:51
for L being non empty unital multMagma
for x being Element of L holds (power L) . (x,2) = x * x
proof end;

theorem :: GROUP_1:52
for L being non empty unital associative commutative multMagma
for x, y being Element of L
for n being Element of NAT holds (power L) . ((x * y),n) = ((power L) . (x,n)) * ((power L) . (y,n))
proof end;

:: Moved from ENDALG, 17.01_2006, AK
definition
let G, H be multMagma ;
let IT be Function of G,H;
attr IT is unity-preserving means :: GROUP_1:def 13
IT . (1_ G) = 1_ H;
end;

:: deftheorem defines unity-preserving GROUP_1:def 13 :
for G, H being multMagma
for IT being Function of G,H holds
( IT is unity-preserving iff IT . (1_ G) = 1_ H );