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

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 #) by XREAL_0:def 1;
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 #) by XREAL_0:def 1;
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 :: 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 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 b₁ being multMagma st b₁ is Group-like holds
b₁ is unital ;

end;

registration

cluster non empty strict Group-like associative for multMagma ;

existence
ex b₁ being multMagma st
( b₁ is strict & b₁ is Group-like & b₁ is associative & not b₁ 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 b₁ being Element of G st
for h being Element of G holds
( h * b₁ = h & b₁ * h = h ) by A1;
uniqueness
for b₁, b₂ being Element of G st ( for h being Element of G holds
( h * b₁ = h & b₁ * h = h ) ) & ( for h being Element of G holds
( h * b₂ = h & b₂ * h = h ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines 1_ GROUP_1:def 4 :
for G being multMagma st G is unital holds
for b₂ being Element of G holds
( b₂ = 1_ G iff for h being Element of G holds
( h * b₂ = h & b₂ * 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 b₁ being Element of G st
( h * b₁ = 1_ G & b₁ * h = 1_ G )

proof end;

uniqueness
for b₁, b₂ being Element of G st h * b₁ = 1_ G & b₁ * h = 1_ G & h * b₂ = 1_ G & b₂ * h = 1_ G holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Element of G st b₂ * b₁ = 1_ G & b₁ * b₂ = 1_ G holds
( b₁ * b₂ = 1_ G & b₂ * b₁ = 1_ G ) ;

end;

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

theorem :: GROUP_1:5

for G being Group
for g, h 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 f, g, h 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 g, h 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 g, h 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;

::$CT

theorem Th11: :: GROUP_1:12

for G being Group
for g, h being Element of G st h * g = 1_ G holds
( h = g " & g = h " )

proof end;

theorem Th12: :: GROUP_1:13

for G being Group
for f, g, h being Element of G holds
( h * f = g iff f = (h ") * g )

proof end;

theorem Th13: :: GROUP_1:14

for G being Group
for f, g, h 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 Th16: :: GROUP_1:17

for G being Group
for g, h being Element of G holds (h * g) " = (g ") * (h ")

proof end;

theorem Th17: :: 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 Th18: :: 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 Th19: :: 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 b₁ being UnOp of G st
for h being Element of G holds b₁ . h = h "

proof end;

uniqueness
for b₁, b₂ being UnOp of G st ( for h being Element of G holds b₁ . h = h " ) & ( for h being Element of G holds b₂ . h = h " ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines inverse_op GROUP_1:def 6 :
for G being Group
for b₂ being UnOp of G holds
( b₂ = inverse_op G iff for h being Element of G holds b₂ . 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 Th20: :: GROUP_1:21

for G being non empty unital multMagma holds 1_ G is_a_unity_wrt the multF of G

proof end;

theorem Th21: :: 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 Th22: :: 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 Nat holds it . (h,(n + 1)) = (it . (h,n)) * h ) );

existence
ex b₁ being Function of [: the carrier of G,NAT:], the carrier of G st
for h being Element of G holds
( b₁ . (h,0) = 1_ G & ( for n being Nat holds b₁ . (h,(n + 1)) = (b₁ . (h,n)) * h ) )

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of G,NAT:], the carrier of G st ( for h being Element of G holds
( b₁ . (h,0) = 1_ G & ( for n being Nat holds b₁ . (h,(n + 1)) = (b₁ . (h,n)) * h ) ) ) & ( for h being Element of G holds
( b₂ . (h,0) = 1_ G & ( for n being Nat holds b₂ . (h,(n + 1)) = (b₂ . (h,n)) * h ) ) ) holds
b₁ = b₂

proof end;

end;

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

definition

let G be Group;
let h be Element of G;
let i be Integer;

func h |^ i -> Element of G equals :Def8: :: GROUP_1:def 8
(power G) . (h,|.i.|) if 0 <= i
otherwise ((power G) . (h,|.i.|)) " ;

correctness
coherence
( ( 0 <= i implies (power G) . (h,|.i.|) is Element of G ) & ( not 0 <= i implies ((power G) . (h,|.i.|)) " is Element of G ) );
consistency
for b₁ being Element of G holds verum;
;

end;

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

definition

let G be Group;
let h be Element of G;
let n be natural Number ;

redefine func h |^ n equals :: GROUP_1:def 9
(power G) . (h,n);

compatibility
for b₁ being Element of G holds
( b₁ = h |^ n iff b₁ = (power G) . (h,n) )

proof end;

end;

:: deftheorem defines |^ GROUP_1:def 9 :
for G being Group
for h being Element of G
for n being natural Number 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
by Def7;

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 Th25: :: GROUP_1:26

for G being Group
for h being Element of G holds h |^ 1 = h

proof end;

theorem Th26: :: 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 m, n 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 m, n 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 m, n 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 Th29: :: GROUP_1:30

for i being Integer
for G being Group
for h being Element of G st i <= 0 holds
h |^ i = (h |^ |.i.|) "

proof end;

theorem :: GROUP_1:31

for i being Integer
for G being Group holds (1_ G) |^ i = 1_ G

proof end;

theorem Th31: :: 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 Th32: :: 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 Th37: :: 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 Th38: :: 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 :: GROUP_1:def 10
for n being Nat st h |^ n = 1_ G holds
n = 0 ;

end;

:: deftheorem 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 b₁ being Element of NAT st b₁ = 0 ) & ( not h is being_of_order_0 implies ex b₁ being Element of NAT st
( h |^ b₁ = 1_ G & b₁ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₁ <= m ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT holds
( ( h is being_of_order_0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) & ( not h is being_of_order_0 & h |^ b₁ = 1_ G & b₁ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₁ <= m ) & h |^ b₂ = 1_ G & b₂ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₂ <= m ) implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ 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 b₃ being Element of NAT holds
( ( h is being_of_order_0 implies ( b₃ = ord h iff b₃ = 0 ) ) & ( not h is being_of_order_0 implies ( b₃ = ord h iff ( h |^ b₃ = 1_ G & b₃ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₃ <= m ) ) ) ) );

theorem Th40: :: 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 b₁ being Group st
( b₁ is strict & b₁ 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 Th16;

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 Th37;

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;

:: from COMPTRIG, 2006.08.12, A.T.

theorem Th49: :: 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 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 );