:: GROUP_1 semantic presentation
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 ;
attrIT 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 );
attrIT 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 ) );
attrIT 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
let IT be multMagma ; ::_thesis: ( IT is Group-like implies IT is unital )
assume 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 ) ) ; :: according to GROUP_1:def_2 ::_thesis: IT is unital
hence ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h ) ; :: according to GROUP_1:def_1 ::_thesis: verum
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
( multMagma(# REAL,addreal #) is Group-like & multMagma(# REAL,addreal #) is associative ) by Def2, Def3, Lm1;
hence ex b1 being multMagma st
( b1 is strict & b1 is Group-like & b1 is associative & not b1 is empty ) ; ::_thesis: verum
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
let S be non empty multMagma ; ::_thesis: ( ( 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 ) ) implies ( S is associative & S is Group-like ) )
set r = the Element of S;
assume that
A1: for r, s, t being Element of S holds (r * s) * t = r * (s * t) and
A2: 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 ) ; ::_thesis: ( S is associative & S is Group-like )
consider s1 being Element of S such that
A3: the Element of S * s1 = the Element of S by A2;
thus for r, s, t being Element of S holds (r * s) * t = r * (s * t) by A1; :: according to GROUP_1:def_3 ::_thesis: S is Group-like
take s1 ; :: according to GROUP_1:def_2 ::_thesis: for h being Element of S holds
( h * s1 = h & s1 * h = h & ex g being Element of S st
( h * g = s1 & g * h = s1 ) )
let s be Element of S; ::_thesis: ( s * s1 = s & s1 * s = s & ex g being Element of S st
( s * g = s1 & g * s = s1 ) )
ex t being Element of S st t * the Element of S = s by A2;
hence A4: s * s1 = s by A1, A3; ::_thesis: ( s1 * s = s & ex g being Element of S st
( s * g = s1 & g * s = s1 ) )
consider s2 being Element of S such that
A5: s2 * the Element of S = the Element of S by A2;
consider t1 being Element of S such that
A6: the Element of S * t1 = s1 by A2;
A7: ex t2 being Element of S st t2 * the Element of S = s2 by A2;
A8: s1 = s2 * ( the Element of S * t1) by A1, A5, A6
.= s2 by A1, A3, A6, A7 ;
ex t being Element of S st the Element of S * t = s by A2;
hence A9: s1 * s = s by A1, A5, A8; ::_thesis: ex g being Element of S st
( s * g = s1 & g * s = s1 )
consider t1 being Element of S such that
A10: s * t1 = s1 by A2;
consider t2 being Element of S such that
A11: t2 * s = s1 by A2;
take t1 ; ::_thesis: ( s * t1 = s1 & t1 * s = s1 )
consider r1 being Element of S such that
A12: s * r1 = t1 by A2;
A13: ex r2 being Element of S st r2 * s = t2 by A2;
t1 = s1 * (s * r1) by A1, A9, A12
.= t2 * (s * t1) by A1, A11, A12
.= t2 by A1, A4, A10, A13 ;
hence ( s * t1 = s1 & t1 * s = s1 ) by A10, A11; ::_thesis: verum
end;
theorem Th3: :: GROUP_1:3
( multMagma(# REAL,addreal #) is associative & multMagma(# REAL,addreal #) is Group-like )
proof
set G = multMagma(# REAL,addreal #);
thus for h, g, f being Element of multMagma(# REAL,addreal #) holds (h * g) * f = h * (g * f) :: according to GROUP_1:def_3 ::_thesis: multMagma(# REAL,addreal #) is Group-like
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 ; :: according to GROUP_1:def_2 ::_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 ; ::_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 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
let e1, e2 be Element of G; ::_thesis: ( ( for h being Element of G holds
( h * e1 = h & e1 * h = h ) ) & ( for h being Element of G holds
( h * e2 = h & e2 * h = h ) ) implies e1 = e2 )
assume that
A1: for h being Element of G holds
( h * e1 = h & e1 * h = h ) and
A2: for h being Element of G holds
( h * e2 = h & e2 * h = h ) ; ::_thesis: e1 = e2
thus e1 = e2 * e1 by A2
.= e2 by A1 ; ::_thesis: verum
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;
funch " -> 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
consider e being Element of G such that
A1: for h being Element of G holds
( h * e = h & e * h = h & ex g being Element of G st
( h * g = e & g * h = e ) ) by Def2;
consider g being Element of G such that
A2: ( h * g = e & g * h = e ) by A1;
take g ; ::_thesis: ( h * g = 1_ G & g * h = 1_ G )
thus ( h * g = 1_ G & g * h = 1_ G ) by A1, A2, Def4; ::_thesis: verum
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
let h1, h2 be Element of G; ::_thesis: ( h * h1 = 1_ G & h1 * h = 1_ G & h * h2 = 1_ G & h2 * h = 1_ G implies h1 = h2 )
assume that
A3: h * h1 = 1_ G and
h1 * h = 1_ G and
h * h2 = 1_ G and
A4: h2 * h = 1_ G ; ::_thesis: h1 = h2
thus h1 = (1_ G) * h1 by Def4
.= h2 * (h * h1) by A4, Def3
.= h2 by A3, Def4 ; ::_thesis: verum
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
let G be Group; ::_thesis: for h, g, f being Element of G st ( h * g = h * f or g * h = f * h ) holds
g = f
let h, g, f be Element of G; ::_thesis: ( ( h * g = h * f or g * h = f * h ) implies g = f )
assume ( h * g = h * f or g * h = f * h ) ; ::_thesis: g = f
then ( (h ") * (h * g) = ((h ") * h) * f or (g * h) * (h ") = f * (h * (h ")) ) by Def3;
then ( (h ") * (h * g) = (1_ G) * f or g * (h * (h ")) = f * (h * (h ")) ) by Def3, Def5;
then ( (h ") * (h * g) = f or g * (1_ G) = f * (h * (h ")) ) by Def4, Def5;
then ( ((h ") * h) * g = f or g = f * (h * (h ")) ) by Def3, Def4;
then ( ((h ") * h) * g = f or g = f * (1_ G) ) by Def5;
then ( (1_ G) * g = f or g = f ) by Def4, Def5;
hence g = f by Def4; ::_thesis: verum
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
let G be Group; ::_thesis: for h, g being Element of G st ( h * g = h or g * h = h ) holds
g = 1_ G
let h, g be Element of G; ::_thesis: ( ( h * g = h or g * h = h ) implies g = 1_ G )
( h * (1_ G) = h & (1_ G) * h = h ) by Def4;
hence ( ( h * g = h or g * h = h ) implies g = 1_ G ) by Th6; ::_thesis: verum
end;
theorem Th8: :: GROUP_1:8
for G being Group holds (1_ G) " = 1_ G
proof
let G be Group; ::_thesis: (1_ G) " = 1_ G
((1_ G) ") * (1_ G) = 1_ G by Def5;
hence (1_ G) " = 1_ G by Def4; ::_thesis: verum
end;
theorem :: GROUP_1:9
for G being Group
for h, g being Element of G st h " = g " holds
h = g
proof
let G be Group; ::_thesis: for h, g being Element of G st h " = g " holds
h = g
let h, g be Element of G; ::_thesis: ( h " = g " implies h = g )
assume h " = g " ; ::_thesis: h = g
then A1: h * (g ") = 1_ G by Def5;
g * (g ") = 1_ G by Def5;
hence h = g by A1, Th6; ::_thesis: verum
end;
theorem :: GROUP_1:10
for G being Group
for h being Element of G st h " = 1_ G holds
h = 1_ G
proof
let G be Group; ::_thesis: for h being Element of G st h " = 1_ G holds
h = 1_ G
let h be Element of G; ::_thesis: ( h " = 1_ G implies h = 1_ G )
(1_ G) " = 1_ G by Th8;
hence ( h " = 1_ G implies h = 1_ G ) ; ::_thesis: verum
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
let G be Group; ::_thesis: for h, g being Element of G st h * g = 1_ G holds
( h = g " & g = h " )
let h, g be Element of G; ::_thesis: ( h * g = 1_ G implies ( h = g " & g = h " ) )
assume A1: h * g = 1_ G ; ::_thesis: ( h = g " & g = h " )
( h * (h ") = 1_ G & (g ") * g = 1_ G ) by Def5;
hence ( h = g " & g = h " ) by A1, Th6; ::_thesis: verum
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
let G be Group; ::_thesis: for h, f, g being Element of G holds
( h * f = g iff f = (h ") * g )
let h, f, g be Element of G; ::_thesis: ( h * f = g iff f = (h ") * g )
h * ((h ") * g) = (h * (h ")) * g by Def3
.= (1_ G) * g by Def5
.= g by Def4 ;
hence ( h * f = g implies f = (h ") * g ) by Th6; ::_thesis: ( f = (h ") * g implies h * f = g )
assume f = (h ") * g ; ::_thesis: h * f = g
hence h * f = (h * (h ")) * g by Def3
.= (1_ G) * g by Def5
.= g by Def4 ;
::_thesis: verum
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
let G be Group; ::_thesis: for f, h, g being Element of G holds
( f * h = g iff f = g * (h ") )
let f, h, g be Element of G; ::_thesis: ( f * h = g iff f = g * (h ") )
(g * (h ")) * h = g * ((h ") * h) by Def3
.= g * (1_ G) by Def5
.= g by Def4 ;
hence ( f * h = g implies f = g * (h ") ) by Th6; ::_thesis: ( f = g * (h ") implies f * h = g )
assume f = g * (h ") ; ::_thesis: f * h = g
hence f * h = g * ((h ") * h) by Def3
.= g * (1_ G) by Def5
.= g by Def4 ;
::_thesis: verum
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
let G be Group; ::_thesis: for g, h being Element of G ex f being Element of G st g * f = h
let g, h be Element of G; ::_thesis: ex f being Element of G st g * f = h
take (g ") * h ; ::_thesis: g * ((g ") * h) = h
thus g * ((g ") * h) = h by Th13; ::_thesis: verum
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
let G be Group; ::_thesis: for g, h being Element of G ex f being Element of G st f * g = h
let g, h be Element of G; ::_thesis: ex f being Element of G st f * g = h
take h * (g ") ; ::_thesis: (h * (g ")) * g = h
thus (h * (g ")) * g = h by Th14; ::_thesis: verum
end;
theorem Th17: :: GROUP_1:17
for G being Group
for h, g being Element of G holds (h * g) " = (g ") * (h ")
proof
let G be Group; ::_thesis: for h, g being Element of G holds (h * g) " = (g ") * (h ")
let h, g be Element of G; ::_thesis: (h * g) " = (g ") * (h ")
((g ") * (h ")) * (h * g) = (((g ") * (h ")) * h) * g by Def3
.= ((g ") * ((h ") * h)) * g by Def3
.= ((g ") * (1_ G)) * g by Def5
.= (g ") * g by Def4
.= 1_ G by Def5 ;
hence (h * g) " = (g ") * (h ") by Th12; ::_thesis: verum
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
let G be Group; ::_thesis: for g, h being Element of G holds
( g * h = h * g iff (g * h) " = (g ") * (h ") )
let g, h be Element of G; ::_thesis: ( g * h = h * g iff (g * h) " = (g ") * (h ") )
thus ( g * h = h * g implies (g * h) " = (g ") * (h ") ) by Th17; ::_thesis: ( (g * h) " = (g ") * (h ") implies g * h = h * g )
assume (g * h) " = (g ") * (h ") ; ::_thesis: g * h = h * g
then A1: (h * g) * ((g * h) ") = ((h * g) * (g ")) * (h ") by Def3
.= (h * (g * (g "))) * (h ") by Def3
.= (h * (1_ G)) * (h ") by Def5
.= h * (h ") by Def4
.= 1_ G by Def5 ;
(g * h) * ((g * h) ") = 1_ G by Def5;
hence g * h = h * g by A1, Th6; ::_thesis: verum
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
let G be Group; ::_thesis: for g, h being Element of G holds
( g * h = h * g iff (g ") * (h ") = (h ") * (g ") )
let g, h be Element of G; ::_thesis: ( g * h = h * g iff (g ") * (h ") = (h ") * (g ") )
thus ( g * h = h * g implies (g ") * (h ") = (h ") * (g ") ) ::_thesis: ( (g ") * (h ") = (h ") * (g ") implies g * h = h * g )
proof
assume A1: g * h = h * g ; ::_thesis: (g ") * (h ") = (h ") * (g ")
hence (g ") * (h ") = (g * h) " by Th17
.= (h ") * (g ") by A1, Th18 ;
::_thesis: verum
end;
assume A2: (g ") * (h ") = (h ") * (g ") ; ::_thesis: g * h = h * g
thus g * h = ((g * h) ") "
.= ((h ") * (g ")) " by Th17
.= ((h ") ") * ((g ") ") by A2, Th17
.= h * g ; ::_thesis: verum
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
let G be Group; ::_thesis: for g, h being Element of G holds
( g * h = h * g iff g * (h ") = (h ") * g )
let g, h be Element of G; ::_thesis: ( g * h = h * g iff g * (h ") = (h ") * g )
thus ( g * h = h * g implies g * (h ") = (h ") * g ) ::_thesis: ( g * (h ") = (h ") * g implies g * h = h * g )
proof
assume A1: g * h = h * g ; ::_thesis: g * (h ") = (h ") * g
(g * (h ")) * ((g ") * h) = ((g * (h ")) * (g ")) * h by Def3
.= (g * ((h ") * (g "))) * h by Def3
.= (g * ((g ") * (h "))) * h by A1, Th19
.= ((g * (g ")) * (h ")) * h by Def3
.= ((1_ G) * (h ")) * h by Def5
.= (h ") * h by Def4
.= 1_ G by Def5 ;
then g * (h ") = ((g ") * h) " by Th12
.= (h ") * ((g ") ") by Th17 ;
hence g * (h ") = (h ") * g ; ::_thesis: verum
end;
assume g * (h ") = (h ") * g ; ::_thesis: g * h = h * g
then g * ((h ") * h) = ((h ") * g) * h by Def3;
then g * (1_ G) = ((h ") * g) * h by Def5;
then g = ((h ") * g) * h by Def4;
then g = (h ") * (g * h) by Def3;
then h * g = (h * (h ")) * (g * h) by Def3;
then h * g = (1_ G) * (g * h) by Def5;
hence g * h = h * g by Def4; ::_thesis: verum
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
deffunc H1( Element of G) -> Element of G = $1 " ;
consider u being UnOp of G such that
A1: for h being Element of G holds u . h = H1(h) from FUNCT_2:sch_4();
take u ; ::_thesis: for h being Element of G holds u . h = h "
let h be Element of G; ::_thesis: u . h = h "
thus u . h = h " by A1; ::_thesis: verum
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
let u1, u2 be UnOp of G; ::_thesis: ( ( for h being Element of G holds u1 . h = h " ) & ( for h being Element of G holds u2 . h = h " ) implies u1 = u2 )
assume A2: for h being Element of G holds u1 . h = h " ; ::_thesis: ( ex h being Element of G st not u2 . h = h " or u1 = u2 )
assume A3: for h being Element of G holds u2 . h = h " ; ::_thesis: u1 = u2
let h be Element of G; :: according to FUNCT_2:def_8 ::_thesis: u1 . h = u2 . h
thus u1 . h = h " by A2
.= u2 . h by A3 ; ::_thesis: verum
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
let h, g, f be Element of G; :: according to BINOP_1:def_3 ::_thesis: the multF of G . (h,( the multF of G . (g,f))) = the multF of G . (( the multF of G . (h,g)),f)
set o = the multF of G;
thus the multF of G . (h,( the multF of G . (g,f))) = h * (g * f)
.= (h * g) * f by Def3
.= the multF of G . (( the multF of G . (h,g)),f) ; ::_thesis: verum
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
let G be non empty unital multMagma ; ::_thesis: 1_ G is_a_unity_wrt the multF of G
set o = the multF of G;
now__::_thesis:_for_h_being_Element_of_G_holds_
(_the_multF_of_G_._((1__G),h)_=_h_&_the_multF_of_G_._(h,(1__G))_=_h_)
let h be Element of G; ::_thesis: ( the multF of G . ((1_ G),h) = h & the multF of G . (h,(1_ G)) = h )
thus the multF of G . ((1_ G),h) = (1_ G) * h
.= h by Def4 ; ::_thesis: the multF of G . (h,(1_ G)) = h
thus the multF of G . (h,(1_ G)) = h * (1_ G)
.= h by Def4 ; ::_thesis: verum
end;
hence 1_ G is_a_unity_wrt the multF of G by BINOP_1:3; ::_thesis: verum
end;
theorem Th22: :: GROUP_1:22
for G being non empty unital multMagma holds the_unity_wrt the multF of G = 1_ G
proof
let G be non empty unital multMagma ; ::_thesis: the_unity_wrt the multF of G = 1_ G
1_ G is_a_unity_wrt the multF of G by Th21;
hence the_unity_wrt the multF of G = 1_ G by BINOP_1:def_8; ::_thesis: verum
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
take 1_ G ; :: according to SETWISEO:def_2 ::_thesis: 1_ G is_a_unity_wrt the multF of G
thus 1_ G is_a_unity_wrt the multF of G by Th21; ::_thesis: verum
end;
end;
theorem Th23: :: GROUP_1:23
for G being Group holds inverse_op G is_an_inverseOp_wrt the multF of G
proof
let G be Group; ::_thesis: inverse_op G is_an_inverseOp_wrt the multF of G
let h be Element of G; :: according to FINSEQOP:def_1 ::_thesis: ( the multF of G . (h,((inverse_op G) . h)) = the_unity_wrt the multF of G & the multF of G . (((inverse_op G) . h),h) = the_unity_wrt the multF of G )
thus the multF of G . (h,((inverse_op G) . h)) = h * (h ") by Def6
.= 1_ G by Def5
.= the_unity_wrt the multF of G by Th22 ; ::_thesis: the multF of G . (((inverse_op G) . h),h) = the_unity_wrt the multF of G
thus the multF of G . (((inverse_op G) . h),h) = (h ") * h by Def6
.= 1_ G by Def5
.= the_unity_wrt the multF of G by Th22 ; ::_thesis: verum
end;
registration
let G be Group;
cluster the multF of G -> having_an_inverseOp ;
coherence
the multF of G is having_an_inverseOp
proof
inverse_op G is_an_inverseOp_wrt the multF of G by Th23;
hence the multF of G is having_an_inverseOp by FINSEQOP:def_2; ::_thesis: verum
end;
end;
theorem :: GROUP_1:24
for G being Group holds the_inverseOp_wrt the multF of G = inverse_op G
proof
let G be Group; ::_thesis: the_inverseOp_wrt the multF of G = inverse_op G
set o = the multF of G;
( the multF of G is having_an_inverseOp & inverse_op G is_an_inverseOp_wrt the multF of G ) by Th23;
hence the_inverseOp_wrt the multF of G = inverse_op G by FINSEQOP:def_3; ::_thesis: verum
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
defpred S1[ set , set ] means ex g0 being Function of NAT, the carrier of G ex h being Element of G st
( $1 = h & g0 = $2 & g0 . 0 = 1_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * h ) );
A1: for x being set st x in the carrier of G holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier of G implies ex y being set st S1[x,y] )
assume x in the carrier of G ; ::_thesis: ex y being set st S1[x,y]
then reconsider b = x as Element of G ;
deffunc H1( Nat, Element of G) -> Element of the carrier of G = $2 * b;
consider g0 being Function of NAT, the carrier of G such that
A2: g0 . 0 = 1_ G and
A3: for n being Nat holds g0 . (n + 1) = H1(n,g0 . n) from NAT_1:sch_12();
reconsider y = g0 as set ;
take y ; ::_thesis: S1[x,y]
take g0 ; ::_thesis: ex h being Element of G st
( x = h & g0 = y & g0 . 0 = 1_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * h ) )
take b ; ::_thesis: ( x = b & g0 = y & g0 . 0 = 1_ G & ( for n being Nat holds g0 . (n + 1) = (g0 . n) * b ) )
thus ( x = b & g0 = y & g0 . 0 = 1_ G ) by A2; ::_thesis: for n being Nat holds g0 . (n + 1) = (g0 . n) * b
let n be Nat; ::_thesis: g0 . (n + 1) = (g0 . n) * b
thus g0 . (n + 1) = (g0 . n) * b by A3; ::_thesis: verum
end;
consider f being Function such that
dom f = the carrier of G and
A4: for x being set st x in the carrier of G holds
S1[x,f . x] from CLASSES1:sch_1(A1);
defpred S2[ Element of G, Element of NAT , set ] means ex g0 being Function of NAT, the carrier of G st
( g0 = f . $1 & $3 = g0 . $2 );
A5: for a being Element of G
for n being Element of NAT ex b being Element of G st S2[a,n,b]
proof
let a be Element of G; ::_thesis: for n being Element of NAT ex b being Element of G st S2[a,n,b]
let n be Element of NAT ; ::_thesis: ex b being Element of G st S2[a,n,b]
consider g0 being Function of NAT, the carrier of G, h being Element of G such that
a = h and
A6: g0 = f . a and
g0 . 0 = 1_ G and
for n being Nat holds g0 . (n + 1) = (g0 . n) * h by A4;
take g0 . n ; ::_thesis: S2[a,n,g0 . n]
take g0 ; ::_thesis: ( g0 = f . a & g0 . n = g0 . n )
thus ( g0 = f . a & g0 . n = g0 . n ) by A6; ::_thesis: verum
end;
consider F being Function of [: the carrier of G,NAT:], the carrier of G such that
A7: for a being Element of G
for n being Element of NAT holds S2[a,n,F . (a,n)] from BINOP_1:sch_3(A5);
take F ; ::_thesis: for h being Element of G holds
( F . (h,0) = 1_ G & ( for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h ) )
let h be Element of G; ::_thesis: ( F . (h,0) = 1_ G & ( for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h ) )
A8: ex g2 being Function of NAT, the carrier of G ex b being Element of G st
( h = b & g2 = f . h & g2 . 0 = 1_ G & ( for n being Nat holds g2 . (n + 1) = (g2 . n) * b ) ) by A4;
ex g1 being Function of NAT, the carrier of G st
( g1 = f . h & F . (h,0) = g1 . 0 ) by A7;
hence F . (h,0) = 1_ G by A8; ::_thesis: for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h
let n be Element of NAT ; ::_thesis: F . (h,(n + 1)) = (F . (h,n)) * h
A9: ex g2 being Function of NAT, the carrier of G ex b being Element of G st
( h = b & g2 = f . h & g2 . 0 = 1_ G & ( for n being Nat holds g2 . (n + 1) = (g2 . n) * b ) ) by A4;
( ex g0 being Function of NAT, the carrier of G st
( g0 = f . h & F . (h,n) = g0 . n ) & ex g1 being Function of NAT, the carrier of G st
( g1 = f . h & F . (h,(n + 1)) = g1 . (n + 1) ) ) by A7;
hence F . (h,(n + 1)) = (F . (h,n)) * h by A9; ::_thesis: verum
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
let f, g be Function of [: the carrier of G,NAT:], the carrier of G; ::_thesis: ( ( for h being Element of G holds
( f . (h,0) = 1_ G & ( for n being Element of NAT holds f . (h,(n + 1)) = (f . (h,n)) * h ) ) ) & ( for h being Element of G holds
( g . (h,0) = 1_ G & ( for n being Element of NAT holds g . (h,(n + 1)) = (g . (h,n)) * h ) ) ) implies f = g )
assume that
A10: for h being Element of G holds
( f . (h,0) = 1_ G & ( for n being Element of NAT holds f . (h,(n + 1)) = (f . (h,n)) * h ) ) and
A11: for h being Element of G holds
( g . (h,0) = 1_ G & ( for n being Element of NAT holds g . (h,(n + 1)) = (g . (h,n)) * h ) ) ; ::_thesis: f = g
now__::_thesis:_for_h_being_Element_of_G
for_n_being_Element_of_NAT_holds_f_._(h,n)_=_g_._(h,n)
let h be Element of G; ::_thesis: for n being Element of NAT holds f . (h,n) = g . (h,n)
let n be Element of NAT ; ::_thesis: f . (h,n) = g . (h,n)
defpred S1[ Nat] means f . [h,$1] = g . [h,$1];
A12: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A13: S1[n] ; ::_thesis: S1[n + 1]
A14: g . [h,n] = g . (h,n) ;
f . [h,(n + 1)] = f . (h,(n + 1))
.= (f . (h,n)) * h by A10
.= g . (h,(n + 1)) by A11, A13, A14
.= g . [h,(n + 1)] ;
hence S1[n + 1] ; ::_thesis: verum
end;
f . [h,0] = f . (h,0)
.= 1_ G by A10
.= g . (h,0) by A11
.= g . [h,0] ;
then A15: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A15, A12);
hence f . (h,n) = g . (h,n) ; ::_thesis: verum
end;
hence f = g by BINOP_1:2; ::_thesis: verum
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;
funch |^ 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
let g be Element of G; ::_thesis: ( g = h |^ n iff g = (power G) . (h,n) )
abs n = n by ABSVALUE:def_1;
hence ( g = h |^ n iff g = (power G) . (h,n) ) by Def8; ::_thesis: verum
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
let n be Nat; ::_thesis: for G being Group
for h being Element of G holds h |^ (n + 1) = (h |^ n) * h
let G be Group; ::_thesis: for h being Element of G holds h |^ (n + 1) = (h |^ n) * h
let h be Element of G; ::_thesis: h |^ (n + 1) = (h |^ n) * h
reconsider n = n as Element of NAT by ORDINAL1:def_12;
h |^ (n + 1) = (h |^ n) * h by Def7;
hence h |^ (n + 1) = (h |^ n) * h ; ::_thesis: verum
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
let n be Nat; ::_thesis: for G being Group holds (1_ G) |^ n = 1_ G
let G be Group; ::_thesis: (1_ G) |^ n = 1_ G
defpred S1[ Nat] means (1_ G) |^ $1 = 1_ G;
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then (1_ G) |^ (n + 1) = (1_ G) * (1_ G) by Lm2
.= 1_ G by Def4 ;
hence S1[n + 1] ; ::_thesis: verum
end;
A2: S1[ 0 ] by Def7;
for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1);
hence (1_ G) |^ n = 1_ G ; ::_thesis: verum
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
let G be Group; ::_thesis: for h being Element of G holds h |^ 1 = h
let h be Element of G; ::_thesis: h |^ 1 = h
thus h |^ 1 = h |^ (0 + 1)
.= (h |^ 0) * h by Lm2
.= (1_ G) * h by Def7
.= h by Def4 ; ::_thesis: verum
end;
theorem Th27: :: GROUP_1:27
for G being Group
for h being Element of G holds h |^ 2 = h * h
proof
let G be Group; ::_thesis: for h being Element of G holds h |^ 2 = h * h
let h be Element of G; ::_thesis: h |^ 2 = h * h
thus h |^ 2 = h |^ (1 + 1)
.= (h |^ 1) * h by Lm2
.= h * h by Th26 ; ::_thesis: verum
end;
theorem :: GROUP_1:28
for G being Group
for h being Element of G holds h |^ 3 = (h * h) * h
proof
let G be Group; ::_thesis: for h being Element of G holds h |^ 3 = (h * h) * h
let h be Element of G; ::_thesis: h |^ 3 = (h * h) * h
thus h |^ 3 = h |^ (2 + 1)
.= (h |^ 2) * h by Lm2
.= (h * h) * h by Th27 ; ::_thesis: verum
end;
theorem :: GROUP_1:29
for G being Group
for h being Element of G holds
( h |^ 2 = 1_ G iff h " = h )
proof
let G be Group; ::_thesis: for h being Element of G holds
( h |^ 2 = 1_ G iff h " = h )
let h be Element of G; ::_thesis: ( h |^ 2 = 1_ G iff h " = h )
thus ( h |^ 2 = 1_ G implies h = h " ) ::_thesis: ( h " = h implies h |^ 2 = 1_ G )
proof
assume h |^ 2 = 1_ G ; ::_thesis: h = h "
then h * h = 1_ G by Th27;
hence h = h " by Th12; ::_thesis: verum
end;
assume h = h " ; ::_thesis: h |^ 2 = 1_ G
hence h |^ 2 = h * (h ") by Th27
.= 1_ G by Def5 ;
::_thesis: verum
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
let n, m be Nat; ::_thesis: for G being Group
for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)
let G be Group; ::_thesis: for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)
let h be Element of G; ::_thesis: h |^ (n + m) = (h |^ n) * (h |^ m)
defpred S1[ Nat] means for n being Nat holds h |^ (n + $1) = (h |^ n) * (h |^ $1);
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: for n being Nat holds h |^ (n + m) = (h |^ n) * (h |^ m) ; ::_thesis: S1[m + 1]
let n be Nat; ::_thesis: h |^ (n + (m + 1)) = (h |^ n) * (h |^ (m + 1))
thus h |^ (n + (m + 1)) = h |^ ((n + m) + 1)
.= (h |^ (n + m)) * h by Lm2
.= ((h |^ n) * (h |^ m)) * h by A2
.= (h |^ n) * ((h |^ m) * h) by Def3
.= (h |^ n) * (h |^ (m + 1)) by Lm2 ; ::_thesis: verum
end;
A3: S1[ 0 ]
proof
let n be Nat; ::_thesis: h |^ (n + 0) = (h |^ n) * (h |^ 0)
thus h |^ (n + 0) = (h |^ n) * (1_ G) by Def4
.= (h |^ n) * (h |^ 0) by Def7 ; ::_thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch_2(A3, A1);
hence h |^ (n + m) = (h |^ n) * (h |^ m) ; ::_thesis: verum
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
let n be Nat; ::_thesis: for G being Group
for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
let G be Group; ::_thesis: for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
let h be Element of G; ::_thesis: ( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )
thus h |^ (n + 1) = (h |^ n) * h by Lm2; ::_thesis: h |^ (n + 1) = h * (h |^ n)
thus h |^ (n + 1) = (h |^ 1) * (h |^ n) by Lm5
.= h * (h |^ n) by Th26 ; ::_thesis: verum
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
let n, m be Nat; ::_thesis: for G being Group
for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m
let G be Group; ::_thesis: for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m
let h be Element of G; ::_thesis: h |^ (n * m) = (h |^ n) |^ m
defpred S1[ Nat] means for n being Nat holds h |^ (n * $1) = (h |^ n) |^ $1;
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: for n being Nat holds h |^ (n * m) = (h |^ n) |^ m ; ::_thesis: S1[m + 1]
let n be Nat; ::_thesis: h |^ (n * (m + 1)) = (h |^ n) |^ (m + 1)
thus h |^ (n * (m + 1)) = h |^ ((n * m) + (n * 1))
.= (h |^ (n * m)) * (h |^ n) by Lm5
.= ((h |^ n) |^ m) * (h |^ n) by A2
.= ((h |^ n) |^ m) * ((h |^ n) |^ 1) by Th26
.= (h |^ n) |^ (m + 1) by Lm5 ; ::_thesis: verum
end;
A3: S1[ 0 ]
proof
let n be Nat; ::_thesis: h |^ (n * 0) = (h |^ n) |^ 0
thus h |^ (n * 0) = 1_ G by Def7
.= (h |^ n) |^ 0 by Def7 ; ::_thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch_2(A3, A1);
hence h |^ (n * m) = (h |^ n) |^ m ; ::_thesis: verum
end;
Lm8: for n being Nat
for G being Group
for h being Element of G holds (h ") |^ n = (h |^ n) "
proof
let n be Nat; ::_thesis: for G being Group
for h being Element of G holds (h ") |^ n = (h |^ n) "
let G be Group; ::_thesis: for h being Element of G holds (h ") |^ n = (h |^ n) "
let h be Element of G; ::_thesis: (h ") |^ n = (h |^ n) "
defpred S1[ Nat] means (h ") |^ $1 = (h |^ $1) " ;
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then (h ") |^ (n + 1) = ((h |^ n) ") * (h ") by Lm2
.= (h * (h |^ n)) " by Th17
.= (h |^ (n + 1)) " by Lm6 ;
hence S1[n + 1] ; ::_thesis: verum
end;
(h ") |^ 0 = 1_ G by Def7
.= (1_ G) " by Th8
.= (h |^ 0) " by Def7 ;
then A2: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1);
hence (h ") |^ n = (h |^ n) " ; ::_thesis: verum
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
let n be Nat; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ n) = (h |^ n) * g
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
g * (h |^ n) = (h |^ n) * g
let g, h be Element of G; ::_thesis: ( g * h = h * g implies g * (h |^ n) = (h |^ n) * g )
defpred S1[ Nat] means ( g * h = h * g implies g * (h |^ $1) = (h |^ $1) * g );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: ( g * h = h * g implies g * (h |^ n) = (h |^ n) * g ) ; ::_thesis: S1[n + 1]
assume A3: g * h = h * g ; ::_thesis: g * (h |^ (n + 1)) = (h |^ (n + 1)) * g
thus g * (h |^ (n + 1)) = g * (h * (h |^ n)) by Lm6
.= (g * h) * (h |^ n) by Def3
.= h * ((h |^ n) * g) by A2, A3, Def3
.= (h * (h |^ n)) * g by Def3
.= (h |^ (n + 1)) * g by Lm6 ; ::_thesis: verum
end;
A4: S1[ 0 ]
proof
assume g * h = h * g ; ::_thesis: g * (h |^ 0) = (h |^ 0) * g
thus g * (h |^ 0) = g * (1_ G) by Def7
.= g by Def4
.= (1_ G) * g by Def4
.= (h |^ 0) * g by Def7 ; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1);
hence ( g * h = h * g implies g * (h |^ n) = (h |^ n) * g ) ; ::_thesis: verum
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
let n, m be Nat; ::_thesis: 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)
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)
let g, h be Element of G; ::_thesis: ( g * h = h * g implies (g |^ n) * (h |^ m) = (h |^ m) * (g |^ n) )
defpred S1[ Nat] means for m being Nat st g * h = h * g holds
(g |^ $1) * (h |^ m) = (h |^ m) * (g |^ $1);
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for m being Nat st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n) ; ::_thesis: S1[n + 1]
let m be Nat; ::_thesis: ( g * h = h * g implies (g |^ (n + 1)) * (h |^ m) = (h |^ m) * (g |^ (n + 1)) )
assume A3: g * h = h * g ; ::_thesis: (g |^ (n + 1)) * (h |^ m) = (h |^ m) * (g |^ (n + 1))
thus (g |^ (n + 1)) * (h |^ m) = (g * (g |^ n)) * (h |^ m) by Lm6
.= g * ((g |^ n) * (h |^ m)) by Def3
.= g * ((h |^ m) * (g |^ n)) by A2, A3
.= (g * (h |^ m)) * (g |^ n) by Def3
.= ((h |^ m) * g) * (g |^ n) by A3, Lm9
.= (h |^ m) * (g * (g |^ n)) by Def3
.= (h |^ m) * (g |^ (n + 1)) by Lm6 ; ::_thesis: verum
end;
A4: S1[ 0 ]
proof
let m be Nat; ::_thesis: ( g * h = h * g implies (g |^ 0) * (h |^ m) = (h |^ m) * (g |^ 0) )
assume g * h = h * g ; ::_thesis: (g |^ 0) * (h |^ m) = (h |^ m) * (g |^ 0)
thus (g |^ 0) * (h |^ m) = (1_ G) * (h |^ m) by Def7
.= h |^ m by Def4
.= (h |^ m) * (1_ G) by Def4
.= (h |^ m) * (g |^ 0) by Def7 ; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1);
hence ( g * h = h * g implies (g |^ n) * (h |^ m) = (h |^ m) * (g |^ n) ) ; ::_thesis: verum
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
let n be Nat; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ n = (g |^ n) * (h |^ n)
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
(g * h) |^ n = (g |^ n) * (h |^ n)
let g, h be Element of G; ::_thesis: ( g * h = h * g implies (g * h) |^ n = (g |^ n) * (h |^ n) )
defpred S1[ Nat] means ( g * h = h * g implies (g * h) |^ $1 = (g |^ $1) * (h |^ $1) );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: ( g * h = h * g implies (g * h) |^ n = (g |^ n) * (h |^ n) ) ; ::_thesis: S1[n + 1]
assume A3: g * h = h * g ; ::_thesis: (g * h) |^ (n + 1) = (g |^ (n + 1)) * (h |^ (n + 1))
hence (g * h) |^ (n + 1) = ((g |^ n) * (h |^ n)) * (h * g) by A2, Lm6
.= (((g |^ n) * (h |^ n)) * h) * g by Def3
.= ((g |^ n) * ((h |^ n) * h)) * g by Def3
.= ((g |^ n) * (h |^ (n + 1))) * g by Lm6
.= ((h |^ (n + 1)) * (g |^ n)) * g by A3, Lm10
.= (h |^ (n + 1)) * ((g |^ n) * g) by Def3
.= (h |^ (n + 1)) * (g |^ (n + 1)) by Lm6
.= (g |^ (n + 1)) * (h |^ (n + 1)) by A3, Lm10 ;
::_thesis: verum
end;
A4: S1[ 0 ]
proof
assume g * h = h * g ; ::_thesis: (g * h) |^ 0 = (g |^ 0) * (h |^ 0)
thus (g * h) |^ 0 = 1_ G by Def7
.= (1_ G) * (1_ G) by Def4
.= (g |^ 0) * (1_ G) by Def7
.= (g |^ 0) * (h |^ 0) by Def7 ; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A4, A1);
hence ( g * h = h * g implies (g * h) |^ n = (g |^ n) * (h |^ n) ) ; ::_thesis: verum
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
let i be Integer; ::_thesis: for G being Group
for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "
let G be Group; ::_thesis: for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "
let h be Element of G; ::_thesis: ( i <= 0 implies h |^ i = (h |^ (abs i)) " )
assume A1: i <= 0 ; ::_thesis: h |^ i = (h |^ (abs i)) "
percases ( i < 0 or i = 0 ) by A1;
suppose i < 0 ; ::_thesis: h |^ i = (h |^ (abs i)) "
hence h |^ i = (h |^ (abs i)) " by Def8; ::_thesis: verum
end;
supposeA2: i = 0 ; ::_thesis: h |^ i = (h |^ (abs i)) "
hence h |^ i = 1_ G by Lm3
.= (1_ G) " by Th8
.= (h |^ 0) " by Def7
.= (h |^ (abs i)) " by A2, ABSVALUE:def_1 ;
::_thesis: verum
end;
end;
end;
theorem :: GROUP_1:31
for i being Integer
for G being Group holds (1_ G) |^ i = 1_ G
proof
let i be Integer; ::_thesis: for G being Group holds (1_ G) |^ i = 1_ G
let G be Group; ::_thesis: (1_ G) |^ i = 1_ G
( (1_ G) |^ i = (1_ G) |^ (abs i) or ( (1_ G) |^ i = ((1_ G) |^ (abs i)) " & (1_ G) " = 1_ G ) ) by Def8, Th8;
hence (1_ G) |^ i = 1_ G by Lm4; ::_thesis: verum
end;
theorem Th32: :: GROUP_1:32
for G being Group
for h being Element of G holds h |^ (- 1) = h "
proof
let G be Group; ::_thesis: for h being Element of G holds h |^ (- 1) = h "
let h be Element of G; ::_thesis: h |^ (- 1) = h "
abs (- 1) = - (- 1) by ABSVALUE:def_1;
hence h |^ (- 1) = (h |^ 1) " by Def8
.= h " by Th26 ;
::_thesis: verum
end;
Lm12: for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) "
proof
let i be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) "
let G be Group; ::_thesis: for h being Element of G holds h |^ (- i) = (h |^ i) "
let h be Element of G; ::_thesis: h |^ (- i) = (h |^ i) "
percases ( i >= 0 or i < 0 ) ;
supposeA1: i >= 0 ; ::_thesis: h |^ (- i) = (h |^ i) "
percases ( - i < - 0 or i = 0 ) by A1, XREAL_1:24;
supposeA2: - i < - 0 ; ::_thesis: h |^ (- i) = (h |^ i) "
hence h |^ (- i) = (h |^ (abs (- i))) " by Def8
.= (h |^ (- (- i))) " by A2, ABSVALUE:def_1
.= (h |^ i) " ;
::_thesis: verum
end;
supposeA3: i = 0 ; ::_thesis: h |^ (- i) = (h |^ i) "
hence h |^ (- i) = 1_ G by Lm3
.= (1_ G) " by Th8
.= (h |^ i) " by A3, Lm3 ;
::_thesis: verum
end;
end;
end;
supposeA4: i < 0 ; ::_thesis: h |^ (- i) = (h |^ i) "
then h |^ i = (h |^ (abs i)) " by Def8;
hence h |^ (- i) = (h |^ i) " by A4, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;
Lm13: for j being Integer holds
( j >= 1 or j = 0 or j < 0 )
proof
let j be Integer; ::_thesis: ( j >= 1 or j = 0 or j < 0 )
( j < 0 or ( j is Element of NAT & ( j <> 0 or j = 0 ) ) ) by INT_1:3;
hence ( j >= 1 or j = 0 or j < 0 ) by NAT_1:14; ::_thesis: verum
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
let j be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
let G be Group; ::_thesis: for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
let h be Element of G; ::_thesis: h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
A1: now__::_thesis:_(h_|^_(j_-_1))_*_(h_*_(h_|^_(-_j)))_=_1__G
percases ( j >= 1 or j < 0 or j = 0 ) by Lm13;
supposeA2: j >= 1 ; ::_thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G
then j >= 1 + 0 ;
then A3: j - 1 >= 0 by XREAL_1:19;
then A4: (abs (j - 1)) + 1 = (j - 1) + 1 by ABSVALUE:def_1
.= j ;
A5: abs j = j by A2, ABSVALUE:def_1;
A6: abs j = abs (- j) by COMPLEX1:52;
thus (h |^ (j - 1)) * (h * (h |^ (- j))) = ((h |^ (j - 1)) * h) * (h |^ (- j)) by Def3
.= ((h |^ (abs (j - 1))) * h) * (h |^ (- j)) by A3, Def8
.= ((h |^ (abs (j - 1))) * h) * ((h |^ (abs (- j))) ") by A2, Th30
.= (h |^ ((abs (j - 1)) + 1)) * ((h |^ (abs (- j))) ") by Lm6
.= 1_ G by A4, A5, A6, Def5 ; ::_thesis: verum
end;
supposeA7: j < 0 ; ::_thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G
A8: 1 - j = - (j - 1) ;
thus (h |^ (j - 1)) * (h * (h |^ (- j))) = ((h |^ (abs (j - 1))) ") * (h * (h |^ (- j))) by A7, Def8
.= ((h |^ (abs (j - 1))) ") * (h * (h |^ (abs (- j)))) by A7, Def8
.= ((h |^ (abs (j - 1))) ") * (h |^ (1 + (abs (- j)))) by Lm6
.= ((h |^ (abs (j - 1))) ") * (h |^ (1 + (- j))) by A7, ABSVALUE:def_1
.= ((h |^ (abs (j - 1))) ") * (h |^ (abs (j - 1))) by A7, A8, ABSVALUE:def_1
.= 1_ G by Def5 ; ::_thesis: verum
end;
supposeA9: j = 0 ; ::_thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G
hence (h |^ (j - 1)) * (h * (h |^ (- j))) = (h ") * (h * (h |^ (- j))) by Th32
.= ((h ") * h) * (h |^ (- j)) by Def3
.= (1_ G) * (h |^ (- j)) by Def5
.= h |^ 0 by A9, Def4
.= 1_ G by Def7 ;
::_thesis: verum
end;
end;
end;
(h |^ (j - 1)) * (h |^ (1 - j)) = (h |^ (j - 1)) * (h |^ (- (j - 1)))
.= (h |^ (j - 1)) * ((h |^ (j - 1)) ") by Lm12
.= 1_ G by Def5 ;
then h * (h |^ (- j)) = h |^ (1 - j) by A1, Th6;
then (h |^ (1 - j)) " = ((h |^ (- j)) ") * (h ") by Th17
.= (h |^ (- (- j))) * (h ") by Lm12
.= (h |^ j) * (h |^ (- 1)) by Th32 ;
then (h |^ j) * (h |^ (- 1)) = h |^ (- (1 - j)) by Lm12;
hence h |^ (j - 1) = (h |^ j) * (h |^ (- 1)) ; ::_thesis: verum
end;
Lm15: for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )
proof
let j be Integer; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 )
percases ( j >= 0 or j < 0 ) ;
suppose j >= 0 ; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 )
hence ( j >= 0 or j = - 1 or j < - 1 ) ; ::_thesis: verum
end;
supposeA1: j < 0 ; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 )
then reconsider n = - j as Element of NAT by INT_1:3;
n <> - 0 by A1;
then n >= 1 by NAT_1:14;
then ( n > 1 or n = 1 ) by XXREAL_0:1;
then ( - 1 > - (- j) or - 1 = j ) by XREAL_1:24;
hence ( j >= 0 or j = - 1 or j < - 1 ) ; ::_thesis: verum
end;
end;
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
let j be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)
let G be Group; ::_thesis: for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)
let h be Element of G; ::_thesis: h |^ (j + 1) = (h |^ j) * (h |^ 1)
A1: now__::_thesis:_(h_|^_(j_+_1))_*_((h_|^_(-_1))_*_(h_|^_(-_j)))_=_1__G
percases ( j >= 0 or j < - 1 or j = - 1 ) by Lm15;
supposeA2: j >= 0 ; ::_thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
then reconsider n = j as Element of NAT by INT_1:3;
A3: n + 1 = abs (j + 1) by ABSVALUE:def_1;
n + 1 >= 0 ;
hence (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = (h |^ (abs (j + 1))) * ((h |^ (- 1)) * (h |^ (- j))) by Def8
.= (h |^ (abs (j + 1))) * ((h ") * (h |^ (- j))) by Th32
.= (h |^ (abs (j + 1))) * ((h ") * ((h |^ j) ")) by Lm12
.= (h |^ (abs (j + 1))) * ((h ") * ((h |^ (abs j)) ")) by A2, Def8
.= (h |^ (abs (j + 1))) * (((h |^ (abs j)) * h) ") by Th17
.= (h |^ (abs (j + 1))) * ((h |^ ((abs j) + 1)) ") by Lm6
.= (h |^ (abs (j + 1))) * ((h |^ (abs (j + 1))) ") by A3, ABSVALUE:def_1
.= 1_ G by Def5 ;
::_thesis: verum
end;
suppose j < - 1 ; ::_thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
then A4: j + 1 < (- 1) + 1 by XREAL_1:6;
hence (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = ((h |^ (abs (j + 1))) ") * ((h |^ (- 1)) * (h |^ (- j))) by Def8
.= ((h |^ (abs (j + 1))) ") * ((h ") * (h |^ (- j))) by Th32
.= (((h |^ (abs (j + 1))) ") * (h ")) * (h |^ (- j)) by Def3
.= ((h * (h |^ (abs (j + 1)))) ") * (h |^ (- j)) by Th17
.= ((h |^ ((abs (j + 1)) + 1)) ") * (h |^ (- j)) by Lm6
.= ((h |^ ((- (j + 1)) + 1)) ") * (h |^ (- j)) by A4, ABSVALUE:def_1
.= 1_ G by Def5 ;
::_thesis: verum
end;
supposeA5: j = - 1 ; ::_thesis: (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = 1_ G
hence (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = (1_ G) * ((h |^ (- 1)) * (h |^ (- j))) by Lm3
.= (h |^ (- 1)) * (h |^ (- j)) by Def4
.= (h ") * (h |^ (- j)) by Th32
.= (h ") * ((h |^ j) ") by Lm12
.= (h ") * ((h ") ") by A5, Th32
.= 1_ G by Def5 ;
::_thesis: verum
end;
end;
end;
(h |^ (j + 1)) * (h |^ (- (j + 1))) = (h |^ (j + 1)) * ((h |^ (j + 1)) ") by Lm12
.= 1_ G by Def5 ;
then A6: h |^ (- (j + 1)) = (h |^ (- 1)) * (h |^ (- j)) by A1, Th6;
thus h |^ (j + 1) = h |^ (- (- (j + 1)))
.= ((h |^ (- 1)) * (h |^ (- j))) " by A6, Lm12
.= ((h |^ (- j)) ") * ((h |^ (- 1)) ") by Th17
.= (h |^ (- (- j))) * ((h |^ (- 1)) ") by Lm12
.= (h |^ j) * (h |^ (- (- 1))) by Lm12
.= (h |^ j) * (h |^ 1) ; ::_thesis: verum
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
let i, j be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)
let G be Group; ::_thesis: for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)
let h be Element of G; ::_thesis: h |^ (i + j) = (h |^ i) * (h |^ j)
defpred S1[ Integer] means for i being Integer holds h |^ (i + $1) = (h |^ i) * (h |^ $1);
A1: for j being Integer st S1[j] holds
( S1[j - 1] & S1[j + 1] )
proof
let j be Integer; ::_thesis: ( S1[j] implies ( S1[j - 1] & S1[j + 1] ) )
assume A2: for i being Integer holds h |^ (i + j) = (h |^ i) * (h |^ j) ; ::_thesis: ( S1[j - 1] & S1[j + 1] )
thus for i being Integer holds h |^ (i + (j - 1)) = (h |^ i) * (h |^ (j - 1)) ::_thesis: S1[j + 1]
proof
let i be Integer; ::_thesis: h |^ (i + (j - 1)) = (h |^ i) * (h |^ (j - 1))
thus h |^ (i + (j - 1)) = h |^ ((i - 1) + j)
.= (h |^ (i - 1)) * (h |^ j) by A2
.= ((h |^ i) * (h |^ (- 1))) * (h |^ j) by Lm14
.= (h |^ i) * ((h |^ (- 1)) * (h |^ j)) by Def3
.= (h |^ i) * (h |^ (j + (- 1))) by A2
.= (h |^ i) * (h |^ (j - 1)) ; ::_thesis: verum
end;
let i be Integer; ::_thesis: h |^ (i + (j + 1)) = (h |^ i) * (h |^ (j + 1))
thus h |^ (i + (j + 1)) = h |^ ((i + 1) + j)
.= (h |^ (i + 1)) * (h |^ j) by A2
.= ((h |^ i) * (h |^ 1)) * (h |^ j) by Lm16
.= (h |^ i) * ((h |^ 1) * (h |^ j)) by Def3
.= (h |^ i) * (h |^ (j + 1)) by A2 ; ::_thesis: verum
end;
A3: S1[ 0 ]
proof
let i be Integer; ::_thesis: h |^ (i + 0) = (h |^ i) * (h |^ 0)
thus h |^ (i + 0) = (h |^ i) * (1_ G) by Def4
.= (h |^ i) * (h |^ 0) by Def7 ; ::_thesis: verum
end;
for j being Integer holds S1[j] from INT_1:sch_4(A3, A1);
hence h |^ (i + j) = (h |^ i) * (h |^ j) ; ::_thesis: verum
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
let i be Integer; ::_thesis: for G being Group
for h being Element of G holds
( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
let G be Group; ::_thesis: for h being Element of G holds
( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
let h be Element of G; ::_thesis: ( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) )
h |^ 1 = h by Th26;
hence ( h |^ (i + 1) = (h |^ i) * h & h |^ (i + 1) = h * (h |^ i) ) by Th33; ::_thesis: verum
end;
Lm17: for i being Integer
for G being Group
for h being Element of G holds (h ") |^ i = (h |^ i) "
proof
let i be Integer; ::_thesis: for G being Group
for h being Element of G holds (h ") |^ i = (h |^ i) "
let G be Group; ::_thesis: for h being Element of G holds (h ") |^ i = (h |^ i) "
let h be Element of G; ::_thesis: (h ") |^ i = (h |^ i) "
percases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; ::_thesis: (h ") |^ i = (h |^ i) "
then reconsider n = i as Element of NAT by INT_1:3;
thus (h ") |^ i = (h |^ n) " by Lm8
.= (h |^ i) " ; ::_thesis: verum
end;
supposeA1: i < 0 ; ::_thesis: (h ") |^ i = (h |^ i) "
hence (h ") |^ i = ((h ") |^ (abs i)) " by Def8
.= ((h |^ (abs i)) ") " by Lm8
.= (h |^ i) " by A1, Def8 ;
::_thesis: verum
end;
end;
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
let i, j be Integer; ::_thesis: for G being Group
for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j
let G be Group; ::_thesis: for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j
let h be Element of G; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
percases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( j < 0 & i < 0 ) ) ;
suppose ( i >= 0 & j >= 0 ) ; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
then reconsider m = i, n = j as Element of NAT by INT_1:3;
thus h |^ (i * j) = (h |^ m) |^ n by Lm7
.= (h |^ i) |^ j ; ::_thesis: verum
end;
suppose ( i >= 0 & j < 0 ) ; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
then reconsider m = i, n = - j as Element of NAT by INT_1:3;
i * j = - (i * n) ;
hence h |^ (i * j) = (h |^ (i * n)) " by Lm12
.= (h ") |^ (i * n) by Lm17
.= ((h ") |^ m) |^ n by Lm7
.= ((h |^ i) ") |^ n by Lm17
.= (((h |^ i) ") |^ j) " by Lm12
.= (((h |^ i) |^ j) ") " by Lm17
.= (h |^ i) |^ j ;
::_thesis: verum
end;
suppose ( i < 0 & j >= 0 ) ; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
then reconsider m = - i, n = j as Element of NAT by INT_1:3;
i * j = - (m * j) ;
hence h |^ (i * j) = (h |^ (m * j)) " by Lm12
.= (h ") |^ (m * j) by Lm17
.= ((h ") |^ m) |^ n by Lm7
.= (((h ") |^ i) ") |^ n by Lm12
.= (((h |^ i) ") ") |^ j by Lm17
.= (h |^ i) |^ j ;
::_thesis: verum
end;
suppose ( j < 0 & i < 0 ) ; ::_thesis: h |^ (i * j) = (h |^ i) |^ j
then reconsider m = - i, n = - j as Element of NAT by INT_1:3;
(i * j) * ((- 1) * (- 1)) = m * n ;
hence h |^ (i * j) = (h |^ m) |^ n by Lm7
.= ((h |^ (- i)) |^ j) " by Lm12
.= (((h |^ i) ") |^ j) " by Lm12
.= (((h ") |^ i) |^ j) " by Lm17
.= (((h ") |^ i) ") |^ j by Lm17
.= (((h ") ") |^ i) |^ j by Lm17
.= (h |^ i) |^ j ;
::_thesis: verum
end;
end;
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
let i be Integer; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ i = (g |^ i) * (h |^ i)
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
(g * h) |^ i = (g |^ i) * (h |^ i)
let g, h be Element of G; ::_thesis: ( g * h = h * g implies (g * h) |^ i = (g |^ i) * (h |^ i) )
assume A1: g * h = h * g ; ::_thesis: (g * h) |^ i = (g |^ i) * (h |^ i)
percases ( i >= 0 or i < 0 ) ;
supposeA2: i >= 0 ; ::_thesis: (g * h) |^ i = (g |^ i) * (h |^ i)
then A3: h |^ i = h |^ (abs i) by Def8;
( (g * h) |^ i = (g * h) |^ (abs i) & g |^ i = g |^ (abs i) ) by A2, Def8;
hence (g * h) |^ i = (g |^ i) * (h |^ i) by A1, A3, Lm11; ::_thesis: verum
end;
supposeA4: i < 0 ; ::_thesis: (g * h) |^ i = (g |^ i) * (h |^ i)
hence (g * h) |^ i = ((h * g) |^ (abs i)) " by A1, Def8
.= ((h |^ (abs i)) * (g |^ (abs i))) " by A1, Lm11
.= ((g |^ (abs i)) ") * ((h |^ (abs i)) ") by Th17
.= (g |^ i) * ((h |^ (abs i)) ") by A4, Def8
.= (g |^ i) * (h |^ i) by A4, Def8 ;
::_thesis: verum
end;
end;
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
let i, j be Integer; ::_thesis: 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)
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
(g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
let g, h be Element of G; ::_thesis: ( g * h = h * g implies (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) )
assume A1: g * h = h * g ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
percases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( i < 0 & j < 0 ) ) ;
suppose ( i >= 0 & j >= 0 ) ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
then ( g |^ i = g |^ (abs i) & h |^ j = h |^ (abs j) ) by Def8;
hence (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A1, Lm10; ::_thesis: verum
end;
supposeA2: ( i >= 0 & j < 0 ) ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
A3: (g |^ (abs i)) * (h |^ (abs j)) = (h |^ (abs j)) * (g |^ (abs i)) by A1, Lm10;
( g |^ i = g |^ (abs i) & h |^ j = (h |^ (abs j)) " ) by A2, Def8;
hence (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A3, Th20; ::_thesis: verum
end;
supposeA4: ( i < 0 & j >= 0 ) ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
A5: (g |^ (abs i)) * (h |^ (abs j)) = (h |^ (abs j)) * (g |^ (abs i)) by A1, Lm10;
( g |^ i = (g |^ (abs i)) " & h |^ j = h |^ (abs j) ) by A4, Def8;
hence (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A5, Th20; ::_thesis: verum
end;
suppose ( i < 0 & j < 0 ) ; ::_thesis: (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)
then A6: ( g |^ i = (g |^ (abs i)) " & h |^ j = (h |^ (abs j)) " ) by Def8;
hence (g |^ i) * (h |^ j) = ((h |^ (abs j)) * (g |^ (abs i))) " by Th17
.= ((g |^ (abs i)) * (h |^ (abs j))) " by A1, Lm10
.= (h |^ j) * (g |^ i) by A6, Th17 ;
::_thesis: verum
end;
end;
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
let i be Integer; ::_thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ i) = (h |^ i) * g
let G be Group; ::_thesis: for g, h being Element of G st g * h = h * g holds
g * (h |^ i) = (h |^ i) * g
let g, h be Element of G; ::_thesis: ( g * h = h * g implies g * (h |^ i) = (h |^ i) * g )
assume A1: g * h = h * g ; ::_thesis: g * (h |^ i) = (h |^ i) * g
thus g * (h |^ i) = (g |^ 1) * (h |^ i) by Th26
.= (h |^ i) * (g |^ 1) by A1, Th39
.= (h |^ i) * g by Th26 ; ::_thesis: verum
end;
definition
let G be Group;
let h be Element of G;
attrh 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
(1_ G) |^ 8 = 1_ G by Lm4;
hence not 1_ G is being_of_order_0 by Def10; ::_thesis: verum
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
defpred S1[ Nat] means ( h |^ $1 = 1_ G & $1 <> 0 );
thus ( h is being_of_order_0 implies ex n being Element of NAT st n = 0 ) ; ::_thesis: ( 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 ) ) )
hereby ::_thesis: verum
assume not h is being_of_order_0 ; ::_thesis: ex k being Element of NAT st
( h |^ k = 1_ G & k <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
k <= m ) )
then A1: ex n being Nat st S1[n] by Def10;
consider k being Nat such that
A2: S1[k] and
A3: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A1);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take k = k; ::_thesis: ( h |^ k = 1_ G & k <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
k <= m ) )
thus ( h |^ k = 1_ G & k <> 0 ) by A2; ::_thesis: for m being Nat st h |^ m = 1_ G & m <> 0 holds
k <= m
let m be Nat; ::_thesis: ( h |^ m = 1_ G & m <> 0 implies k <= m )
assume ( h |^ m = 1_ G & m <> 0 ) ; ::_thesis: k <= m
hence k <= m by A3; ::_thesis: verum
end;
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
let n1, n2 be Element of NAT ; ::_thesis: ( ( h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2 ) & ( not h is being_of_order_0 & h |^ n1 = 1_ G & n1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n1 <= m ) & h |^ n2 = 1_ G & n2 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n2 <= m ) implies n1 = n2 ) )
thus ( h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ; ::_thesis: ( not h is being_of_order_0 & h |^ n1 = 1_ G & n1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n1 <= m ) & h |^ n2 = 1_ G & n2 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n2 <= m ) implies n1 = n2 )
assume that
not h is being_of_order_0 and
A4: ( h |^ n1 = 1_ G & n1 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n1 <= m ) & h |^ n2 = 1_ G & n2 <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
n2 <= m ) ) ; ::_thesis: n1 = n2
( n1 <= n2 & n2 <= n1 ) by A4;
hence n1 = n2 by XXREAL_0:1; ::_thesis: verum
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
let G be Group; ::_thesis: for h being Element of G holds h |^ (ord h) = 1_ G
let h be Element of G; ::_thesis: h |^ (ord h) = 1_ G
percases ( h is being_of_order_0 or not h is being_of_order_0 ) ;
suppose h is being_of_order_0 ; ::_thesis: h |^ (ord h) = 1_ G
then ord h = 0 by Def11;
hence h |^ (ord h) = 1_ G by Def7; ::_thesis: verum
end;
suppose not h is being_of_order_0 ; ::_thesis: h |^ (ord h) = 1_ G
hence h |^ (ord h) = 1_ G by Def11; ::_thesis: verum
end;
end;
end;
theorem :: GROUP_1:42
for G being Group holds ord (1_ G) = 1
proof
let G be Group; ::_thesis: ord (1_ G) = 1
A1: for n being Nat st (1_ G) |^ n = 1_ G & n <> 0 holds
1 <= n by NAT_1:14;
( not 1_ G is being_of_order_0 & (1_ G) |^ 1 = 1_ G ) by Lm4;
hence ord (1_ G) = 1 by A1, Def11; ::_thesis: verum
end;
theorem :: GROUP_1:43
for G being Group
for h being Element of G st ord h = 1 holds
h = 1_ G
proof
let G be Group; ::_thesis: for h being Element of G st ord h = 1 holds
h = 1_ G
let h be Element of G; ::_thesis: ( ord h = 1 implies h = 1_ G )
assume A1: ord h = 1 ; ::_thesis: h = 1_ G
then not h is being_of_order_0 by Def11;
then h |^ 1 = 1_ G by A1, Def11;
hence h = 1_ G by Th26; ::_thesis: verum
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
let n be Nat; ::_thesis: for G being Group
for h being Element of G st h |^ n = 1_ G holds
ord h divides n
let G be Group; ::_thesis: for h being Element of G st h |^ n = 1_ G holds
ord h divides n
let h be Element of G; ::_thesis: ( h |^ n = 1_ G implies ord h divides n )
defpred S1[ Nat] means ( h |^ $1 = 1_ G implies ord h divides $1 );
A1: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A2: for k being Nat st k < n holds
S1[k] ; ::_thesis: S1[n]
assume A3: h |^ n = 1_ G ; ::_thesis: ord h divides n
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: ord h divides n
hence ord h divides n by NAT_D:6; ::_thesis: verum
end;
supposeA4: n <> 0 ; ::_thesis: ord h divides n
percases ( ord h = 0 or ord h <> 0 ) ;
suppose ord h = 0 ; ::_thesis: ord h divides n
then h is being_of_order_0 by Def11;
hence ord h divides n by A3, A4, Def10; ::_thesis: verum
end;
supposeA5: ord h <> 0 ; ::_thesis: ord h divides n
then not h is being_of_order_0 by Def11;
then ord h <= n by A3, A4, Def11;
then consider m being Nat such that
A6: n = (ord h) + m by NAT_1:10;
h |^ n = (h |^ (ord h)) * (h |^ m) by A6, Lm5
.= (1_ G) * (h |^ m) by Th41
.= h |^ m by Def4 ;
then ord h divides m by A2, A3, A5, A6, NAT_1:16;
then consider i being Nat such that
A7: m = (ord h) * i by NAT_D:def_3;
n = (ord h) * (1 + i) by A6, A7;
hence ord h divides n by NAT_D:def_3; ::_thesis: verum
end;
end;
end;
end;
end;
for n being Nat holds S1[n] from NAT_1:sch_4(A1);
hence ( h |^ n = 1_ G implies ord h divides n ) ; ::_thesis: verum
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
card the carrier of G in NAT ;
hence card G is Element of NAT ; ::_thesis: verum
end;
end;
theorem :: GROUP_1:45
for G being non empty finite 1-sorted holds card G >= 1
proof
let G be non empty finite 1-sorted ; ::_thesis: card G >= 1
set g = the Element of G;
( { the Element of G} c= the carrier of G & card { the Element of G} = 1 ) by CARD_1:30, ZFMISC_1:31;
hence card G >= 1 by NAT_1:43; ::_thesis: verum
end;
definition
let IT be multMagma ;
attrIT 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
reconsider G0 = multMagma(# REAL,addreal #) as Group by Th3;
take G0 ; ::_thesis: ( G0 is strict & G0 is commutative )
thus G0 is strict ; ::_thesis: G0 is commutative
let a, g be Element of G0; :: according to GROUP_1:def_12 ::_thesis: a * g = g * a
reconsider A = a, B = g as Real ;
thus a * g = B + A by BINOP_2:def_9
.= g * a by BINOP_2:def_9 ; ::_thesis: verum
end;
end;
definition
let FS be non empty commutative multMagma ;
let x, y be Element of FS;
:: original: *
redefine funcx * 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
reconsider G = multMagma(# REAL,addreal #) as Group by Th3;
G is commutative
proof
let h, g be Element of G; :: according to GROUP_1:def_12 ::_thesis: h * g = g * h
reconsider A = h, B = g as Real ;
thus h * g = B + A by BINOP_2:def_9
.= g * h by BINOP_2:def_9 ; ::_thesis: verum
end;
hence multMagma(# REAL,addreal #) is commutative Group ; ::_thesis: verum
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
let A be commutative Group; ::_thesis: ( 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 )
set G = addLoopStr(# the carrier of A, the multF of A,(1_ A) #);
thus addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is Abelian ::_thesis: ( 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
let a, b be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a
reconsider x = a, y = b as Element of A ;
A1: for a, b being Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #)
for x, y being Element of A st a = x & b = y holds
a + b = x * y ;
thus a + b = x * y
.= b + a by A1 ; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_3 ::_thesis: ( 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 )
let a, b, c be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); ::_thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of A ;
thus (a + b) + c = (x * y) * z
.= x * (y * z) by Def3
.= a + (b + c) ; ::_thesis: verum
end;
hereby :: according to RLVECT_1:def_4 ::_thesis: addLoopStr(# the carrier of A, the multF of A,(1_ A) #) is right_complementable
let a be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); ::_thesis: a + (0. addLoopStr(# the carrier of A, the multF of A,(1_ A) #)) = a
reconsider x = a as Element of A ;
thus a + (0. addLoopStr(# the carrier of A, the multF of A,(1_ A) #)) = x * (1_ A)
.= a by Def4 ; ::_thesis: verum
end;
let a be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
reconsider x = a as Element of A ;
reconsider b = (inverse_op A) . x as Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #) ;
take b ; :: according to ALGSTR_0:def_11 ::_thesis: a + b = 0. addLoopStr(# the carrier of A, the multF of A,(1_ A) #)
thus a + b = x * (x ") by Def6
.= 0. addLoopStr(# the carrier of A, the multF of A,(1_ A) #) by Def5 ; ::_thesis: verum
end;
begin
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
let L be non empty unital multMagma ; ::_thesis: for x being Element of L holds (power L) . (x,1) = x
let x be Element of L; ::_thesis: (power L) . (x,1) = x
0 + 1 = 1 ;
hence (power L) . (x,1) = ((power L) . (x,0)) * x by Def7
.= (1_ L) * x by Def7
.= x by Def4 ;
::_thesis: verum
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
let L be non empty unital multMagma ; ::_thesis: for x being Element of L holds (power L) . (x,2) = x * x
let x be Element of L; ::_thesis: (power L) . (x,2) = x * x
1 + 1 = 2 ;
hence (power L) . (x,2) = ((power L) . (x,1)) * x by Def7
.= x * x by Th50 ;
::_thesis: verum
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
let L be non empty unital associative commutative multMagma ; ::_thesis: 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))
let x, y be Element of L; ::_thesis: for n being Element of NAT holds (power L) . ((x * y),n) = ((power L) . (x,n)) * ((power L) . (y,n))
defpred S1[ Element of NAT ] means (power L) . ((x * y),$1) = ((power L) . (x,$1)) * ((power L) . (y,$1));
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; ::_thesis: S1[n + 1]
then (power L) . ((x * y),(n + 1)) = (((power L) . (x,n)) * ((power L) . (y,n))) * (x * y) by Def7
.= ((power L) . (x,n)) * (((power L) . (y,n)) * (x * y)) by Def3
.= ((power L) . (x,n)) * (x * (((power L) . (y,n)) * y)) by Def3
.= ((power L) . (x,n)) * (x * ((power L) . (y,(n + 1)))) by Def7
.= (((power L) . (x,n)) * x) * ((power L) . (y,(n + 1))) by Def3
.= ((power L) . (x,(n + 1))) * ((power L) . (y,(n + 1))) by Def7 ;
hence S1[n + 1] ; ::_thesis: verum
end;
(power L) . ((x * y),0) = 1_ L by Def7
.= (1_ L) * (1_ L) by Def4
.= ((power L) . (x,0)) * (1_ L) by Def7
.= ((power L) . (x,0)) * ((power L) . (y,0)) by Def7 ;
then A2: S1[ 0 ] ;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum
end;
definition
let G, H be multMagma ;
let IT be Function of G,H;
attrIT 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 );