:: GROUP_5 semantic presentation
begin
theorem Th1: :: GROUP_5:1
for x being set
for G being Group holds
( x in (1). G iff x = 1_ G )
proof
let x be set ; ::_thesis: for G being Group holds
( x in (1). G iff x = 1_ G )
let G be Group; ::_thesis: ( x in (1). G iff x = 1_ G )
thus ( x in (1). G implies x = 1_ G ) ::_thesis: ( x = 1_ G implies x in (1). G )
proof
assume x in (1). G ; ::_thesis: x = 1_ G
then x in the carrier of ((1). G) by STRUCT_0:def_5;
then x in {(1_ G)} by GROUP_2:def_7;
hence x = 1_ G by TARSKI:def_1; ::_thesis: verum
end;
thus ( x = 1_ G implies x in (1). G ) by GROUP_2:46; ::_thesis: verum
end;
theorem :: GROUP_5:2
for G being Group
for a, b being Element of G
for H being Subgroup of G st a in H & b in H holds
a |^ b in H
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G st a in H & b in H holds
a |^ b in H
let a, b be Element of G; ::_thesis: for H being Subgroup of G st a in H & b in H holds
a |^ b in H
let H be Subgroup of G; ::_thesis: ( a in H & b in H implies a |^ b in H )
assume ( a in H & b in H ) ; ::_thesis: a |^ b in H
then ( b " in H & a * b in H ) by GROUP_2:50, GROUP_2:51;
then (b ") * (a * b) in H by GROUP_2:50;
hence a |^ b in H by GROUP_1:def_3; ::_thesis: verum
end;
theorem Th3: :: GROUP_5:3
for G being Group
for a, b being Element of G
for N being strict normal Subgroup of G st a in N holds
a |^ b in N
proof
let G be Group; ::_thesis: for a, b being Element of G
for N being strict normal Subgroup of G st a in N holds
a |^ b in N
let a, b be Element of G; ::_thesis: for N being strict normal Subgroup of G st a in N holds
a |^ b in N
let N be strict normal Subgroup of G; ::_thesis: ( a in N implies a |^ b in N )
assume a in N ; ::_thesis: a |^ b in N
then a |^ b in N |^ b by GROUP_3:58;
hence a |^ b in N by GROUP_3:def_13; ::_thesis: verum
end;
theorem Th4: :: GROUP_5:4
for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
proof
let x be set ; ::_thesis: for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds
( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
let H1, H2 be Subgroup of G; ::_thesis: ( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
thus ( x in H1 * H2 implies ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) ) ::_thesis: ( ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) implies x in H1 * H2 )
proof
assume x in H1 * H2 ; ::_thesis: ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 )
then x in (carr H1) * H2 ;
then consider a, b being Element of G such that
A1: x = a * b and
A2: a in carr H1 and
A3: b in H2 by GROUP_2:94;
a in H1 by A2, STRUCT_0:def_5;
hence ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) by A1, A3; ::_thesis: verum
end;
given a, b being Element of G such that A4: ( x = a * b & a in H1 ) and
A5: b in H2 ; ::_thesis: x in H1 * H2
b in carr H2 by A5, STRUCT_0:def_5;
then x in H1 * (carr H2) by A4, GROUP_2:95;
hence x in H1 * H2 ; ::_thesis: verum
end;
theorem Th5: :: GROUP_5:5
for x being set
for G being Group
for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
proof
let x be set ; ::_thesis: for G being Group
for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
let H1, H2 be Subgroup of G; ::_thesis: ( H1 * H2 = H2 * H1 implies ( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) ) )
assume A1: H1 * H2 = H2 * H1 ; ::_thesis: ( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
thus ( x in H1 "\/" H2 implies ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) ) ::_thesis: ( ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) implies x in H1 "\/" H2 )
proof
assume x in H1 "\/" H2 ; ::_thesis: ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 )
then x in the carrier of (H1 "\/" H2) by STRUCT_0:def_5;
then x in H1 * H2 by A1, GROUP_4:51;
hence ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) by Th4; ::_thesis: verum
end;
given a, b being Element of G such that A2: ( x = a * b & a in H1 & b in H2 ) ; ::_thesis: x in H1 "\/" H2
x in H1 * H2 by A2, Th4;
then x in the carrier of (H1 "\/" H2) by A1, GROUP_4:51;
hence x in H1 "\/" H2 by STRUCT_0:def_5; ::_thesis: verum
end;
theorem :: GROUP_5:6
for x being set
for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
proof
let x be set ; ::_thesis: for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
let G be Group; ::_thesis: for H1, H2 being Subgroup of G st G is commutative Group holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
let H1, H2 be Subgroup of G; ::_thesis: ( G is commutative Group implies ( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) ) )
assume G is commutative Group ; ::_thesis: ( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )
then H1 * H2 = H2 * H1 by GROUP_2:25;
hence ( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) ) by Th5; ::_thesis: verum
end;
theorem Th7: :: GROUP_5:7
for x being set
for G being Group
for N1, N2 being strict normal Subgroup of G holds
( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )
proof
let x be set ; ::_thesis: for G being Group
for N1, N2 being strict normal Subgroup of G holds
( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )
let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G holds
( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )
let N1, N2 be strict normal Subgroup of G; ::_thesis: ( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )
N1 * N2 = N2 * N1 by GROUP_3:125;
hence ( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) ) by Th5; ::_thesis: verum
end;
theorem :: GROUP_5:8
for G being Group
for H being Subgroup of G
for N being normal Subgroup of G holds H * N = N * H
proof
let G be Group; ::_thesis: for H being Subgroup of G
for N being normal Subgroup of G holds H * N = N * H
let H be Subgroup of G; ::_thesis: for N being normal Subgroup of G holds H * N = N * H
let N be normal Subgroup of G; ::_thesis: H * N = N * H
thus H * N = (carr H) * N
.= N * (carr H) by GROUP_3:120
.= N * H ; ::_thesis: verum
end;
definition
let G be Group;
let F be FinSequence of the carrier of G;
let a be Element of G;
funcF |^ a -> FinSequence of the carrier of G means :Def1: :: GROUP_5:def 1
( len it = len F & ( for k being Nat st k in dom F holds
it . k = (F /. k) |^ a ) );
existence
ex b1 being FinSequence of the carrier of G st
( len b1 = len F & ( for k being Nat st k in dom F holds
b1 . k = (F /. k) |^ a ) )
proof
deffunc H1( Nat) -> Element of the carrier of G = (F /. $1) |^ a;
consider F1 being FinSequence of the carrier of G such that
A1: ( len F1 = len F & ( for k being Nat st k in dom F1 holds
F1 . k = H1(k) ) ) from FINSEQ_2:sch_1();
dom F1 = dom F by A1, FINSEQ_3:29;
hence ex b1 being FinSequence of the carrier of G st
( len b1 = len F & ( for k being Nat st k in dom F holds
b1 . k = (F /. k) |^ a ) ) by A1; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being FinSequence of the carrier of G st len b1 = len F & ( for k being Nat st k in dom F holds
b1 . k = (F /. k) |^ a ) & len b2 = len F & ( for k being Nat st k in dom F holds
b2 . k = (F /. k) |^ a ) holds
b1 = b2;
proof
let F1, F2 be FinSequence of the carrier of G; ::_thesis: ( len F1 = len F & ( for k being Nat st k in dom F holds
F1 . k = (F /. k) |^ a ) & len F2 = len F & ( for k being Nat st k in dom F holds
F2 . k = (F /. k) |^ a ) implies F1 = F2 )
assume that
A2: len F1 = len F and
A3: for k being Nat st k in dom F holds
F1 . k = (F /. k) |^ a and
A4: len F2 = len F and
A5: for k being Nat st k in dom F holds
F2 . k = (F /. k) |^ a ; ::_thesis: F1 = F2
A6: dom F1 = Seg (len F) by A2, FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_F1_holds_
F1_._k_=_F2_._k
let k be Nat; ::_thesis: ( k in dom F1 implies F1 . k = F2 . k )
assume k in dom F1 ; ::_thesis: F1 . k = F2 . k
then A7: k in dom F by A6, FINSEQ_1:def_3;
hence F1 . k = (F /. k) |^ a by A3
.= F2 . k by A5, A7 ;
::_thesis: verum
end;
hence F1 = F2 by A2, A4, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines |^ GROUP_5:def_1_:_
for G being Group
for F being FinSequence of the carrier of G
for a being Element of G
for b4 being FinSequence of the carrier of G holds
( b4 = F |^ a iff ( len b4 = len F & ( for k being Nat st k in dom F holds
b4 . k = (F /. k) |^ a ) ) );
theorem Th9: :: GROUP_5:9
for G being Group
for a being Element of G
for F1, F2 being FinSequence of the carrier of G holds (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a
proof
let G be Group; ::_thesis: for a being Element of G
for F1, F2 being FinSequence of the carrier of G holds (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a
let a be Element of G; ::_thesis: for F1, F2 being FinSequence of the carrier of G holds (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a
let F1, F2 be FinSequence of the carrier of G; ::_thesis: (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(F1_|^_a)_holds_
(F1_|^_a)_._k_=_((F1_^_F2)_|^_a)_._k
let k be Element of NAT ; ::_thesis: ( k in dom (F1 |^ a) implies (F1 |^ a) . k = ((F1 ^ F2) |^ a) . k )
assume k in dom (F1 |^ a) ; ::_thesis: (F1 |^ a) . k = ((F1 ^ F2) |^ a) . k
then k in Seg (len (F1 |^ a)) by FINSEQ_1:def_3;
then k in Seg (len F1) by Def1;
then A2: k in dom F1 by FINSEQ_1:def_3;
then A3: ( F1 /. k = (F1 ^ F2) /. k & k in dom (F1 ^ F2) ) by FINSEQ_3:22, FINSEQ_4:68;
thus (F1 |^ a) . k = (F1 /. k) |^ a by A2, Def1
.= ((F1 ^ F2) |^ a) . k by A3, Def1 ; ::_thesis: verum
end;
A4: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(F2_|^_a)_holds_
((F1_^_F2)_|^_a)_._((len_(F1_|^_a))_+_k)_=_(F2_|^_a)_._k
let k be Element of NAT ; ::_thesis: ( k in dom (F2 |^ a) implies ((F1 ^ F2) |^ a) . ((len (F1 |^ a)) + k) = (F2 |^ a) . k )
assume A5: k in dom (F2 |^ a) ; ::_thesis: ((F1 ^ F2) |^ a) . ((len (F1 |^ a)) + k) = (F2 |^ a) . k
len F2 = len (F2 |^ a) by Def1;
then A6: k in dom F2 by A5, FINSEQ_3:29;
then (len F1) + k in dom (F1 ^ F2) by FINSEQ_1:28;
then (len (F1 |^ a)) + k in dom (F1 ^ F2) by Def1;
hence ((F1 ^ F2) |^ a) . ((len (F1 |^ a)) + k) = ((F1 ^ F2) /. ((len (F1 |^ a)) + k)) |^ a by Def1
.= ((F1 ^ F2) /. ((len F1) + k)) |^ a by Def1
.= (F2 /. k) |^ a by A6, FINSEQ_4:69
.= (F2 |^ a) . k by A6, Def1 ;
::_thesis: verum
end;
(len (F1 |^ a)) + (len (F2 |^ a)) = (len F1) + (len (F2 |^ a)) by Def1
.= (len F1) + (len F2) by Def1
.= len (F1 ^ F2) by FINSEQ_1:22
.= len ((F1 ^ F2) |^ a) by Def1 ;
hence (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a by A1, A4, FINSEQ_3:38; ::_thesis: verum
end;
theorem Th10: :: GROUP_5:10
for G being Group
for a being Element of G holds (<*> the carrier of G) |^ a = {}
proof
let G be Group; ::_thesis: for a being Element of G holds (<*> the carrier of G) |^ a = {}
let a be Element of G; ::_thesis: (<*> the carrier of G) |^ a = {}
len ((<*> the carrier of G) |^ a) = len (<*> the carrier of G) by Def1
.= 0 ;
hence (<*> the carrier of G) |^ a = {} ; ::_thesis: verum
end;
theorem Th11: :: GROUP_5:11
for G being Group
for a, b being Element of G holds <*a*> |^ b = <*(a |^ b)*>
proof
let G be Group; ::_thesis: for a, b being Element of G holds <*a*> |^ b = <*(a |^ b)*>
let a, b be Element of G; ::_thesis: <*a*> |^ b = <*(a |^ b)*>
A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<*a*>_holds_
<*(a_|^_b)*>_._k_=_(<*a*>_/._k)_|^_b
let k be Nat; ::_thesis: ( k in dom <*a*> implies <*(a |^ b)*> . k = (<*a*> /. k) |^ b )
assume k in dom <*a*> ; ::_thesis: <*(a |^ b)*> . k = (<*a*> /. k) |^ b
then k in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A2: k = 1 by TARSKI:def_1;
hence <*(a |^ b)*> . k = a |^ b by FINSEQ_1:40
.= (<*a*> /. k) |^ b by A2, FINSEQ_4:16 ;
::_thesis: verum
end;
len <*(a |^ b)*> = 1 by FINSEQ_1:40
.= len <*a*> by FINSEQ_1:39 ;
hence <*a*> |^ b = <*(a |^ b)*> by A1, Def1; ::_thesis: verum
end;
theorem Th12: :: GROUP_5:12
for G being Group
for a, b, c being Element of G holds <*a,b*> |^ c = <*(a |^ c),(b |^ c)*>
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds <*a,b*> |^ c = <*(a |^ c),(b |^ c)*>
let a, b, c be Element of G; ::_thesis: <*a,b*> |^ c = <*(a |^ c),(b |^ c)*>
thus <*a,b*> |^ c = (<*a*> ^ <*b*>) |^ c by FINSEQ_1:def_9
.= (<*a*> |^ c) ^ (<*b*> |^ c) by Th9
.= <*(a |^ c)*> ^ (<*b*> |^ c) by Th11
.= <*(a |^ c)*> ^ <*(b |^ c)*> by Th11
.= <*(a |^ c),(b |^ c)*> by FINSEQ_1:def_9 ; ::_thesis: verum
end;
theorem :: GROUP_5:13
for G being Group
for a, b, c, d being Element of G holds <*a,b,c*> |^ d = <*(a |^ d),(b |^ d),(c |^ d)*>
proof
let G be Group; ::_thesis: for a, b, c, d being Element of G holds <*a,b,c*> |^ d = <*(a |^ d),(b |^ d),(c |^ d)*>
let a, b, c, d be Element of G; ::_thesis: <*a,b,c*> |^ d = <*(a |^ d),(b |^ d),(c |^ d)*>
thus <*a,b,c*> |^ d = (<*a*> ^ <*b,c*>) |^ d by FINSEQ_1:43
.= (<*a*> |^ d) ^ (<*b,c*> |^ d) by Th9
.= (<*a*> |^ d) ^ <*(b |^ d),(c |^ d)*> by Th12
.= <*(a |^ d)*> ^ <*(b |^ d),(c |^ d)*> by Th11
.= <*(a |^ d),(b |^ d),(c |^ d)*> by FINSEQ_1:43 ; ::_thesis: verum
end;
theorem Th14: :: GROUP_5:14
for G being Group
for a being Element of G
for F being FinSequence of the carrier of G holds Product (F |^ a) = (Product F) |^ a
proof
let G be Group; ::_thesis: for a being Element of G
for F being FinSequence of the carrier of G holds Product (F |^ a) = (Product F) |^ a
let a be Element of G; ::_thesis: for F being FinSequence of the carrier of G holds Product (F |^ a) = (Product F) |^ a
let F be FinSequence of the carrier of G; ::_thesis: Product (F |^ a) = (Product F) |^ a
defpred S1[ FinSequence of the carrier of G] means Product ($1 |^ a) = (Product $1) |^ a;
A1: now__::_thesis:_for_F_being_FinSequence_of_the_carrier_of_G
for_b_being_Element_of_G_st_S1[F]_holds_
S1[F_^_<*b*>]
let F be FinSequence of the carrier of G; ::_thesis: for b being Element of G st S1[F] holds
S1[F ^ <*b*>]
let b be Element of G; ::_thesis: ( S1[F] implies S1[F ^ <*b*>] )
assume A2: S1[F] ; ::_thesis: S1[F ^ <*b*>]
Product ((F ^ <*b*>) |^ a) = Product ((F |^ a) ^ (<*b*> |^ a)) by Th9
.= ((Product F) |^ a) * (Product (<*b*> |^ a)) by A2, GROUP_4:5
.= ((Product F) |^ a) * (Product <*(b |^ a)*>) by Th11
.= ((Product F) |^ a) * (b |^ a) by FINSOP_1:11
.= ((Product F) * b) |^ a by GROUP_3:23
.= (Product (F ^ <*b*>)) |^ a by GROUP_4:6 ;
hence S1[F ^ <*b*>] ; ::_thesis: verum
end;
A3: S1[ <*> the carrier of G]
proof
set p = <*> the carrier of G;
thus Product ((<*> the carrier of G) |^ a) = Product (<*> the carrier of G) by Th10
.= 1_ G by GROUP_4:8
.= (1_ G) |^ a by GROUP_3:17
.= (Product (<*> the carrier of G)) |^ a by GROUP_4:8 ; ::_thesis: verum
end;
for F being FinSequence of the carrier of G holds S1[F] from FINSEQ_2:sch_2(A3, A1);
hence Product (F |^ a) = (Product F) |^ a ; ::_thesis: verum
end;
theorem Th15: :: GROUP_5:15
for G being Group
for a being Element of G
for F being FinSequence of the carrier of G
for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a
proof
let G be Group; ::_thesis: for a being Element of G
for F being FinSequence of the carrier of G
for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a
let a be Element of G; ::_thesis: for F being FinSequence of the carrier of G
for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a
let F be FinSequence of the carrier of G; ::_thesis: for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a
let I be FinSequence of INT ; ::_thesis: (F |^ a) |^ I = (F |^ I) |^ a
len (F |^ I) = len F by GROUP_4:def_3;
then A1: dom (F |^ I) = dom F by FINSEQ_3:29;
A2: len (F |^ a) = len F by Def1;
then A3: dom (F |^ a) = dom F by FINSEQ_3:29;
A4: len ((F |^ a) |^ I) = len (F |^ a) by GROUP_4:def_3;
then A5: dom ((F |^ a) |^ I) = Seg (len F) by A2, FINSEQ_1:def_3;
A6: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((F_|^_a)_|^_I)_holds_
((F_|^_a)_|^_I)_._k_=_((F_|^_I)_|^_a)_._k
let k be Nat; ::_thesis: ( k in dom ((F |^ a) |^ I) implies ((F |^ a) |^ I) . k = ((F |^ I) |^ a) . k )
assume k in dom ((F |^ a) |^ I) ; ::_thesis: ((F |^ a) |^ I) . k = ((F |^ I) |^ a) . k
then A7: k in dom F by A5, FINSEQ_1:def_3;
then A8: (F |^ a) /. k = (F |^ a) . k by A3, PARTFUN1:def_6;
A9: (F |^ I) /. k = (F |^ I) . k by A1, A7, PARTFUN1:def_6;
thus ((F |^ a) |^ I) . k = ((F |^ a) /. k) |^ (@ (I /. k)) by A3, A7, GROUP_4:def_3
.= ((F /. k) |^ a) |^ (@ (I /. k)) by A7, A8, Def1
.= ((F /. k) |^ (@ (I /. k))) |^ a by GROUP_3:28
.= ((F |^ I) /. k) |^ a by A7, A9, GROUP_4:def_3
.= ((F |^ I) |^ a) . k by A1, A7, Def1 ; ::_thesis: verum
end;
len ((F |^ I) |^ a) = len (F |^ I) by Def1
.= len F by GROUP_4:def_3 ;
hence (F |^ a) |^ I = (F |^ I) |^ a by A2, A4, A6, FINSEQ_2:9; ::_thesis: verum
end;
begin
definition
let G be Group;
let a, b be Element of G;
func[.a,b.] -> Element of G equals :: GROUP_5:def 2
(((a ") * (b ")) * a) * b;
correctness
coherence
(((a ") * (b ")) * a) * b is Element of G;
;
end;
:: deftheorem defines [. GROUP_5:def_2_:_
for G being Group
for a, b being Element of G holds [.a,b.] = (((a ") * (b ")) * a) * b;
theorem Th16: :: GROUP_5:16
for G being Group
for a, b being Element of G holds
( [.a,b.] = (((a ") * (b ")) * a) * b & [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
proof
let G be Group; ::_thesis: for a, b being Element of G holds
( [.a,b.] = (((a ") * (b ")) * a) * b & [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
let a, b be Element of G; ::_thesis: ( [.a,b.] = (((a ") * (b ")) * a) * b & [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
thus [.a,b.] = (((a ") * (b ")) * a) * b ; ::_thesis: ( [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
thus [.a,b.] = ((a ") * ((b ") * a)) * b by GROUP_1:def_3; ::_thesis: ( [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
hence [.a,b.] = (a ") * (((b ") * a) * b) by GROUP_1:def_3; ::_thesis: ( [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
hence [.a,b.] = (a ") * ((b ") * (a * b)) by GROUP_1:def_3; ::_thesis: [.a,b.] = ((a ") * (b ")) * (a * b)
thus [.a,b.] = ((a ") * (b ")) * (a * b) by GROUP_1:def_3; ::_thesis: verum
end;
theorem Th17: :: GROUP_5:17
for G being Group
for a, b being Element of G holds [.a,b.] = ((b * a) ") * (a * b)
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,b.] = ((b * a) ") * (a * b)
let a, b be Element of G; ::_thesis: [.a,b.] = ((b * a) ") * (a * b)
thus [.a,b.] = ((a ") * (b ")) * (a * b) by Th16
.= ((b * a) ") * (a * b) by GROUP_1:17 ; ::_thesis: verum
end;
theorem :: GROUP_5:18
for G being Group
for a, b being Element of G holds
( [.a,b.] = ((b ") |^ a) * b & [.a,b.] = (a ") * (a |^ b) ) by Th16;
theorem Th19: :: GROUP_5:19
for G being Group
for a being Element of G holds
( [.(1_ G),a.] = 1_ G & [.a,(1_ G).] = 1_ G )
proof
let G be Group; ::_thesis: for a being Element of G holds
( [.(1_ G),a.] = 1_ G & [.a,(1_ G).] = 1_ G )
let a be Element of G; ::_thesis: ( [.(1_ G),a.] = 1_ G & [.a,(1_ G).] = 1_ G )
thus [.(1_ G),a.] = (((1_ G) ") * (a ")) * a by GROUP_1:def_4
.= ((1_ G) * (a ")) * a by GROUP_1:8
.= (a ") * a by GROUP_1:def_4
.= 1_ G by GROUP_1:def_5 ; ::_thesis: [.a,(1_ G).] = 1_ G
thus [.a,(1_ G).] = ((a ") * ((1_ G) ")) * a by GROUP_1:def_4
.= ((a ") * (1_ G)) * a by GROUP_1:8
.= (a ") * a by GROUP_1:def_4
.= 1_ G by GROUP_1:def_5 ; ::_thesis: verum
end;
theorem Th20: :: GROUP_5:20
for G being Group
for a being Element of G holds [.a,a.] = 1_ G
proof
let G be Group; ::_thesis: for a being Element of G holds [.a,a.] = 1_ G
let a be Element of G; ::_thesis: [.a,a.] = 1_ G
thus [.a,a.] = ((a * a) ") * (a * a) by Th17
.= 1_ G by GROUP_1:def_5 ; ::_thesis: verum
end;
theorem :: GROUP_5:21
for G being Group
for a being Element of G holds
( [.a,(a ").] = 1_ G & [.(a "),a.] = 1_ G )
proof
let G be Group; ::_thesis: for a being Element of G holds
( [.a,(a ").] = 1_ G & [.(a "),a.] = 1_ G )
let a be Element of G; ::_thesis: ( [.a,(a ").] = 1_ G & [.(a "),a.] = 1_ G )
thus [.a,(a ").] = ((a ") * ((a ") ")) * (a * (a ")) by Th16
.= (1_ G) * (a * (a ")) by GROUP_1:def_5
.= a * (a ") by GROUP_1:def_4
.= 1_ G by GROUP_1:def_5 ; ::_thesis: [.(a "),a.] = 1_ G
thus [.(a "),a.] = (((a ") ") * (a ")) * ((a ") * a) by Th16
.= (((a ") ") * (a ")) * (1_ G) by GROUP_1:def_5
.= ((a ") ") * (a ") by GROUP_1:def_4
.= 1_ G by GROUP_1:def_5 ; ::_thesis: verum
end;
theorem Th22: :: GROUP_5:22
for G being Group
for a, b being Element of G holds [.a,b.] " = [.b,a.]
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,b.] " = [.b,a.]
let a, b be Element of G; ::_thesis: [.a,b.] " = [.b,a.]
thus [.a,b.] " = (((a ") * (b ")) * (a * b)) " by Th16
.= ((a * b) ") * (((a ") * (b ")) ") by GROUP_1:17
.= ((b ") * (a ")) * (((a ") * (b ")) ") by GROUP_1:17
.= ((b ") * (a ")) * (((b ") ") * ((a ") ")) by GROUP_1:17
.= ((b ") * (a ")) * (((b ") ") * a)
.= ((b ") * (a ")) * (b * a)
.= [.b,a.] by Th16 ; ::_thesis: verum
end;
theorem Th23: :: GROUP_5:23
for G being Group
for a, b, c being Element of G holds [.a,b.] |^ c = [.(a |^ c),(b |^ c).]
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds [.a,b.] |^ c = [.(a |^ c),(b |^ c).]
let a, b, c be Element of G; ::_thesis: [.a,b.] |^ c = [.(a |^ c),(b |^ c).]
thus [.a,b.] |^ c = ((c ") * (((((a ") * (1_ G)) * (b ")) * a) * b)) * c by GROUP_1:def_4
.= ((c ") * (((((a ") * (c * (c "))) * (b ")) * a) * b)) * c by GROUP_1:def_5
.= ((c ") * ((((a ") * (c * (c "))) * (b ")) * (a * b))) * c by GROUP_1:def_3
.= ((c ") * (((a ") * (c * (c "))) * ((b ") * (a * b)))) * c by GROUP_1:def_3
.= ((c ") * ((a ") * ((c * (c ")) * ((b ") * (a * b))))) * c by GROUP_1:def_3
.= (((c ") * (a ")) * ((c * (c ")) * ((b ") * (a * b)))) * c by GROUP_1:def_3
.= (((c ") * (a ")) * (c * ((c ") * ((b ") * (a * b))))) * c by GROUP_1:def_3
.= (((a ") |^ c) * ((c ") * ((b ") * (a * b)))) * c by GROUP_1:def_3
.= (((a |^ c) ") * ((c ") * ((b ") * (a * b)))) * c by GROUP_3:26
.= (((a |^ c) ") * ((c ") * (((b ") * (1_ G)) * (a * b)))) * c by GROUP_1:def_4
.= (((a |^ c) ") * ((c ") * (((b ") * (c * (c "))) * (a * b)))) * c by GROUP_1:def_5
.= (((a |^ c) ") * ((c ") * ((b ") * ((c * (c ")) * (a * b))))) * c by GROUP_1:def_3
.= (((a |^ c) ") * (((c ") * (b ")) * ((c * (c ")) * (a * b)))) * c by GROUP_1:def_3
.= (((a |^ c) ") * (((c ") * (b ")) * (c * ((c ") * (a * b))))) * c by GROUP_1:def_3
.= (((a |^ c) ") * (((b ") |^ c) * ((c ") * (a * b)))) * c by GROUP_1:def_3
.= (((a |^ c) ") * (((b |^ c) ") * ((c ") * (a * b)))) * c by GROUP_3:26
.= (((a |^ c) ") * (((b |^ c) ") * ((c ") * ((a * (1_ G)) * b)))) * c by GROUP_1:def_4
.= (((a |^ c) ") * (((b |^ c) ") * ((c ") * ((a * (c * (c "))) * b)))) * c by GROUP_1:def_5
.= (((a |^ c) ") * (((b |^ c) ") * ((c ") * (a * ((c * (c ")) * b))))) * c by GROUP_1:def_3
.= (((a |^ c) ") * (((b |^ c) ") * (((c ") * a) * ((c * (c ")) * b)))) * c by GROUP_1:def_3
.= (((a |^ c) ") * (((b |^ c) ") * (((c ") * a) * (c * ((c ") * b))))) * c by GROUP_1:def_3
.= (((a |^ c) ") * (((b |^ c) ") * ((a |^ c) * ((c ") * b)))) * c by GROUP_1:def_3
.= ((a |^ c) ") * ((((b |^ c) ") * ((a |^ c) * ((c ") * b))) * c) by GROUP_1:def_3
.= ((a |^ c) ") * (((b |^ c) ") * (((a |^ c) * ((c ") * b)) * c)) by GROUP_1:def_3
.= ((a |^ c) ") * (((b |^ c) ") * ((a |^ c) * (b |^ c))) by GROUP_1:def_3
.= [.(a |^ c),(b |^ c).] by Th16 ; ::_thesis: verum
end;
theorem :: GROUP_5:24
for G being Group
for a, b being Element of G holds [.a,b.] = (((a ") |^ 2) * ((a * (b ")) |^ 2)) * (b |^ 2)
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,b.] = (((a ") |^ 2) * ((a * (b ")) |^ 2)) * (b |^ 2)
let a, b be Element of G; ::_thesis: [.a,b.] = (((a ") |^ 2) * ((a * (b ")) |^ 2)) * (b |^ 2)
thus [.a,b.] = ((a ") * (b ")) * (a * b) by Th16
.= (((a ") * (1_ G)) * (b ")) * (a * b) by GROUP_1:def_4
.= (((a ") * (1_ G)) * (b ")) * ((a * (1_ G)) * b) by GROUP_1:def_4
.= (((a ") * ((a ") * a)) * (b ")) * ((a * (1_ G)) * b) by GROUP_1:def_5
.= (((a ") * ((a ") * a)) * (b ")) * ((a * ((b ") * b)) * b) by GROUP_1:def_5
.= ((((a ") * (a ")) * a) * (b ")) * ((a * ((b ") * b)) * b) by GROUP_1:def_3
.= ((((a ") |^ 2) * a) * (b ")) * ((a * ((b ") * b)) * b) by GROUP_1:27
.= ((((a ") |^ 2) * a) * (b ")) * (a * (((b ") * b) * b)) by GROUP_1:def_3
.= ((((a ") |^ 2) * a) * (b ")) * (a * ((b ") * (b * b))) by GROUP_1:def_3
.= ((((a ") |^ 2) * a) * (b ")) * (a * ((b ") * (b |^ 2))) by GROUP_1:27
.= (((a ") |^ 2) * (a * (b "))) * (a * ((b ") * (b |^ 2))) by GROUP_1:def_3
.= ((a ") |^ 2) * ((a * (b ")) * (a * ((b ") * (b |^ 2)))) by GROUP_1:def_3
.= ((a ") |^ 2) * ((a * (b ")) * ((a * (b ")) * (b |^ 2))) by GROUP_1:def_3
.= ((a ") |^ 2) * (((a * (b ")) * (a * (b "))) * (b |^ 2)) by GROUP_1:def_3
.= (((a ") |^ 2) * ((a * (b ")) * (a * (b ")))) * (b |^ 2) by GROUP_1:def_3
.= (((a ") |^ 2) * ((a * (b ")) |^ 2)) * (b |^ 2) by GROUP_1:27 ; ::_thesis: verum
end;
theorem Th25: :: GROUP_5:25
for G being Group
for a, b, c being Element of G holds [.(a * b),c.] = ([.a,c.] |^ b) * [.b,c.]
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds [.(a * b),c.] = ([.a,c.] |^ b) * [.b,c.]
let a, b, c be Element of G; ::_thesis: [.(a * b),c.] = ([.a,c.] |^ b) * [.b,c.]
thus [.(a * b),c.] = (((a * b) ") * (c ")) * ((a * b) * c) by Th16
.= (((b ") * (a ")) * (c ")) * ((a * b) * c) by GROUP_1:17
.= (((b ") * (a ")) * (c ")) * (((a * (1_ G)) * b) * c) by GROUP_1:def_4
.= (((b ") * (a ")) * (c ")) * (((a * (c * (c "))) * b) * c) by GROUP_1:def_5
.= (((b ") * (a ")) * (c ")) * (((a * ((c * (1_ G)) * (c "))) * b) * c) by GROUP_1:def_4
.= (((b ") * (a ")) * (c ")) * (((a * ((c * (b * (b "))) * (c "))) * b) * c) by GROUP_1:def_5
.= ((b ") * ((a ") * (c "))) * (((a * ((c * (b * (b "))) * (c "))) * b) * c) by GROUP_1:def_3
.= ((b ") * ((a ") * (c "))) * ((a * ((c * (b * (b "))) * (c "))) * (b * c)) by GROUP_1:def_3
.= ((b ") * ((a ") * (c "))) * ((a * (((c * b) * (b ")) * (c "))) * (b * c)) by GROUP_1:def_3
.= ((b ") * ((a ") * (c "))) * ((a * ((c * b) * ((b ") * (c ")))) * (b * c)) by GROUP_1:def_3
.= ((b ") * ((a ") * (c "))) * ((a * (c * (b * ((b ") * (c "))))) * (b * c)) by GROUP_1:def_3
.= ((b ") * ((a ") * (c "))) * (((a * c) * (b * ((b ") * (c ")))) * (b * c)) by GROUP_1:def_3
.= ((b ") * ((a ") * (c "))) * ((a * c) * ((b * ((b ") * (c "))) * (b * c))) by GROUP_1:def_3
.= (((b ") * ((a ") * (c "))) * (a * c)) * ((b * ((b ") * (c "))) * (b * c)) by GROUP_1:def_3
.= ((b ") * (((a ") * (c ")) * (a * c))) * ((b * ((b ") * (c "))) * (b * c)) by GROUP_1:def_3
.= ((b ") * (((a ") * (c ")) * (a * c))) * (b * (((b ") * (c ")) * (b * c))) by GROUP_1:def_3
.= (((b ") * (((a ") * (c ")) * (a * c))) * b) * (((b ") * (c ")) * (b * c)) by GROUP_1:def_3
.= ([.a,c.] |^ b) * (((b ") * (c ")) * (b * c)) by Th16
.= ([.a,c.] |^ b) * [.b,c.] by Th16 ; ::_thesis: verum
end;
theorem :: GROUP_5:26
for G being Group
for a, b, c being Element of G holds [.a,(b * c).] = [.a,c.] * ([.a,b.] |^ c)
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds [.a,(b * c).] = [.a,c.] * ([.a,b.] |^ c)
let a, b, c be Element of G; ::_thesis: [.a,(b * c).] = [.a,c.] * ([.a,b.] |^ c)
thus [.a,(b * c).] = ((a ") * ((b * c) ")) * (a * (b * c)) by Th16
.= ((a ") * ((c ") * (b "))) * (a * (b * c)) by GROUP_1:17
.= ((a ") * (((c ") * (1_ G)) * (b "))) * (a * (b * c)) by GROUP_1:def_4
.= ((a ") * (((c ") * (a * (a "))) * (b "))) * (a * (b * c)) by GROUP_1:def_5
.= ((a ") * (((c ") * ((a * (1_ G)) * (a "))) * (b "))) * (a * (b * c)) by GROUP_1:def_4
.= ((a ") * (((c ") * ((a * (c * (c "))) * (a "))) * (b "))) * (a * (b * c)) by GROUP_1:def_5
.= ((a ") * (((c ") * (((a * c) * (c ")) * (a "))) * (b "))) * (a * (b * c)) by GROUP_1:def_3
.= ((a ") * (((c ") * ((a * c) * ((c ") * (a ")))) * (b "))) * (a * (b * c)) by GROUP_1:def_3
.= ((a ") * ((c ") * (((a * c) * ((c ") * (a "))) * (b ")))) * (a * (b * c)) by GROUP_1:def_3
.= (((a ") * (c ")) * (((a * c) * ((c ") * (a "))) * (b "))) * (a * (b * c)) by GROUP_1:def_3
.= ((((a ") * (c ")) * ((a * c) * ((c ") * (a ")))) * (b ")) * (a * (b * c)) by GROUP_1:def_3
.= (((((a ") * (c ")) * (a * c)) * ((c ") * (a "))) * (b ")) * (a * (b * c)) by GROUP_1:def_3
.= ((((a ") * (c ")) * (a * c)) * (((c ") * (a ")) * (b "))) * (a * (b * c)) by GROUP_1:def_3
.= (((a ") * (c ")) * (a * c)) * ((((c ") * (a ")) * (b ")) * (a * (b * c))) by GROUP_1:def_3
.= (((a ") * (c ")) * (a * c)) * ((((c ") * (a ")) * (b ")) * ((a * b) * c)) by GROUP_1:def_3
.= (((a ") * (c ")) * (a * c)) * (((c ") * ((a ") * (b "))) * ((a * b) * c)) by GROUP_1:def_3
.= (((a ") * (c ")) * (a * c)) * ((c ") * (((a ") * (b ")) * ((a * b) * c))) by GROUP_1:def_3
.= (((a ") * (c ")) * (a * c)) * ((c ") * ((((a ") * (b ")) * (a * b)) * c)) by GROUP_1:def_3
.= (((a ") * (c ")) * (a * c)) * (((c ") * (((a ") * (b ")) * (a * b))) * c) by GROUP_1:def_3
.= [.a,c.] * (((c ") * (((a ") * (b ")) * (a * b))) * c) by Th16
.= [.a,c.] * ([.a,b.] |^ c) by Th16 ; ::_thesis: verum
end;
theorem Th27: :: GROUP_5:27
for G being Group
for a, b being Element of G holds [.(a "),b.] = [.b,a.] |^ (a ")
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.(a "),b.] = [.b,a.] |^ (a ")
let a, b be Element of G; ::_thesis: [.(a "),b.] = [.b,a.] |^ (a ")
thus [.(a "),b.] = ((a ") ") * ((b ") * ((a ") * b)) by Th16
.= (((a ") ") * ((b ") * ((a ") * b))) * (1_ G) by GROUP_1:def_4
.= (((a ") ") * ((b ") * ((a ") * b))) * (a * (a ")) by GROUP_1:def_5
.= ((((a ") ") * ((b ") * ((a ") * b))) * a) * (a ") by GROUP_1:def_3
.= (((a ") ") * (((b ") * ((a ") * b)) * a)) * (a ") by GROUP_1:def_3
.= [.b,a.] |^ (a ") by Th16 ; ::_thesis: verum
end;
theorem Th28: :: GROUP_5:28
for G being Group
for a, b being Element of G holds [.a,(b ").] = [.b,a.] |^ (b ")
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,(b ").] = [.b,a.] |^ (b ")
let a, b be Element of G; ::_thesis: [.a,(b ").] = [.b,a.] |^ (b ")
thus [.a,(b ").] = (((a ") * b) * a) * (b ")
.= (1_ G) * ((((a ") * b) * a) * (b ")) by GROUP_1:def_4
.= (((b ") ") * (b ")) * ((((a ") * b) * a) * (b ")) by GROUP_1:def_5
.= ((((b ") ") * (b ")) * (((a ") * b) * a)) * (b ") by GROUP_1:def_3
.= (((b ") ") * ((b ") * (((a ") * b) * a))) * (b ") by GROUP_1:def_3
.= [.b,a.] |^ (b ") by Th16 ; ::_thesis: verum
end;
theorem :: GROUP_5:29
for G being Group
for a, b being Element of G holds
( [.(a "),(b ").] = [.a,b.] |^ ((a * b) ") & [.(a "),(b ").] = [.a,b.] |^ ((b * a) ") )
proof
let G be Group; ::_thesis: for a, b being Element of G holds
( [.(a "),(b ").] = [.a,b.] |^ ((a * b) ") & [.(a "),(b ").] = [.a,b.] |^ ((b * a) ") )
let a, b be Element of G; ::_thesis: ( [.(a "),(b ").] = [.a,b.] |^ ((a * b) ") & [.(a "),(b ").] = [.a,b.] |^ ((b * a) ") )
thus [.(a "),(b ").] = [.(b "),a.] |^ (a ") by Th27
.= ([.a,b.] |^ (b ")) |^ (a ") by Th27
.= [.a,b.] |^ ((b ") * (a ")) by GROUP_3:24
.= [.a,b.] |^ ((a * b) ") by GROUP_1:17 ; ::_thesis: [.(a "),(b ").] = [.a,b.] |^ ((b * a) ")
thus [.(a "),(b ").] = [.b,(a ").] |^ (b ") by Th28
.= ([.a,b.] |^ (a ")) |^ (b ") by Th28
.= [.a,b.] |^ ((a ") * (b ")) by GROUP_3:24
.= [.a,b.] |^ ((b * a) ") by GROUP_1:17 ; ::_thesis: verum
end;
theorem :: GROUP_5:30
for G being Group
for a, b being Element of G holds [.a,(b |^ (a ")).] = [.b,(a ").]
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,(b |^ (a ")).] = [.b,(a ").]
let a, b be Element of G; ::_thesis: [.a,(b |^ (a ")).] = [.b,(a ").]
thus [.a,(b |^ (a ")).] = (((a ") * ((b ") |^ (a "))) * a) * (b |^ (a ")) by GROUP_3:26
.= (((a ") * (((a ") ") * ((b ") * (a ")))) * a) * (b |^ (a ")) by GROUP_1:def_3
.= (((b ") * (a ")) * a) * (b |^ (a ")) by GROUP_3:1
.= (b ") * ((((a ") ") * b) * (a ")) by GROUP_3:1
.= [.b,(a ").] by Th16 ; ::_thesis: verum
end;
theorem :: GROUP_5:31
for G being Group
for a, b being Element of G holds [.(a |^ (b ")),b.] = [.(b "),a.]
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.(a |^ (b ")),b.] = [.(b "),a.]
let a, b be Element of G; ::_thesis: [.(a |^ (b ")),b.] = [.(b "),a.]
thus [.(a |^ (b ")),b.] = ((((a ") |^ (b ")) * (b ")) * (a |^ (b "))) * b by GROUP_3:26
.= (((a ") |^ (b ")) * ((b ") * ((((b ") ") * a) * (b ")))) * b by GROUP_1:def_3
.= (((a ") |^ (b ")) * ((b ") * (((b ") ") * (a * (b "))))) * b by GROUP_1:def_3
.= (((a ") |^ (b ")) * (a * (b "))) * b by GROUP_3:1
.= ((a ") |^ (b ")) * ((a * (b ")) * b) by GROUP_1:def_3
.= [.(b "),a.] by GROUP_3:1 ; ::_thesis: verum
end;
theorem :: GROUP_5:32
for n being Element of NAT
for G being Group
for a, b being Element of G holds [.(a |^ n),b.] = (a |^ (- n)) * ((a |^ b) |^ n)
proof
let n be Element of NAT ; ::_thesis: for G being Group
for a, b being Element of G holds [.(a |^ n),b.] = (a |^ (- n)) * ((a |^ b) |^ n)
let G be Group; ::_thesis: for a, b being Element of G holds [.(a |^ n),b.] = (a |^ (- n)) * ((a |^ b) |^ n)
let a, b be Element of G; ::_thesis: [.(a |^ n),b.] = (a |^ (- n)) * ((a |^ b) |^ n)
thus [.(a |^ n),b.] = ((a |^ n) ") * (((b ") * (a |^ n)) * b) by Th16
.= (a |^ (- n)) * ((a |^ n) |^ b) by GROUP_1:36
.= (a |^ (- n)) * ((a |^ b) |^ n) by GROUP_3:27 ; ::_thesis: verum
end;
theorem :: GROUP_5:33
for n being Element of NAT
for G being Group
for a, b being Element of G holds [.a,(b |^ n).] = ((b |^ a) |^ (- n)) * (b |^ n)
proof
let n be Element of NAT ; ::_thesis: for G being Group
for a, b being Element of G holds [.a,(b |^ n).] = ((b |^ a) |^ (- n)) * (b |^ n)
let G be Group; ::_thesis: for a, b being Element of G holds [.a,(b |^ n).] = ((b |^ a) |^ (- n)) * (b |^ n)
let a, b be Element of G; ::_thesis: [.a,(b |^ n).] = ((b |^ a) |^ (- n)) * (b |^ n)
thus [.a,(b |^ n).] = ((b |^ (- n)) |^ a) * (b |^ n) by GROUP_1:36
.= ((b |^ a) |^ (- n)) * (b |^ n) by GROUP_3:28 ; ::_thesis: verum
end;
theorem :: GROUP_5:34
for i being Integer
for G being Group
for a, b being Element of G holds [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)
proof
let i be Integer; ::_thesis: for G being Group
for a, b being Element of G holds [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)
let G be Group; ::_thesis: for a, b being Element of G holds [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)
let a, b be Element of G; ::_thesis: [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)
thus [.(a |^ i),b.] = ((a |^ i) ") * (((b ") * (a |^ i)) * b) by Th16
.= (a |^ (- i)) * ((a |^ i) |^ b) by GROUP_1:36
.= (a |^ (- i)) * ((a |^ b) |^ i) by GROUP_3:28 ; ::_thesis: verum
end;
theorem :: GROUP_5:35
for i being Integer
for G being Group
for a, b being Element of G holds [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)
proof
let i be Integer; ::_thesis: for G being Group
for a, b being Element of G holds [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)
let G be Group; ::_thesis: for a, b being Element of G holds [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)
let a, b be Element of G; ::_thesis: [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)
thus [.a,(b |^ i).] = ((b |^ (- i)) |^ a) * (b |^ i) by GROUP_1:36
.= ((b |^ a) |^ (- i)) * (b |^ i) by GROUP_3:28 ; ::_thesis: verum
end;
theorem Th36: :: GROUP_5:36
for G being Group
for a, b being Element of G holds
( [.a,b.] = 1_ G iff a * b = b * a )
proof
let G be Group; ::_thesis: for a, b being Element of G holds
( [.a,b.] = 1_ G iff a * b = b * a )
let a, b be Element of G; ::_thesis: ( [.a,b.] = 1_ G iff a * b = b * a )
thus ( [.a,b.] = 1_ G implies a * b = b * a ) ::_thesis: ( a * b = b * a implies [.a,b.] = 1_ G )
proof
assume [.a,b.] = 1_ G ; ::_thesis: a * b = b * a
then ((b * a) ") * (a * b) = 1_ G by Th17;
then a * b = ((b * a) ") " by GROUP_1:12;
hence a * b = b * a ; ::_thesis: verum
end;
assume a * b = b * a ; ::_thesis: [.a,b.] = 1_ G
then A1: (b * a) " = (b ") * (a ") by GROUP_1:18;
[.a,b.] = ((b * a) ") * (a * b) by Th17;
hence [.a,b.] = (((b ") * (a ")) * a) * b by A1, GROUP_1:def_3
.= (b ") * b by GROUP_3:1
.= 1_ G by GROUP_1:def_5 ;
::_thesis: verum
end;
Lm1: for G being commutative Group
for a, b being Element of G holds a * b = b * a
;
theorem :: GROUP_5:37
for G being Group holds
( G is commutative Group iff for a, b being Element of G holds [.a,b.] = 1_ G )
proof
let G be Group; ::_thesis: ( G is commutative Group iff for a, b being Element of G holds [.a,b.] = 1_ G )
thus ( G is commutative Group implies for a, b being Element of G holds [.a,b.] = 1_ G ) ::_thesis: ( ( for a, b being Element of G holds [.a,b.] = 1_ G ) implies G is commutative Group )
proof
assume A1: G is commutative Group ; ::_thesis: for a, b being Element of G holds [.a,b.] = 1_ G
let a, b be Element of G; ::_thesis: [.a,b.] = 1_ G
a * b = b * a by A1, Lm1;
hence [.a,b.] = 1_ G by Th36; ::_thesis: verum
end;
assume A2: for a, b being Element of G holds [.a,b.] = 1_ G ; ::_thesis: G is commutative Group
G is commutative
proof
let a be Element of G; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * a
let b be Element of G; ::_thesis: a * b = b * a
[.a,b.] = 1_ G by A2;
hence a * b = b * a by Th36; ::_thesis: verum
end;
hence G is commutative Group ; ::_thesis: verum
end;
theorem Th38: :: GROUP_5:38
for G being Group
for a, b being Element of G
for H being Subgroup of G st a in H & b in H holds
[.a,b.] in H
proof
let G be Group; ::_thesis: for a, b being Element of G
for H being Subgroup of G st a in H & b in H holds
[.a,b.] in H
let a, b be Element of G; ::_thesis: for H being Subgroup of G st a in H & b in H holds
[.a,b.] in H
let H be Subgroup of G; ::_thesis: ( a in H & b in H implies [.a,b.] in H )
assume A1: ( a in H & b in H ) ; ::_thesis: [.a,b.] in H
then ( a " in H & b " in H ) by GROUP_2:51;
then A2: (a ") * (b ") in H by GROUP_2:50;
a * b in H by A1, GROUP_2:50;
then ((a ") * (b ")) * (a * b) in H by A2, GROUP_2:50;
hence [.a,b.] in H by Th16; ::_thesis: verum
end;
definition
let G be Group;
let a, b, c be Element of G;
func[.a,b,c.] -> Element of G equals :: GROUP_5:def 3
[.[.a,b.],c.];
correctness
coherence
[.[.a,b.],c.] is Element of G;
;
end;
:: deftheorem defines [. GROUP_5:def_3_:_
for G being Group
for a, b, c being Element of G holds [.a,b,c.] = [.[.a,b.],c.];
theorem :: GROUP_5:39
for G being Group
for a, b being Element of G holds
( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )
proof
let G be Group; ::_thesis: for a, b being Element of G holds
( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )
let a, b be Element of G; ::_thesis: ( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )
thus [.a,b,(1_ G).] = 1_ G by Th19; ::_thesis: ( [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )
thus [.a,(1_ G),b.] = [.(1_ G),b.] by Th19
.= 1_ G by Th19 ; ::_thesis: [.(1_ G),a,b.] = 1_ G
thus [.(1_ G),a,b.] = [.(1_ G),b.] by Th19
.= 1_ G by Th19 ; ::_thesis: verum
end;
theorem :: GROUP_5:40
for G being Group
for a, b being Element of G holds [.a,a,b.] = 1_ G
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,a,b.] = 1_ G
let a, b be Element of G; ::_thesis: [.a,a,b.] = 1_ G
thus [.a,a,b.] = [.(1_ G),b.] by Th20
.= 1_ G by Th19 ; ::_thesis: verum
end;
theorem :: GROUP_5:41
for G being Group
for a, b being Element of G holds [.a,b,a.] = [.(a |^ b),a.]
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,b,a.] = [.(a |^ b),a.]
let a, b be Element of G; ::_thesis: [.a,b,a.] = [.(a |^ b),a.]
thus [.a,b,a.] = (([.b,a.] * (a ")) * [.a,b.]) * a by Th22
.= (((a ") |^ b) * ((((a ") * (b ")) * a) * b)) * a by GROUP_3:1
.= (((a |^ b) ") * ((((a ") * (b ")) * a) * b)) * a by GROUP_3:26
.= (((a |^ b) ") * (((a ") * (b ")) * (a * b))) * a by GROUP_1:def_3
.= (((a |^ b) ") * ((a ") * ((b ") * (a * b)))) * a by GROUP_1:def_3
.= (((a |^ b) ") * ((a ") * (a |^ b))) * a by GROUP_1:def_3
.= [.(a |^ b),a.] by Th16 ; ::_thesis: verum
end;
theorem :: GROUP_5:42
for G being Group
for b, a being Element of G holds [.b,a,a.] = ([.b,(a ").] * [.b,a.]) |^ a
proof
let G be Group; ::_thesis: for b, a being Element of G holds [.b,a,a.] = ([.b,(a ").] * [.b,a.]) |^ a
let b, a be Element of G; ::_thesis: [.b,a,a.] = ([.b,(a ").] * [.b,a.]) |^ a
thus [.b,a,a.] = (([.a,b.] * (a ")) * [.b,a.]) * a by Th22
.= ((((a ") * ((b ") * (a * b))) * (a ")) * [.b,a.]) * a by Th16
.= ((((a ") * ((b ") * (((a ") ") * b))) * (a ")) * [.b,a.]) * a
.= (((a ") * (((b ") * (((a ") ") * b)) * (a "))) * [.b,a.]) * a by GROUP_1:def_3
.= (((a ") * [.b,(a ").]) * [.b,a.]) * a by Th16
.= ([.b,(a ").] * [.b,a.]) |^ a by GROUP_1:def_3 ; ::_thesis: verum
end;
theorem :: GROUP_5:43
for G being Group
for a, b being Element of G holds [.a,b,(b |^ a).] = [.b,[.b,a.].]
proof
let G be Group; ::_thesis: for a, b being Element of G holds [.a,b,(b |^ a).] = [.b,[.b,a.].]
let a, b be Element of G; ::_thesis: [.a,b,(b |^ a).] = [.b,[.b,a.].]
thus [.a,b,(b |^ a).] = (([.b,a.] * ((b |^ a) ")) * [.a,b.]) * (b |^ a) by Th22
.= ((((((b ") * (a ")) * b) * a) * ((b ") |^ a)) * [.a,b.]) * (b |^ a) by GROUP_3:26
.= ((((((b ") * (a ")) * b) * a) * ((a ") * ((b ") * a))) * [.a,b.]) * (b |^ a) by GROUP_1:def_3
.= (((((((b ") * (a ")) * b) * a) * (a ")) * ((b ") * a)) * [.a,b.]) * (b |^ a) by GROUP_1:def_3
.= (((((b ") * (a ")) * b) * ((b ") * a)) * [.a,b.]) * (b |^ a) by GROUP_3:1
.= ((((b ") * (a ")) * (b * ((b ") * a))) * [.a,b.]) * (b |^ a) by GROUP_1:def_3
.= ((((b ") * (a ")) * a) * [.a,b.]) * (b |^ a) by GROUP_3:1
.= ((b ") * ((((a ") * (b ")) * a) * b)) * (b |^ a) by GROUP_3:1
.= (((b ") * ((((a ") * (b ")) * a) * b)) * (1_ G)) * (((a ") * b) * a) by GROUP_1:def_4
.= (((b ") * [.a,b.]) * (b * (b "))) * (((a ") * b) * a) by GROUP_1:def_5
.= ((b ") * [.a,b.]) * ((b * (b ")) * (((a ") * b) * a)) by GROUP_1:def_3
.= ((b ") * [.a,b.]) * (b * ((b ") * (((a ") * b) * a))) by GROUP_1:def_3
.= ((b ") * [.a,b.]) * (b * [.b,a.]) by Th16
.= ((b ") * ([.b,a.] ")) * (b * [.b,a.]) by Th22
.= [.b,[.b,a.].] by Th16 ; ::_thesis: verum
end;
theorem :: GROUP_5:44
for G being Group
for a, b, c being Element of G holds [.(a * b),c.] = ([.a,c.] * [.a,c,b.]) * [.b,c.]
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds [.(a * b),c.] = ([.a,c.] * [.a,c,b.]) * [.b,c.]
let a, b, c be Element of G; ::_thesis: [.(a * b),c.] = ([.a,c.] * [.a,c,b.]) * [.b,c.]
([.a,c.] * [.a,c,b.]) * [.b,c.] = (((((a ") * (c ")) * a) * c) * ((([.c,a.] * (b ")) * [.a,c.]) * b)) * [.b,c.] by Th22
.= (((((a ") * (c ")) * a) * c) * ((((((c ") * (a ")) * (c * a)) * (b ")) * [.a,c.]) * b)) * [.b,c.] by Th16
.= (((((a ") * (c ")) * a) * c) * ((((((a * c) ") * (c * a)) * (b ")) * [.a,c.]) * b)) * [.b,c.] by GROUP_1:17
.= ((((a ") * (c ")) * (a * c)) * ((((((a * c) ") * (c * a)) * (b ")) * [.a,c.]) * b)) * [.b,c.] by GROUP_1:def_3
.= (((a ") * (c ")) * ((a * c) * ((((((a * c) ") * (c * a)) * (b ")) * [.a,c.]) * b))) * [.b,c.] by GROUP_1:def_3
.= (((a ") * (c ")) * ((a * c) * (((((a * c) ") * (c * a)) * (b ")) * ([.a,c.] * b)))) * [.b,c.] by GROUP_1:def_3
.= (((a ") * (c ")) * ((a * c) * ((((a * c) ") * (c * a)) * ((b ") * ([.a,c.] * b))))) * [.b,c.] by GROUP_1:def_3
.= (((a ") * (c ")) * ((a * c) * (((a * c) ") * ((c * a) * ((b ") * ([.a,c.] * b)))))) * [.b,c.] by GROUP_1:def_3
.= (((a ") * (c ")) * (((a * c) * ((a * c) ")) * ((c * a) * ((b ") * ([.a,c.] * b))))) * [.b,c.] by GROUP_1:def_3
.= (((a ") * (c ")) * ((1_ G) * ((c * a) * ((b ") * ([.a,c.] * b))))) * [.b,c.] by GROUP_1:def_5
.= (((a ") * (c ")) * ((c * a) * ((b ") * ([.a,c.] * b)))) * [.b,c.] by GROUP_1:def_4
.= ((((a ") * (c ")) * (c * a)) * ((b ") * ([.a,c.] * b))) * [.b,c.] by GROUP_1:def_3
.= ((((c * a) ") * (c * a)) * ((b ") * ([.a,c.] * b))) * [.b,c.] by GROUP_1:17
.= ((1_ G) * ((b ") * ([.a,c.] * b))) * [.b,c.] by GROUP_1:def_5
.= ((b ") * ([.a,c.] * b)) * [.b,c.] by GROUP_1:def_4
.= ((b ") * (((((a ") * (c ")) * a) * c) * b)) * (((b ") * (c ")) * (b * c)) by Th16
.= (((b ") * ((((a ") * (c ")) * a) * c)) * b) * (((b ") * (c ")) * (b * c)) by GROUP_1:def_3
.= (((b ") * (((a ") * (c ")) * (a * c))) * b) * (((b ") * (c ")) * (b * c)) by GROUP_1:def_3
.= (((b ") * ((a ") * ((c ") * (a * c)))) * b) * (((b ") * (c ")) * (b * c)) by GROUP_1:def_3
.= ((((b ") * (a ")) * ((c ") * (a * c))) * b) * (((b ") * (c ")) * (b * c)) by GROUP_1:def_3
.= (((((b ") * (a ")) * (c ")) * (a * c)) * b) * (((b ") * (c ")) * (b * c)) by GROUP_1:def_3
.= ((((((b ") * (a ")) * (c ")) * a) * c) * b) * (((b ") * (c ")) * (b * c)) by GROUP_1:def_3
.= (((((b ") * (a ")) * (c ")) * a) * (c * b)) * (((b ") * (c ")) * (b * c)) by GROUP_1:def_3
.= ((((((b ") * (a ")) * (c ")) * a) * (c * b)) * ((b ") * (c "))) * (b * c) by GROUP_1:def_3
.= ((((((b ") * (a ")) * (c ")) * a) * (c * b)) * ((c * b) ")) * (b * c) by GROUP_1:17
.= (((((b ") * (a ")) * (c ")) * a) * ((c * b) * ((c * b) "))) * (b * c) by GROUP_1:def_3
.= (((((b ") * (a ")) * (c ")) * a) * (1_ G)) * (b * c) by GROUP_1:def_5
.= ((((b ") * (a ")) * (c ")) * a) * (b * c) by GROUP_1:def_4
.= ((((a * b) ") * (c ")) * a) * (b * c) by GROUP_1:17
.= (((a * b) ") * (c ")) * (a * (b * c)) by GROUP_1:def_3
.= (((a * b) ") * (c ")) * ((a * b) * c) by GROUP_1:def_3 ;
hence [.(a * b),c.] = ([.a,c.] * [.a,c,b.]) * [.b,c.] by Th16; ::_thesis: verum
end;
theorem :: GROUP_5:45
for G being Group
for a, b, c being Element of G holds [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.]
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.]
let a, b, c be Element of G; ::_thesis: [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.]
([.a,c.] * [.a,b.]) * [.a,b,c.] = [.a,c.] * ([.a,b.] * [.[.a,b.],c.]) by GROUP_1:def_3
.= [.a,c.] * ((((a ") * (b ")) * (a * b)) * (((([.a,b.] ") * (c ")) * [.a,b.]) * c)) by Th16
.= [.a,c.] * ((((a ") * (b ")) * (a * b)) * ((([.b,a.] * (c ")) * [.a,b.]) * c)) by Th22
.= [.a,c.] * ((((a ") * (b ")) * (a * b)) * ((((((b ") * (a ")) * (b * a)) * (c ")) * [.a,b.]) * c)) by Th16
.= [.a,c.] * (((a ") * (b ")) * ((a * b) * ((((((b ") * (a ")) * (b * a)) * (c ")) * [.a,b.]) * c))) by GROUP_1:def_3
.= [.a,c.] * (((a ") * (b ")) * ((a * b) * (((((b ") * (a ")) * (b * a)) * (c ")) * ([.a,b.] * c)))) by GROUP_1:def_3
.= [.a,c.] * (((a ") * (b ")) * ((a * b) * ((((b ") * (a ")) * (b * a)) * ((c ") * ([.a,b.] * c))))) by GROUP_1:def_3
.= [.a,c.] * (((a ") * (b ")) * (((a * b) * (((b ") * (a ")) * (b * a))) * ((c ") * ([.a,b.] * c)))) by GROUP_1:def_3
.= [.a,c.] * (((a ") * (b ")) * ((((a * b) * ((b ") * (a "))) * (b * a)) * ((c ") * ([.a,b.] * c)))) by GROUP_1:def_3
.= [.a,c.] * (((a ") * (b ")) * ((((a * b) * ((a * b) ")) * (b * a)) * ((c ") * ([.a,b.] * c)))) by GROUP_1:17
.= [.a,c.] * (((a ") * (b ")) * (((1_ G) * (b * a)) * ((c ") * ([.a,b.] * c)))) by GROUP_1:def_5
.= [.a,c.] * (((a ") * (b ")) * ((b * a) * ((c ") * ([.a,b.] * c)))) by GROUP_1:def_4
.= [.a,c.] * ((((a ") * (b ")) * (b * a)) * ((c ") * ([.a,b.] * c))) by GROUP_1:def_3
.= [.a,c.] * ((((b * a) ") * (b * a)) * ((c ") * ([.a,b.] * c))) by GROUP_1:17
.= [.a,c.] * ((1_ G) * ((c ") * ([.a,b.] * c))) by GROUP_1:def_5
.= [.a,c.] * ((c ") * ([.a,b.] * c)) by GROUP_1:def_4
.= (((a ") * (c ")) * (a * c)) * ((c ") * ([.a,b.] * c)) by Th16
.= (((a ") * (c ")) * (a * c)) * ((c ") * (((a ") * (((b ") * a) * b)) * c)) by Th16
.= (((a ") * (c ")) * (a * c)) * (((c ") * ((a ") * (((b ") * a) * b))) * c) by GROUP_1:def_3
.= (((a ") * (c ")) * (a * c)) * ((((c ") * (a ")) * (((b ") * a) * b)) * c) by GROUP_1:def_3
.= (((a ") * (c ")) * (a * c)) * (((c ") * (a ")) * ((((b ") * a) * b) * c)) by GROUP_1:def_3
.= ((((a ") * (c ")) * (a * c)) * ((c ") * (a "))) * ((((b ") * a) * b) * c) by GROUP_1:def_3
.= (((a ") * (c ")) * ((a * c) * ((c ") * (a ")))) * ((((b ") * a) * b) * c) by GROUP_1:def_3
.= (((a ") * (c ")) * ((a * c) * ((a * c) "))) * ((((b ") * a) * b) * c) by GROUP_1:17
.= (((a ") * (c ")) * (1_ G)) * ((((b ") * a) * b) * c) by GROUP_1:def_5
.= ((a ") * (c ")) * ((((b ") * a) * b) * c) by GROUP_1:def_4
.= (((a ") * (c ")) * (((b ") * a) * b)) * c by GROUP_1:def_3
.= (((a ") * (c ")) * ((b ") * (a * b))) * c by GROUP_1:def_3
.= ((((a ") * (c ")) * (b ")) * (a * b)) * c by GROUP_1:def_3
.= (((a ") * ((c ") * (b "))) * (a * b)) * c by GROUP_1:def_3
.= ((a ") * ((c ") * (b "))) * ((a * b) * c) by GROUP_1:def_3
.= ((a ") * ((c ") * (b "))) * (a * (b * c)) by GROUP_1:def_3
.= ((a ") * ((b * c) ")) * (a * (b * c)) by GROUP_1:17 ;
hence [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.] by Th16; ::_thesis: verum
end;
theorem :: GROUP_5:46
for G being Group
for a, b, c being Element of G holds (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = 1_ G
proof
let G be Group; ::_thesis: for a, b, c being Element of G holds (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = 1_ G
let a, b, c be Element of G; ::_thesis: (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = 1_ G
set d = ((a ") * [.b,(c ").]) * a;
set e = ((c ") * [.a,(b ").]) * c;
set f = ((b ") * [.c,(a ").]) * b;
set x = [.a,(b "),c.] |^ b;
set y = [.b,(c "),a.] |^ c;
set z = [.c,(a "),b.] |^ a;
A1: [.(c "),b.] = ((c ") ") * (((b ") * (c ")) * b) by Th16;
A2: [.(a "),c.] = ((a ") ") * (((c ") * (a ")) * c) by Th16;
A3: [.(b "),a.] = ((b ") ") * (((a ") * (b ")) * a) by Th16;
[.a,(b "),c.] = ([.a,(b ").] ") * (((c ") * [.a,(b ").]) * c) by Th16
.= [.(b "),a.] * (((c ") * [.a,(b ").]) * c) by Th22 ;
then A4: [.a,(b "),c.] |^ b = ((b ") * (((b ") ") * ((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)))) * b by A3, GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)) * b by GROUP_3:1 ;
[.c,(a "),b.] = ([.c,(a ").] ") * (((b ") * [.c,(a ").]) * b) by Th16
.= [.(a "),c.] * (((b ") * [.c,(a ").]) * b) by Th22 ;
then A5: [.c,(a "),b.] |^ a = ((a ") * (((a ") ") * ((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)))) * a by A2, GROUP_1:def_3
.= ((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a by GROUP_3:1 ;
[.b,(c "),a.] = ([.b,(c ").] ") * (((a ") * [.b,(c ").]) * a) by Th16
.= [.(c "),b.] * (((a ") * [.b,(c ").]) * a) by Th22 ;
then [.b,(c "),a.] |^ c = ((c ") * (((c ") ") * ((((b ") * (c ")) * b) * (((a ") * [.b,(c ").]) * a)))) * c by A1, GROUP_1:def_3
.= ((((b ") * (c ")) * b) * (((a ") * [.b,(c ").]) * a)) * c by GROUP_3:1
.= (((b ") * (c ")) * b) * ((((a ") * [.b,(c ").]) * a) * c) by GROUP_1:def_3
.= ((b ") * ((c ") * b)) * ((((a ") * [.b,(c ").]) * a) * c) by GROUP_1:def_3
.= (b ") * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c)) by GROUP_1:def_3 ;
then ([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c) = ((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)) * (b * ((b ") * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c)))) by A4, GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (((c ") * [.a,(b ").]) * c)) * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c)) by GROUP_3:1
.= ((((a ") * (b ")) * a) * ((c ") * ([.a,(b ").] * c))) * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c)) by GROUP_1:def_3
.= (((((a ") * (b ")) * a) * (c ")) * ([.a,(b ").] * c)) * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c)) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * (([.a,(b ").] * c) * (((c ") * b) * ((((a ") * [.b,(c ").]) * a) * c))) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * ((([.a,(b ").] * c) * ((c ") * b)) * ((((a ") * [.b,(c ").]) * a) * c)) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * (((([.a,(b ").] * c) * (c ")) * b) * ((((a ") * [.b,(c ").]) * a) * c)) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * ((((((a ") * ((b ") ")) * a) * (b ")) * b) * ((((a ") * [.b,(c ").]) * a) * c)) by GROUP_3:1
.= ((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * a) * ((((a ") * [.b,(c ").]) * a) * c)) by GROUP_3:1
.= ((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * a) * (((a ") * [.b,(c ").]) * (a * c))) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * a) * ((a ") * ([.b,(c ").] * (a * c)))) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * (((((a ") * ((b ") ")) * a) * (a ")) * ([.b,(c ").] * (a * c))) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * (((a ") * ((b ") ")) * ([.b,(c ").] * (a * c))) by GROUP_3:1
.= ((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * [.b,(c ").]) * (a * c)) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * ((b ") * ((((c ") ") * b) * (c ")))) * (a * c)) by Th16
.= ((((a ") * (b ")) * a) * (c ")) * (((a ") * ((b ") ")) * (((b ") * ((((c ") ") * b) * (c "))) * (a * c))) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * (((a ") * ((b ") ")) * ((b ") * (((((c ") ") * b) * (c ")) * (a * c)))) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * ((((a ") * ((b ") ")) * (b ")) * (((((c ") ") * b) * (c ")) * (a * c))) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * ((a ") * (((((c ") ") * b) * (c ")) * (a * c))) by GROUP_3:1 ;
then (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = (((((a ") * (b ")) * a) * (c ")) * (((a ") * ((((c ") ") * b) * (c "))) * (a * c))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by A5, GROUP_1:def_3
.= ((((a ") * (b ")) * a) * ((c ") * (((a ") * ((((c ") ") * b) * (c "))) * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * ((c ") * ((a ") * (((((c ") ") * b) * (c ")) * (a * c))))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= (((((a ") * (b ")) * a) * (c ")) * ((a ") * (((((c ") ") * b) * (c ")) * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= (((((a ") * (b ")) * a) * (c ")) * ((a ") * ((((c ") ") * (b * (c "))) * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= (((((a ") * (b ")) * a) * (c ")) * ((a ") * (((c ") ") * ((b * (c ")) * (a * c))))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= ((((((a ") * (b ")) * a) * (c ")) * (a ")) * (((c ") ") * ((b * (c ")) * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= (((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * ((b * (c ")) * (a * c))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= (((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * (b * ((c ") * (a * c)))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= ((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * ((c ") * (a * c))) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= (((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * (a * c)) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a) by GROUP_1:def_3
.= ((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * ((a * c) * (((((c ") * (a ")) * c) * (((b ") * [.c,(a ").]) * b)) * a)) by GROUP_1:def_3
.= ((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * ((a * c) * ((((c ") * (a ")) * c) * ((((b ") * [.c,(a ").]) * b) * a))) by GROUP_1:def_3
.= ((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * ((a * c) * (((c ") * (a ")) * (c * ((((b ") * [.c,(a ").]) * b) * a)))) by GROUP_1:def_3
.= ((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * (((a * c) * ((c ") * (a "))) * (c * ((((b ") * [.c,(a ").]) * b) * a))) by GROUP_1:def_3
.= ((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * (((a * c) * ((a * c) ")) * (c * ((((b ") * [.c,(a ").]) * b) * a))) by GROUP_1:17
.= ((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * ((1_ G) * (c * ((((b ") * [.c,(a ").]) * b) * a))) by GROUP_1:def_5
.= ((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * (c * ((((b ") * [.c,(a ").]) * b) * a)) by GROUP_1:def_4
.= (((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (c ")) * c) * ((((b ") * [.c,(a ").]) * b) * a) by GROUP_1:def_3
.= (((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * ((((b ") * [.c,(a ").]) * b) * a) by GROUP_3:1
.= (((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (((b ") * [.c,(a ").]) * (b * a)) by GROUP_1:def_3
.= (((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * ((b ") * ([.c,(a ").] * (b * a))) by GROUP_1:def_3
.= ((((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * b) * (b ")) * ([.c,(a ").] * (b * a)) by GROUP_1:def_3
.= ((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * ([.c,(a ").] * (b * a)) by GROUP_3:1
.= ((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * (((c ") * ((((a ") ") * c) * (a "))) * (b * a)) by Th16
.= ((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * ((c ") * (((((a ") ") * c) * (a ")) * (b * a))) by GROUP_1:def_3
.= (((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((c ") ")) * (c ")) * (((((a ") ") * c) * (a ")) * (b * a)) by GROUP_1:def_3
.= (((((a ") * (b ")) * a) * (c ")) * (a ")) * (((((a ") ") * c) * (a ")) * (b * a)) by GROUP_3:1
.= (((((a ") * (b ")) * a) * (c ")) * (a ")) * ((((a ") ") * (c * (a "))) * (b * a)) by GROUP_1:def_3
.= (((((a ") * (b ")) * a) * (c ")) * (a ")) * (((a ") ") * ((c * (a ")) * (b * a))) by GROUP_1:def_3
.= ((((((a ") * (b ")) * a) * (c ")) * (a ")) * ((a ") ")) * ((c * (a ")) * (b * a)) by GROUP_1:def_3
.= ((((a ") * (b ")) * a) * (c ")) * ((c * (a ")) * (b * a)) by GROUP_3:1
.= (((((a ") * (b ")) * a) * (c ")) * (c * (a "))) * (b * a) by GROUP_1:def_3
.= ((((a ") * (b ")) * (a * (c "))) * (c * (a "))) * (b * a) by GROUP_1:def_3
.= ((((a ") * (b ")) * (a * (c "))) * (((c ") ") * (a "))) * (b * a)
.= ((((a ") * (b ")) * (a * (c "))) * ((a * (c ")) ")) * (b * a) by GROUP_1:17
.= (((a ") * (b ")) * ((a * (c ")) * ((a * (c ")) "))) * (b * a) by GROUP_1:def_3
.= (((a ") * (b ")) * (1_ G)) * (b * a) by GROUP_1:def_5
.= ((a ") * (b ")) * (b * a) by GROUP_1:def_4
.= ((b * a) ") * (b * a) by GROUP_1:17 ;
hence (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = 1_ G by GROUP_1:def_5; ::_thesis: verum
end;
definition
let G be Group;
let A, B be Subset of G;
func commutators (A,B) -> Subset of G equals :: GROUP_5:def 4
{ [.a,b.] where a, b is Element of G : ( a in A & b in B ) } ;
coherence
{ [.a,b.] where a, b is Element of G : ( a in A & b in B ) } is Subset of G
proof
defpred S1[ Element of G, Element of G] means ( $1 in A & $2 in B );
deffunc H1( Element of G, Element of G) -> Element of G = [.$1,$2.];
{ H1(a,b) where a, b is Element of G : S1[a,b] } is Subset of G from DOMAIN_1:sch_9();
hence { [.a,b.] where a, b is Element of G : ( a in A & b in B ) } is Subset of G ; ::_thesis: verum
end;
end;
:: deftheorem defines commutators GROUP_5:def_4_:_
for G being Group
for A, B being Subset of G holds commutators (A,B) = { [.a,b.] where a, b is Element of G : ( a in A & b in B ) } ;
theorem Th47: :: GROUP_5:47
for x being set
for G being Group
for A, B being Subset of G holds
( x in commutators (A,B) iff ex a, b being Element of G st
( x = [.a,b.] & a in A & b in B ) ) ;
theorem :: GROUP_5:48
for G being Group
for A being Subset of G holds
( commutators (({} the carrier of G),A) = {} & commutators (A,({} the carrier of G)) = {} )
proof
let G be Group; ::_thesis: for A being Subset of G holds
( commutators (({} the carrier of G),A) = {} & commutators (A,({} the carrier of G)) = {} )
let A be Subset of G; ::_thesis: ( commutators (({} the carrier of G),A) = {} & commutators (A,({} the carrier of G)) = {} )
commutators (({} the carrier of G),A) c= {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (({} the carrier of G),A) or x in {} )
assume x in commutators (({} the carrier of G),A) ; ::_thesis: x in {}
then ex a, b being Element of G st
( x = [.a,b.] & a in {} the carrier of G & b in A ) ;
hence x in {} ; ::_thesis: verum
end;
hence commutators (({} the carrier of G),A) = {} ; ::_thesis: commutators (A,({} the carrier of G)) = {}
thus commutators (A,({} the carrier of G)) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= commutators (A,({} the carrier of G))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (A,({} the carrier of G)) or x in {} )
assume x in commutators (A,({} the carrier of G)) ; ::_thesis: x in {}
then ex a, b being Element of G st
( x = [.a,b.] & a in A & b in {} the carrier of G ) ;
hence x in {} ; ::_thesis: verum
end;
thus {} c= commutators (A,({} the carrier of G)) by XBOOLE_1:2; ::_thesis: verum
end;
theorem :: GROUP_5:49
for G being Group
for a, b being Element of G holds commutators ({a},{b}) = {[.a,b.]}
proof
let G be Group; ::_thesis: for a, b being Element of G holds commutators ({a},{b}) = {[.a,b.]}
let a, b be Element of G; ::_thesis: commutators ({a},{b}) = {[.a,b.]}
thus commutators ({a},{b}) c= {[.a,b.]} :: according to XBOOLE_0:def_10 ::_thesis: {[.a,b.]} c= commutators ({a},{b})
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators ({a},{b}) or x in {[.a,b.]} )
assume x in commutators ({a},{b}) ; ::_thesis: x in {[.a,b.]}
then consider c, d being Element of G such that
A1: x = [.c,d.] and
A2: ( c in {a} & d in {b} ) ;
( c = a & b = d ) by A2, TARSKI:def_1;
hence x in {[.a,b.]} by A1, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {[.a,b.]} or x in commutators ({a},{b}) )
assume x in {[.a,b.]} ; ::_thesis: x in commutators ({a},{b})
then A3: x = [.a,b.] by TARSKI:def_1;
( a in {a} & b in {b} ) by TARSKI:def_1;
hence x in commutators ({a},{b}) by A3; ::_thesis: verum
end;
theorem Th50: :: GROUP_5:50
for G being Group
for A, B, C, D being Subset of G st A c= B & C c= D holds
commutators (A,C) c= commutators (B,D)
proof
let G be Group; ::_thesis: for A, B, C, D being Subset of G st A c= B & C c= D holds
commutators (A,C) c= commutators (B,D)
let A, B, C, D be Subset of G; ::_thesis: ( A c= B & C c= D implies commutators (A,C) c= commutators (B,D) )
assume A1: ( A c= B & C c= D ) ; ::_thesis: commutators (A,C) c= commutators (B,D)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (A,C) or x in commutators (B,D) )
assume x in commutators (A,C) ; ::_thesis: x in commutators (B,D)
then ex a, c being Element of G st
( x = [.a,c.] & a in A & c in C ) ;
hence x in commutators (B,D) by A1; ::_thesis: verum
end;
theorem Th51: :: GROUP_5:51
for G being Group holds
( G is commutative Group iff for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)} )
proof
let G be Group; ::_thesis: ( G is commutative Group iff for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)} )
thus ( G is commutative Group implies for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)} ) ::_thesis: ( ( for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)} ) implies G is commutative Group )
proof
assume A1: G is commutative Group ; ::_thesis: for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)}
let A, B be Subset of G; ::_thesis: ( A <> {} & B <> {} implies commutators (A,B) = {(1_ G)} )
assume A2: ( A <> {} & B <> {} ) ; ::_thesis: commutators (A,B) = {(1_ G)}
thus commutators (A,B) c= {(1_ G)} :: according to XBOOLE_0:def_10 ::_thesis: {(1_ G)} c= commutators (A,B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (A,B) or x in {(1_ G)} )
assume x in commutators (A,B) ; ::_thesis: x in {(1_ G)}
then consider a, b being Element of G such that
A3: x = [.a,b.] and
a in A and
b in B ;
x = ((a ") * ((b ") * a)) * b by A3, Th16
.= ((a ") * (a * (b "))) * b by A1, Lm1
.= (b ") * b by GROUP_3:1
.= 1_ G by GROUP_1:def_5 ;
hence x in {(1_ G)} by TARSKI:def_1; ::_thesis: verum
end;
set b = the Element of B;
set a = the Element of A;
reconsider a = the Element of A, b = the Element of B as Element of G by A2, TARSKI:def_3;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(1_ G)} or x in commutators (A,B) )
assume x in {(1_ G)} ; ::_thesis: x in commutators (A,B)
then A4: x = 1_ G by TARSKI:def_1;
[.a,b.] = ((a ") * ((b ") * a)) * b by Th16
.= ((a ") * (a * (b "))) * b by A1, Lm1
.= (b ") * b by GROUP_3:1
.= x by A4, GROUP_1:def_5 ;
hence x in commutators (A,B) by A2; ::_thesis: verum
end;
assume A5: for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)} ; ::_thesis: G is commutative Group
G is commutative
proof
let a be Element of G; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * a
let b be Element of G; ::_thesis: a * b = b * a
( a in {a} & b in {b} ) by TARSKI:def_1;
then A6: [.a,b.] in commutators ({a},{b}) ;
commutators ({a},{b}) = {(1_ G)} by A5;
then [.a,b.] = 1_ G by A6, TARSKI:def_1;
then ((a ") * (b ")) * (a * b) = 1_ G by Th16;
then ((b * a) ") * (a * b) = 1_ G by GROUP_1:17;
then a * b = ((b * a) ") " by GROUP_1:12;
hence a * b = b * a ; ::_thesis: verum
end;
hence G is commutative Group ; ::_thesis: verum
end;
definition
let G be Group;
let H1, H2 be Subgroup of G;
func commutators (H1,H2) -> Subset of G equals :: GROUP_5:def 5
commutators ((carr H1),(carr H2));
correctness
coherence
commutators ((carr H1),(carr H2)) is Subset of G;
;
end;
:: deftheorem defines commutators GROUP_5:def_5_:_
for G being Group
for H1, H2 being Subgroup of G holds commutators (H1,H2) = commutators ((carr H1),(carr H2));
theorem Th52: :: GROUP_5:52
for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )
proof
let x be set ; ::_thesis: for G being Group
for H1, H2 being Subgroup of G holds
( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds
( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )
let H1, H2 be Subgroup of G; ::_thesis: ( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )
thus ( x in commutators (H1,H2) implies ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) ) ::_thesis: ( ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) implies x in commutators (H1,H2) )
proof
assume x in commutators (H1,H2) ; ::_thesis: ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 )
then consider a, b being Element of G such that
A1: x = [.a,b.] and
A2: ( a in carr H1 & b in carr H2 ) ;
( a in H1 & b in H2 ) by A2, STRUCT_0:def_5;
hence ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) by A1; ::_thesis: verum
end;
given a, b being Element of G such that A3: x = [.a,b.] and
A4: ( a in H1 & b in H2 ) ; ::_thesis: x in commutators (H1,H2)
( a in carr H1 & b in carr H2 ) by A4, STRUCT_0:def_5;
hence x in commutators (H1,H2) by A3; ::_thesis: verum
end;
theorem Th53: :: GROUP_5:53
for G being Group
for H1, H2 being Subgroup of G holds 1_ G in commutators (H1,H2)
proof
let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds 1_ G in commutators (H1,H2)
let H1, H2 be Subgroup of G; ::_thesis: 1_ G in commutators (H1,H2)
A1: 1_ G in H2 by GROUP_2:46;
( [.(1_ G),(1_ G).] = 1_ G & 1_ G in H1 ) by Th19, GROUP_2:46;
hence 1_ G in commutators (H1,H2) by A1, Th52; ::_thesis: verum
end;
theorem :: GROUP_5:54
for G being Group
for H being Subgroup of G holds
( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )
proof
let G be Group; ::_thesis: for H being Subgroup of G holds
( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )
let H be Subgroup of G; ::_thesis: ( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )
A1: commutators (((1). G),H) c= {(1_ G)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (((1). G),H) or x in {(1_ G)} )
assume x in commutators (((1). G),H) ; ::_thesis: x in {(1_ G)}
then consider a, b being Element of G such that
A2: x = [.a,b.] and
A3: a in (1). G and
b in H by Th52;
a = 1_ G by A3, Th1;
then x = 1_ G by A2, Th19;
hence x in {(1_ G)} by TARSKI:def_1; ::_thesis: verum
end;
1_ G in commutators (((1). G),H) by Th53;
hence commutators (((1). G),H) = {(1_ G)} by A1, ZFMISC_1:33; ::_thesis: commutators (H,((1). G)) = {(1_ G)}
thus commutators (H,((1). G)) c= {(1_ G)} :: according to XBOOLE_0:def_10 ::_thesis: {(1_ G)} c= commutators (H,((1). G))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (H,((1). G)) or x in {(1_ G)} )
assume x in commutators (H,((1). G)) ; ::_thesis: x in {(1_ G)}
then consider a, b being Element of G such that
A4: x = [.a,b.] and
a in H and
A5: b in (1). G by Th52;
b = 1_ G by A5, Th1;
then x = 1_ G by A4, Th19;
hence x in {(1_ G)} by TARSKI:def_1; ::_thesis: verum
end;
1_ G in commutators (H,((1). G)) by Th53;
hence {(1_ G)} c= commutators (H,((1). G)) by ZFMISC_1:31; ::_thesis: verum
end;
theorem Th55: :: GROUP_5:55
for G being Group
for H being Subgroup of G
for N being strict normal Subgroup of G holds
( commutators (H,N) c= carr N & commutators (N,H) c= carr N )
proof
let G be Group; ::_thesis: for H being Subgroup of G
for N being strict normal Subgroup of G holds
( commutators (H,N) c= carr N & commutators (N,H) c= carr N )
let H be Subgroup of G; ::_thesis: for N being strict normal Subgroup of G holds
( commutators (H,N) c= carr N & commutators (N,H) c= carr N )
let N be strict normal Subgroup of G; ::_thesis: ( commutators (H,N) c= carr N & commutators (N,H) c= carr N )
thus commutators (H,N) c= carr N ::_thesis: commutators (N,H) c= carr N
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (H,N) or x in carr N )
assume x in commutators (H,N) ; ::_thesis: x in carr N
then consider a, b being Element of G such that
A1: x = [.a,b.] and
a in H and
A2: b in N by Th52;
b " in N by A2, GROUP_2:51;
then (b ") |^ a in N |^ a by GROUP_3:58;
then (b ") |^ a in N by GROUP_3:def_13;
then x in N by A1, A2, GROUP_2:50;
hence x in carr N by STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (N,H) or x in carr N )
assume x in commutators (N,H) ; ::_thesis: x in carr N
then consider a, b being Element of G such that
A3: x = [.a,b.] and
A4: a in N and
b in H by Th52;
a |^ b in N |^ b by A4, GROUP_3:58;
then A5: a |^ b in N by GROUP_3:def_13;
( x = (a ") * (a |^ b) & a " in N ) by A3, A4, Th16, GROUP_2:51;
then x in N by A5, GROUP_2:50;
hence x in carr N by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th56: :: GROUP_5:56
for G being Group
for H1, H2, H3, H4 being Subgroup of G st H1 is Subgroup of H2 & H3 is Subgroup of H4 holds
commutators (H1,H3) c= commutators (H2,H4)
proof
let G be Group; ::_thesis: for H1, H2, H3, H4 being Subgroup of G st H1 is Subgroup of H2 & H3 is Subgroup of H4 holds
commutators (H1,H3) c= commutators (H2,H4)
let H1, H2, H3, H4 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 & H3 is Subgroup of H4 implies commutators (H1,H3) c= commutators (H2,H4) )
assume ( H1 is Subgroup of H2 & H3 is Subgroup of H4 ) ; ::_thesis: commutators (H1,H3) c= commutators (H2,H4)
then ( the carrier of H1 c= the carrier of H2 & the carrier of H3 c= the carrier of H4 ) by GROUP_2:def_5;
hence commutators (H1,H3) c= commutators (H2,H4) by Th50; ::_thesis: verum
end;
theorem Th57: :: GROUP_5:57
for G being Group holds
( G is commutative Group iff for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} )
proof
let G be Group; ::_thesis: ( G is commutative Group iff for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} )
thus ( G is commutative Group implies for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ) by Th51; ::_thesis: ( ( for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ) implies G is commutative Group )
assume A1: for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} ; ::_thesis: G is commutative Group
G is commutative
proof
let a be Element of G; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * a
let b be Element of G; ::_thesis: a * b = b * a
b in {b} by TARSKI:def_1;
then A2: b in gr {b} by GROUP_4:29;
a in {a} by TARSKI:def_1;
then a in gr {a} by GROUP_4:29;
then [.a,b.] in commutators ((gr {a}),(gr {b})) by A2, Th52;
then [.a,b.] in {(1_ G)} by A1;
then [.a,b.] = 1_ G by TARSKI:def_1;
hence a * b = b * a by Th36; ::_thesis: verum
end;
hence G is commutative Group ; ::_thesis: verum
end;
definition
let G be Group;
func commutators G -> Subset of G equals :: GROUP_5:def 6
commutators (((Omega). G),((Omega). G));
correctness
coherence
commutators (((Omega). G),((Omega). G)) is Subset of G;
;
end;
:: deftheorem defines commutators GROUP_5:def_6_:_
for G being Group holds commutators G = commutators (((Omega). G),((Omega). G));
theorem Th58: :: GROUP_5:58
for x being set
for G being Group holds
( x in commutators G iff ex a, b being Element of G st x = [.a,b.] )
proof
let x be set ; ::_thesis: for G being Group holds
( x in commutators G iff ex a, b being Element of G st x = [.a,b.] )
let G be Group; ::_thesis: ( x in commutators G iff ex a, b being Element of G st x = [.a,b.] )
thus ( x in commutators G implies ex a, b being Element of G st x = [.a,b.] ) ::_thesis: ( ex a, b being Element of G st x = [.a,b.] implies x in commutators G )
proof
assume x in commutators G ; ::_thesis: ex a, b being Element of G st x = [.a,b.]
then ex a, b being Element of G st
( x = [.a,b.] & a in (Omega). G & b in (Omega). G ) by Th52;
hence ex a, b being Element of G st x = [.a,b.] ; ::_thesis: verum
end;
given a, b being Element of G such that A1: x = [.a,b.] ; ::_thesis: x in commutators G
thus x in commutators G by A1; ::_thesis: verum
end;
theorem :: GROUP_5:59
for G being Group holds
( G is commutative Group iff commutators G = {(1_ G)} )
proof
let G be Group; ::_thesis: ( G is commutative Group iff commutators G = {(1_ G)} )
thus ( G is commutative Group implies commutators G = {(1_ G)} ) by Th57; ::_thesis: ( commutators G = {(1_ G)} implies G is commutative Group )
assume A1: commutators G = {(1_ G)} ; ::_thesis: G is commutative Group
G is commutative
proof
let a be Element of G; :: according to GROUP_1:def_12 ::_thesis: for b1 being Element of the carrier of G holds a * b1 = b1 * a
let b be Element of G; ::_thesis: a * b = b * a
[.a,b.] in {(1_ G)} by A1;
then [.a,b.] = 1_ G by TARSKI:def_1;
hence a * b = b * a by Th36; ::_thesis: verum
end;
hence G is commutative Group ; ::_thesis: verum
end;
definition
let G be Group;
let A, B be Subset of G;
func[.A,B.] -> strict Subgroup of G equals :: GROUP_5:def 7
gr (commutators (A,B));
correctness
coherence
gr (commutators (A,B)) is strict Subgroup of G;
;
end;
:: deftheorem defines [. GROUP_5:def_7_:_
for G being Group
for A, B being Subset of G holds [.A,B.] = gr (commutators (A,B));
theorem Th60: :: GROUP_5:60
for G being Group
for a, b being Element of G
for A, B being Subset of G st a in A & b in B holds
[.a,b.] in [.A,B.]
proof
let G be Group; ::_thesis: for a, b being Element of G
for A, B being Subset of G st a in A & b in B holds
[.a,b.] in [.A,B.]
let a, b be Element of G; ::_thesis: for A, B being Subset of G st a in A & b in B holds
[.a,b.] in [.A,B.]
let A, B be Subset of G; ::_thesis: ( a in A & b in B implies [.a,b.] in [.A,B.] )
assume ( a in A & b in B ) ; ::_thesis: [.a,b.] in [.A,B.]
then [.a,b.] in commutators (A,B) ;
hence [.a,b.] in [.A,B.] by GROUP_4:29; ::_thesis: verum
end;
theorem Th61: :: GROUP_5:61
for x being set
for G being Group
for A, B being Subset of G holds
( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )
proof
let x be set ; ::_thesis: for G being Group
for A, B being Subset of G holds
( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )
let G be Group; ::_thesis: for A, B being Subset of G holds
( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )
let A, B be Subset of G; ::_thesis: ( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )
thus ( x in [.A,B.] implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) ) ::_thesis: ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) implies x in [.A,B.] )
proof
assume A1: x in [.A,B.] ; ::_thesis: ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) )
then x in G by GROUP_2:40;
then reconsider a = x as Element of G by STRUCT_0:def_5;
a in gr (commutators (A,B)) by A1;
hence ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) by GROUP_4:28; ::_thesis: verum
end;
thus ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) implies x in [.A,B.] ) by GROUP_4:28; ::_thesis: verum
end;
theorem :: GROUP_5:62
for G being Group
for A, C, B, D being Subset of G st A c= C & B c= D holds
[.A,B.] is Subgroup of [.C,D.] by Th50, GROUP_4:32;
definition
let G be Group;
let H1, H2 be Subgroup of G;
func[.H1,H2.] -> strict Subgroup of G equals :: GROUP_5:def 8
[.(carr H1),(carr H2).];
correctness
coherence
[.(carr H1),(carr H2).] is strict Subgroup of G;
;
end;
:: deftheorem defines [. GROUP_5:def_8_:_
for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] = [.(carr H1),(carr H2).];
theorem :: GROUP_5:63
for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] = gr (commutators (H1,H2)) ;
theorem :: GROUP_5:64
for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in [.H1,H2.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (H1,H2) & x = Product (F |^ I) ) ) by Th61;
theorem Th65: :: GROUP_5:65
for G being Group
for a, b being Element of G
for H1, H2 being Subgroup of G st a in H1 & b in H2 holds
[.a,b.] in [.H1,H2.]
proof
let G be Group; ::_thesis: for a, b being Element of G
for H1, H2 being Subgroup of G st a in H1 & b in H2 holds
[.a,b.] in [.H1,H2.]
let a, b be Element of G; ::_thesis: for H1, H2 being Subgroup of G st a in H1 & b in H2 holds
[.a,b.] in [.H1,H2.]
let H1, H2 be Subgroup of G; ::_thesis: ( a in H1 & b in H2 implies [.a,b.] in [.H1,H2.] )
assume ( a in H1 & b in H2 ) ; ::_thesis: [.a,b.] in [.H1,H2.]
then ( a in carr H1 & b in carr H2 ) by STRUCT_0:def_5;
hence [.a,b.] in [.H1,H2.] by Th60; ::_thesis: verum
end;
theorem :: GROUP_5:66
for G being Group
for H1, H2, H3, H4 being Subgroup of G st H1 is Subgroup of H2 & H3 is Subgroup of H4 holds
[.H1,H3.] is Subgroup of [.H2,H4.]
proof
let G be Group; ::_thesis: for H1, H2, H3, H4 being Subgroup of G st H1 is Subgroup of H2 & H3 is Subgroup of H4 holds
[.H1,H3.] is Subgroup of [.H2,H4.]
let H1, H2, H3, H4 be Subgroup of G; ::_thesis: ( H1 is Subgroup of H2 & H3 is Subgroup of H4 implies [.H1,H3.] is Subgroup of [.H2,H4.] )
assume ( H1 is Subgroup of H2 & H3 is Subgroup of H4 ) ; ::_thesis: [.H1,H3.] is Subgroup of [.H2,H4.]
then commutators (H1,H3) c= commutators (H2,H4) by Th56;
hence [.H1,H3.] is Subgroup of [.H2,H4.] by GROUP_4:32; ::_thesis: verum
end;
theorem :: GROUP_5:67
for G being Group
for H being Subgroup of G
for N being strict normal Subgroup of G holds
( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )
proof
let G be Group; ::_thesis: for H being Subgroup of G
for N being strict normal Subgroup of G holds
( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )
let H be Subgroup of G; ::_thesis: for N being strict normal Subgroup of G holds
( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )
let N be strict normal Subgroup of G; ::_thesis: ( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )
now__::_thesis:_for_a_being_Element_of_G_st_a_in_[.N,H.]_holds_
a_in_N
let a be Element of G; ::_thesis: ( a in [.N,H.] implies a in N )
assume a in [.N,H.] ; ::_thesis: a in N
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A1: len F = len I and
A2: rng F c= commutators (N,H) and
A3: a = Product (F |^ I) by Th61;
commutators (N,H) c= carr N by Th55;
then rng F c= carr N by A2, XBOOLE_1:1;
then a in gr (carr N) by A1, A3, GROUP_4:28;
hence a in N by GROUP_4:31; ::_thesis: verum
end;
hence [.N,H.] is Subgroup of N by GROUP_2:58; ::_thesis: [.H,N.] is Subgroup of N
now__::_thesis:_for_a_being_Element_of_G_st_a_in_[.H,N.]_holds_
a_in_N
let a be Element of G; ::_thesis: ( a in [.H,N.] implies a in N )
assume a in [.H,N.] ; ::_thesis: a in N
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A4: len F = len I and
A5: rng F c= commutators (H,N) and
A6: a = Product (F |^ I) by Th61;
commutators (H,N) c= carr N by Th55;
then rng F c= carr N by A5, XBOOLE_1:1;
then a in gr (carr N) by A4, A6, GROUP_4:28;
hence a in N by GROUP_4:31; ::_thesis: verum
end;
hence [.H,N.] is Subgroup of N by GROUP_2:58; ::_thesis: verum
end;
theorem Th68: :: GROUP_5:68
for G being Group
for N1, N2 being strict normal Subgroup of G holds [.N1,N2.] is normal Subgroup of G
proof
let G be Group; ::_thesis: for N1, N2 being strict normal Subgroup of G holds [.N1,N2.] is normal Subgroup of G
let N1, N2 be strict normal Subgroup of G; ::_thesis: [.N1,N2.] is normal Subgroup of G
now__::_thesis:_for_a_being_Element_of_G_holds_[.N1,N2.]_|^_a_is_Subgroup_of_[.N1,N2.]
let a be Element of G; ::_thesis: [.N1,N2.] |^ a is Subgroup of [.N1,N2.]
now__::_thesis:_for_b_being_Element_of_G_st_b_in_[.N1,N2.]_|^_a_holds_
b_in_[.N1,N2.]
let b be Element of G; ::_thesis: ( b in [.N1,N2.] |^ a implies b in [.N1,N2.] )
assume b in [.N1,N2.] |^ a ; ::_thesis: b in [.N1,N2.]
then consider c being Element of G such that
A1: b = c |^ a and
A2: c in [.N1,N2.] by GROUP_3:58;
consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A3: len F = len I and
A4: rng F c= commutators ((carr N1),(carr N2)) and
A5: c = Product (F |^ I) by A2, GROUP_4:28;
A6: len (F |^ a) = len F by Def1;
A7: rng (F |^ a) c= commutators ((carr N1),(carr N2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (F |^ a) or x in commutators ((carr N1),(carr N2)) )
assume x in rng (F |^ a) ; ::_thesis: x in commutators ((carr N1),(carr N2))
then consider y being set such that
A8: y in dom (F |^ a) and
A9: (F |^ a) . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A8;
A10: y in dom F by A6, A8, FINSEQ_3:29;
then A11: F . y = F /. y by PARTFUN1:def_6;
y in dom F by A6, A8, FINSEQ_3:29;
then F . y in rng F by FUNCT_1:def_3;
then consider d, e being Element of G such that
A12: F . y = [.d,e.] and
A13: d in carr N1 and
A14: e in carr N2 by A4, Th47;
d in N1 by A13, STRUCT_0:def_5;
then d |^ a in N1 |^ a by GROUP_3:58;
then d |^ a in N1 by GROUP_3:def_13;
then A15: d |^ a in carr N1 by STRUCT_0:def_5;
e in N2 by A14, STRUCT_0:def_5;
then e |^ a in N2 |^ a by GROUP_3:58;
then e |^ a in N2 by GROUP_3:def_13;
then A16: e |^ a in carr N2 by STRUCT_0:def_5;
x = (F /. y) |^ a by A9, A10, Def1;
then x = [.(d |^ a),(e |^ a).] by A12, A11, Th23;
hence x in commutators ((carr N1),(carr N2)) by A15, A16; ::_thesis: verum
end;
b = Product ((F |^ I) |^ a) by A1, A5, Th14
.= Product ((F |^ a) |^ I) by Th15 ;
hence b in [.N1,N2.] by A3, A6, A7, GROUP_4:28; ::_thesis: verum
end;
hence [.N1,N2.] |^ a is Subgroup of [.N1,N2.] by GROUP_2:58; ::_thesis: verum
end;
hence [.N1,N2.] is normal Subgroup of G by GROUP_3:122; ::_thesis: verum
end;
Lm2: for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]
proof
let G be Group; ::_thesis: for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]
let N1, N2 be normal Subgroup of G; ::_thesis: [.N1,N2.] is Subgroup of [.N2,N1.]
now__::_thesis:_for_a_being_Element_of_G_st_a_in_[.N1,N2.]_holds_
a_in_[.N2,N1.]
let a be Element of G; ::_thesis: ( a in [.N1,N2.] implies a in [.N2,N1.] )
assume a in [.N1,N2.] ; ::_thesis: a in [.N2,N1.]
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
len F = len I and
A1: rng F c= commutators (N1,N2) and
A2: a = Product (F |^ I) by Th61;
deffunc H1( Nat) -> Element of the carrier of G = (F /. $1) " ;
consider F1 being FinSequence of the carrier of G such that
A3: len F1 = len F and
A4: for k being Nat st k in dom F1 holds
F1 . k = H1(k) from FINSEQ_2:sch_1();
A5: dom F = Seg (len F) by FINSEQ_1:def_3;
A6: rng F1 c= commutators (N2,N1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F1 or x in commutators (N2,N1) )
assume x in rng F1 ; ::_thesis: x in commutators (N2,N1)
then consider y being set such that
A7: y in dom F1 and
A8: F1 . y = x by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A7;
y in dom F by A3, A7, FINSEQ_3:29;
then A9: F /. y = F . y by PARTFUN1:def_6;
y in dom F by A3, A7, FINSEQ_3:29;
then F . y in rng F by FUNCT_1:def_3;
then consider b, c being Element of G such that
A10: F . y = [.b,c.] and
A11: ( b in N1 & c in N2 ) by A1, Th52;
x = (F /. y) " by A4, A7, A8;
then x = [.c,b.] by A10, A9, Th22;
hence x in commutators (N2,N1) by A11, Th52; ::_thesis: verum
end;
A12: len (F |^ I) = len F by GROUP_4:def_3;
then A13: dom (F |^ I) = Seg (len F) by FINSEQ_1:def_3;
deffunc H2( Nat) -> Element of INT = @ (- (@ (I /. $1)));
consider I1 being FinSequence of INT such that
A14: len I1 = len F and
A15: for k being Nat st k in dom I1 holds
I1 . k = H2(k) from FINSEQ_2:sch_1();
set J = F1 |^ I1;
A16: dom F1 = dom F by A3, FINSEQ_3:29;
A17: dom I1 = dom F by A14, FINSEQ_3:29;
A18: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(F_|^_I)_holds_
(F_|^_I)_._k_=_(F1_|^_I1)_._k
let k be Nat; ::_thesis: ( k in dom (F |^ I) implies (F |^ I) . k = (F1 |^ I1) . k )
assume A19: k in dom (F |^ I) ; ::_thesis: (F |^ I) . k = (F1 |^ I1) . k
then A20: k in dom F by A13, FINSEQ_1:def_3;
A21: ( (F1 |^ I1) . k = (F1 /. k) |^ (@ (I1 /. k)) & F1 /. k = F1 . k ) by A5, A16, A13, A19, GROUP_4:def_3, PARTFUN1:def_6;
A22: I1 . k = @ (- (@ (I /. k))) by A15, A5, A17, A13, A19;
( F1 . k = (F /. k) " & I1 . k = I1 /. k ) by A4, A5, A16, A17, A13, A19, PARTFUN1:def_6;
then (F1 |^ I1) . k = (((F /. k) ") |^ (@ (I /. k))) " by A21, A22, GROUP_1:36
.= (((F /. k) |^ (@ (I /. k))) ") " by GROUP_1:37
.= (F /. k) |^ (@ (I /. k)) ;
hence (F |^ I) . k = (F1 |^ I1) . k by A20, GROUP_4:def_3; ::_thesis: verum
end;
len (F1 |^ I1) = len F by A3, GROUP_4:def_3;
then F1 |^ I1 = F |^ I by A12, A18, FINSEQ_2:9;
hence a in [.N2,N1.] by A2, A3, A14, A6, Th61; ::_thesis: verum
end;
hence [.N1,N2.] is Subgroup of [.N2,N1.] by GROUP_2:58; ::_thesis: verum
end;
theorem Th69: :: GROUP_5:69
for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] = [.N2,N1.]
proof
let G be Group; ::_thesis: for N1, N2 being normal Subgroup of G holds [.N1,N2.] = [.N2,N1.]
let N1, N2 be normal Subgroup of G; ::_thesis: [.N1,N2.] = [.N2,N1.]
( [.N1,N2.] is Subgroup of [.N2,N1.] & [.N2,N1.] is Subgroup of [.N1,N2.] ) by Lm2;
hence [.N1,N2.] = [.N2,N1.] by GROUP_2:55; ::_thesis: verum
end;
theorem Th70: :: GROUP_5:70
for G being Group
for N1, N2, N3 being strict normal Subgroup of G holds [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.]
proof
let G be Group; ::_thesis: for N1, N2, N3 being strict normal Subgroup of G holds [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.]
let N1, N2, N3 be strict normal Subgroup of G; ::_thesis: [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.]
A1: [.N1,N3.] is normal Subgroup of G by Th68;
A2: [.N2,N3.] is normal Subgroup of G by Th68;
now__::_thesis:_for_a_being_Element_of_G_st_a_in_[.N1,N3.]_"\/"_[.N2,N3.]_holds_
a_in_[.(N1_"\/"_N2),N3.]
let a be Element of G; ::_thesis: ( a in [.N1,N3.] "\/" [.N2,N3.] implies a in [.(N1 "\/" N2),N3.] )
A3: N3 is Subgroup of N3 by GROUP_2:54;
N2 is Subgroup of N1 "\/" N2 by GROUP_4:60;
then A4: commutators (N2,N3) c= commutators ((N1 "\/" N2),N3) by A3, Th56;
assume a in [.N1,N3.] "\/" [.N2,N3.] ; ::_thesis: a in [.(N1 "\/" N2),N3.]
then consider b, c being Element of G such that
A5: a = b * c and
A6: b in [.N1,N3.] and
A7: c in [.N2,N3.] by A1, A2, Th7;
consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT such that
A8: len F1 = len I1 and
A9: rng F1 c= commutators (N1,N3) and
A10: b = Product (F1 |^ I1) by A6, Th61;
consider F2 being FinSequence of the carrier of G, I2 being FinSequence of INT such that
A11: len F2 = len I2 and
A12: rng F2 c= commutators (N2,N3) and
A13: c = Product (F2 |^ I2) by A7, Th61;
A14: len (F1 ^ F2) = (len I1) + (len I2) by A8, A11, FINSEQ_1:22
.= len (I1 ^ I2) by FINSEQ_1:22 ;
rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:31;
then A15: rng (F1 ^ F2) c= (commutators (N1,N3)) \/ (commutators (N2,N3)) by A9, A12, XBOOLE_1:13;
N1 is Subgroup of N1 "\/" N2 by GROUP_4:60;
then commutators (N1,N3) c= commutators ((N1 "\/" N2),N3) by A3, Th56;
then (commutators (N1,N3)) \/ (commutators (N2,N3)) c= commutators ((N1 "\/" N2),N3) by A4, XBOOLE_1:8;
then A16: rng (F1 ^ F2) c= commutators ((N1 "\/" N2),N3) by A15, XBOOLE_1:1;
Product ((F1 ^ F2) |^ (I1 ^ I2)) = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A8, A11, GROUP_4:19
.= a by A5, A10, A13, GROUP_4:5 ;
hence a in [.(N1 "\/" N2),N3.] by A16, A14, Th61; ::_thesis: verum
end;
then A17: [.N1,N3.] "\/" [.N2,N3.] is Subgroup of [.(N1 "\/" N2),N3.] by GROUP_2:58;
commutators ((N1 "\/" N2),N3) c= [.N1,N3.] * [.N2,N3.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators ((N1 "\/" N2),N3) or x in [.N1,N3.] * [.N2,N3.] )
assume x in commutators ((N1 "\/" N2),N3) ; ::_thesis: x in [.N1,N3.] * [.N2,N3.]
then consider a, b being Element of G such that
A18: x = [.a,b.] and
A19: a in N1 "\/" N2 and
A20: b in N3 by Th52;
consider c, d being Element of G such that
A21: a = c * d and
A22: c in N1 and
A23: d in N2 by A19, Th7;
[.c,b.] in [.N1,N3.] by A20, A22, Th65;
then [.c,b.] |^ d in [.N1,N3.] |^ d by GROUP_3:58;
then A24: [.c,b.] |^ d in [.N1,N3.] by A1, GROUP_3:def_13;
( x = ([.c,b.] |^ d) * [.d,b.] & [.d,b.] in [.N2,N3.] ) by A18, A20, A21, A23, Th25, Th65;
hence x in [.N1,N3.] * [.N2,N3.] by A24, Th4; ::_thesis: verum
end;
then gr (commutators ((N1 "\/" N2),N3)) is Subgroup of gr ([.N1,N3.] * [.N2,N3.]) by GROUP_4:32;
then [.(N1 "\/" N2),N3.] is Subgroup of [.N1,N3.] "\/" [.N2,N3.] by GROUP_4:50;
hence [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.] by A17, GROUP_2:55; ::_thesis: verum
end;
theorem :: GROUP_5:71
for G being Group
for N1, N2, N3 being strict normal Subgroup of G holds [.N1,(N2 "\/" N3).] = [.N1,N2.] "\/" [.N1,N3.]
proof
let G be Group; ::_thesis: for N1, N2, N3 being strict normal Subgroup of G holds [.N1,(N2 "\/" N3).] = [.N1,N2.] "\/" [.N1,N3.]
let N1, N2, N3 be strict normal Subgroup of G; ::_thesis: [.N1,(N2 "\/" N3).] = [.N1,N2.] "\/" [.N1,N3.]
N2 "\/" N3 is normal Subgroup of G by GROUP_4:54;
hence [.N1,(N2 "\/" N3).] = [.(N2 "\/" N3),N1.] by Th69
.= [.N2,N1.] "\/" [.N3,N1.] by Th70
.= [.N1,N2.] "\/" [.N3,N1.] by Th69
.= [.N1,N2.] "\/" [.N1,N3.] by Th69 ;
::_thesis: verum
end;
definition
let G be Group;
funcG ` -> strict normal Subgroup of G equals :: GROUP_5:def 9
[.((Omega). G),((Omega). G).];
coherence
[.((Omega). G),((Omega). G).] is strict normal Subgroup of G
proof
(Omega). G is normal Subgroup of G by GROUP_3:114;
hence [.((Omega). G),((Omega). G).] is strict normal Subgroup of G by Th68; ::_thesis: verum
end;
end;
:: deftheorem defines ` GROUP_5:def_9_:_
for G being Group holds G ` = [.((Omega). G),((Omega). G).];
theorem :: GROUP_5:72
for G being Group holds G ` = gr (commutators G) ;
theorem Th73: :: GROUP_5:73
for x being set
for G being Group holds
( x in G ` iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & x = Product (F |^ I) ) )
proof
let x be set ; ::_thesis: for G being Group holds
( x in G ` iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & x = Product (F |^ I) ) )
let G be Group; ::_thesis: ( x in G ` iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & x = Product (F |^ I) ) )
thus ( x in G ` implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & x = Product (F |^ I) ) ) ::_thesis: ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & x = Product (F |^ I) ) implies x in G ` )
proof
assume A1: x in G ` ; ::_thesis: ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & x = Product (F |^ I) )
then x in G by GROUP_2:40;
then reconsider a = x as Element of G by STRUCT_0:def_5;
ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & a = Product (F |^ I) ) by A1, GROUP_4:28;
hence ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & x = Product (F |^ I) ) ; ::_thesis: verum
end;
given F being FinSequence of the carrier of G, I being FinSequence of INT such that A2: ( len F = len I & rng F c= commutators G & x = Product (F |^ I) ) ; ::_thesis: x in G `
thus x in G ` by A2, GROUP_4:28; ::_thesis: verum
end;
theorem Th74: :: GROUP_5:74
for G being strict Group
for a, b being Element of G holds [.a,b.] in G `
proof
let G be strict Group; ::_thesis: for a, b being Element of G holds [.a,b.] in G `
let a, b be Element of G; ::_thesis: [.a,b.] in G `
( a in (Omega). G & b in (Omega). G ) by STRUCT_0:def_5;
hence [.a,b.] in G ` by Th65; ::_thesis: verum
end;
theorem :: GROUP_5:75
for G being strict Group holds
( G is commutative Group iff G ` = (1). G )
proof
let G be strict Group; ::_thesis: ( G is commutative Group iff G ` = (1). G )
thus ( G is commutative Group implies G ` = (1). G ) ::_thesis: ( G ` = (1). G implies G is commutative Group )
proof
assume A1: G is commutative Group ; ::_thesis: G ` = (1). G
now__::_thesis:_for_a_being_Element_of_G_st_a_in_G_`_holds_
a_in_(1)._G
let a be Element of G; ::_thesis: ( a in G ` implies a in (1). G )
assume a in G ` ; ::_thesis: a in (1). G
then a in gr {(1_ G)} by A1, Th51;
then a in gr ({(1_ G)} \ {(1_ G)}) by GROUP_4:35;
then a in gr ({} the carrier of G) by XBOOLE_1:37;
hence a in (1). G by GROUP_4:30; ::_thesis: verum
end;
then A2: G ` is Subgroup of (1). G by GROUP_2:58;
(1). G is Subgroup of G ` by GROUP_2:65;
hence G ` = (1). G by A2, GROUP_2:55; ::_thesis: verum
end;
assume A3: G ` = (1). G ; ::_thesis: G is commutative Group
G is commutative
proof
let a, b be Element of G; :: according to GROUP_1:def_12 ::_thesis: a * b = b * a
[.a,b.] in G ` by Th74;
then [.a,b.] = 1_ G by A3, Th1;
hence a * b = b * a by Th36; ::_thesis: verum
end;
hence G is commutative Group ; ::_thesis: verum
end;
theorem :: GROUP_5:76
for G being Group
for H being strict Subgroup of G st Left_Cosets H is finite & index H = 2 holds
G ` is Subgroup of H
proof
let G be Group; ::_thesis: for H being strict Subgroup of G st Left_Cosets H is finite & index H = 2 holds
G ` is Subgroup of H
let H be strict Subgroup of G; ::_thesis: ( Left_Cosets H is finite & index H = 2 implies G ` is Subgroup of H )
assume that
A1: Left_Cosets H is finite and
A2: index H = 2 ; ::_thesis: G ` is Subgroup of H
A3: H is normal Subgroup of G by A1, A2, GROUP_3:128;
now__::_thesis:_for_a_being_Element_of_G_st_a_in_G_`_holds_
a_in_H
let a be Element of G; ::_thesis: ( a in G ` implies a in H )
assume a in G ` ; ::_thesis: a in H
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A4: len F = len I and
A5: rng F c= commutators G and
A6: a = Product (F |^ I) by Th73;
rng F c= carr H
proof
ex B being finite set st
( B = Left_Cosets H & index H = card B ) by A1, GROUP_2:146;
then consider x, y being set such that
x <> y and
A7: Left_Cosets H = {x,y} by A2, CARD_2:60;
x in Left_Cosets H by A7, TARSKI:def_2;
then consider d being Element of G such that
A8: x = d * H by GROUP_2:def_15;
y in Left_Cosets H by A7, TARSKI:def_2;
then consider e being Element of G such that
A9: y = e * H by GROUP_2:def_15;
carr H in Left_Cosets H by GROUP_2:135;
then ( Left_Cosets H = {(carr H),(e * H)} or Left_Cosets H = {(d * H),(carr H)} ) by A7, A8, A9, TARSKI:def_2;
then consider c being Element of G such that
A10: Left_Cosets H = {(carr H),(c * H)} ;
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in rng F or X in carr H )
assume X in rng F ; ::_thesis: X in carr H
then consider a, b being Element of G such that
A11: X = [.a,b.] by A5, Th58;
b in the carrier of G ;
then b in union (Left_Cosets H) by GROUP_2:137;
then A12: b in (carr H) \/ (c * H) by A10, ZFMISC_1:75;
a in the carrier of G ;
then a in union (Left_Cosets H) by GROUP_2:137;
then A13: a in (carr H) \/ (c * H) by A10, ZFMISC_1:75;
now__::_thesis:_X_in_carr_H
percases ( ( a in carr H & b in carr H ) or ( a in carr H & b in c * H ) or ( a in c * H & b in carr H ) or ( a in c * H & b in c * H ) ) by A13, A12, XBOOLE_0:def_3;
suppose ( a in carr H & b in carr H ) ; ::_thesis: X in carr H
then ( a in H & b in H ) by STRUCT_0:def_5;
then X in H by A11, Th38;
hence X in carr H by STRUCT_0:def_5; ::_thesis: verum
end;
suppose ( a in carr H & b in c * H ) ; ::_thesis: X in carr H
then a in H by STRUCT_0:def_5;
then ( a |^ b in H & a " in H ) by A3, Th3, GROUP_2:51;
then (a ") * (a |^ b) in H by GROUP_2:50;
then X in H by A11, Th16;
hence X in carr H by STRUCT_0:def_5; ::_thesis: verum
end;
suppose ( a in c * H & b in carr H ) ; ::_thesis: X in carr H
then A14: b in H by STRUCT_0:def_5;
then b " in H by GROUP_2:51;
then (b ") |^ a in H by A3, Th3;
then ((b ") |^ a) * b in H by A14, GROUP_2:50;
hence X in carr H by A11, STRUCT_0:def_5; ::_thesis: verum
end;
supposeA15: ( a in c * H & b in c * H ) ; ::_thesis: X in carr H
then consider d being Element of G such that
A16: a = c * d and
A17: d in H by GROUP_2:103;
consider e being Element of G such that
A18: b = c * e and
A19: e in H by A15, GROUP_2:103;
e " in H by A19, GROUP_2:51;
then A20: (e ") |^ c in H by A3, Th3;
d " in H by A17, GROUP_2:51;
then A21: (d ") * ((e ") |^ c) in H by A20, GROUP_2:50;
d |^ c in H by A3, A17, Th3;
then A22: (d |^ c) * e in H by A19, GROUP_2:50;
[.a,b.] = ((a ") * (b ")) * (a * b) by Th16
.= (((d ") * (c ")) * (b ")) * ((c * d) * (c * e)) by A16, A18, GROUP_1:17
.= (((d ") * (c ")) * ((e ") * (c "))) * ((c * d) * (c * e)) by A18, GROUP_1:17
.= ((((d ") * (c ")) * (e ")) * (c ")) * ((c * d) * (c * e)) by GROUP_1:def_3
.= ((((d ") * (c ")) * (e ")) * (c ")) * (c * (d * (c * e))) by GROUP_1:def_3
.= (((((d ") * (c ")) * (e ")) * (c ")) * c) * (d * (c * e)) by GROUP_1:def_3
.= ((((d ") * (c ")) * (e ")) * ((c ") * c)) * (d * (c * e)) by GROUP_1:def_3
.= ((((d ") * (c ")) * (e ")) * (1_ G)) * (d * (c * e)) by GROUP_1:def_5
.= ((((d ") * (c ")) * (e ")) * (c * (c "))) * (d * (c * e)) by GROUP_1:def_5
.= (((((d ") * (c ")) * (e ")) * c) * (c ")) * (d * (c * e)) by GROUP_1:def_3
.= ((((d ") * ((c ") * (e "))) * c) * (c ")) * (d * (c * e)) by GROUP_1:def_3
.= (((d ") * ((e ") |^ c)) * (c ")) * (d * (c * e)) by GROUP_1:def_3
.= (((d ") * ((e ") |^ c)) * (c ")) * ((d * c) * e) by GROUP_1:def_3
.= ((d ") * ((e ") |^ c)) * ((c ") * ((d * c) * e)) by GROUP_1:def_3
.= ((d ") * ((e ") |^ c)) * ((c ") * (d * (c * e))) by GROUP_1:def_3
.= ((d ") * ((e ") |^ c)) * (((c ") * d) * (c * e)) by GROUP_1:def_3
.= ((d ") * ((e ") |^ c)) * ((d |^ c) * e) by GROUP_1:def_3 ;
then X in H by A11, A21, A22, GROUP_2:50;
hence X in carr H by STRUCT_0:def_5; ::_thesis: verum
end;
end;
end;
hence X in carr H ; ::_thesis: verum
end;
then a in gr (carr H) by A4, A6, GROUP_4:28;
hence a in H by GROUP_4:31; ::_thesis: verum
end;
hence G ` is Subgroup of H by GROUP_2:58; ::_thesis: verum
end;
begin
definition
let G be Group;
func center G -> strict Subgroup of G means :Def10: :: GROUP_5:def 10
the carrier of it = { a where a is Element of G : for b being Element of G holds a * b = b * a } ;
existence
ex b1 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : for b being Element of G holds a * b = b * a }
proof
defpred S1[ Element of G] means for b being Element of G holds $1 * b = b * $1;
reconsider A = { a where a is Element of G : S1[a] } as Subset of G from DOMAIN_1:sch_7();
A1: now__::_thesis:_for_a,_b_being_Element_of_G_st_a_in_A_&_b_in_A_holds_
a_*_b_in_A
let a, b be Element of G; ::_thesis: ( a in A & b in A implies a * b in A )
assume that
A2: a in A and
A3: b in A ; ::_thesis: a * b in A
consider c being Element of G such that
A4: c = a and
A5: for b being Element of G holds c * b = b * c by A2;
consider d being Element of G such that
A6: d = b and
A7: for a being Element of G holds d * a = a * d by A3;
now__::_thesis:_for_e_being_Element_of_G_holds_(a_*_b)_*_e_=_e_*_(a_*_b)
let e be Element of G; ::_thesis: (a * b) * e = e * (a * b)
thus (a * b) * e = a * (b * e) by GROUP_1:def_3
.= a * (e * d) by A6, A7
.= (a * e) * b by A6, GROUP_1:def_3
.= (e * c) * b by A4, A5
.= e * (a * b) by A4, GROUP_1:def_3 ; ::_thesis: verum
end;
hence a * b in A ; ::_thesis: verum
end;
A8: now__::_thesis:_for_a_being_Element_of_G_st_a_in_A_holds_
a_"_in_A
let a be Element of G; ::_thesis: ( a in A implies a " in A )
assume a in A ; ::_thesis: a " in A
then consider b being Element of G such that
A9: b = a and
A10: for c being Element of G holds b * c = c * b ;
now__::_thesis:_for_c_being_Element_of_G_holds_(a_")_*_c_=_c_*_(a_")
let c be Element of G; ::_thesis: (a ") * c = c * (a ")
thus (a ") * c = (((a ") * c) ") "
.= ((c ") * ((a ") ")) " by GROUP_1:17
.= ((c ") * b) " by A9
.= (b * (c ")) " by A10
.= (((a ") ") * (c ")) " by A9
.= ((c * (a ")) ") " by GROUP_1:17
.= c * (a ") ; ::_thesis: verum
end;
hence a " in A ; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_G_holds_(1__G)_*_b_=_b_*_(1__G)
let b be Element of G; ::_thesis: (1_ G) * b = b * (1_ G)
(1_ G) * b = b by GROUP_1:def_4;
hence (1_ G) * b = b * (1_ G) by GROUP_1:def_4; ::_thesis: verum
end;
then 1_ G in A ;
hence ex b1 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : for b being Element of G holds a * b = b * a } by A1, A8, GROUP_2:52; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : for b being Element of G holds a * b = b * a } & the carrier of b2 = { a where a is Element of G : for b being Element of G holds a * b = b * a } holds
b1 = b2 by GROUP_2:59;
end;
:: deftheorem Def10 defines center GROUP_5:def_10_:_
for G being Group
for b2 being strict Subgroup of G holds
( b2 = center G iff the carrier of b2 = { a where a is Element of G : for b being Element of G holds a * b = b * a } );
theorem Th77: :: GROUP_5:77
for G being Group
for a being Element of G holds
( a in center G iff for b being Element of G holds a * b = b * a )
proof
let G be Group; ::_thesis: for a being Element of G holds
( a in center G iff for b being Element of G holds a * b = b * a )
let a be Element of G; ::_thesis: ( a in center G iff for b being Element of G holds a * b = b * a )
thus ( a in center G implies for b being Element of G holds a * b = b * a ) ::_thesis: ( ( for b being Element of G holds a * b = b * a ) implies a in center G )
proof
assume a in center G ; ::_thesis: for b being Element of G holds a * b = b * a
then a in the carrier of (center G) by STRUCT_0:def_5;
then a in { b where b is Element of G : for c being Element of G holds b * c = c * b } by Def10;
then ex b being Element of G st
( a = b & ( for c being Element of G holds b * c = c * b ) ) ;
hence for b being Element of G holds a * b = b * a ; ::_thesis: verum
end;
assume for b being Element of G holds a * b = b * a ; ::_thesis: a in center G
then a in { c where c is Element of G : for b being Element of G holds c * b = b * c } ;
then a in the carrier of (center G) by Def10;
hence a in center G by STRUCT_0:def_5; ::_thesis: verum
end;
theorem :: GROUP_5:78
for G being Group holds center G is normal Subgroup of G
proof
let G be Group; ::_thesis: center G is normal Subgroup of G
now__::_thesis:_for_a_being_Element_of_G_holds_a_*_(center_G)_c=_(center_G)_*_a
let a be Element of G; ::_thesis: a * (center G) c= (center G) * a
thus a * (center G) c= (center G) * a ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a * (center G) or x in (center G) * a )
assume x in a * (center G) ; ::_thesis: x in (center G) * a
then consider b being Element of G such that
A1: x = a * b and
A2: b in center G by GROUP_2:103;
x = b * a by A1, A2, Th77;
hence x in (center G) * a by A2, GROUP_2:104; ::_thesis: verum
end;
end;
hence center G is normal Subgroup of G by GROUP_3:118; ::_thesis: verum
end;
theorem :: GROUP_5:79
for G being Group
for H being Subgroup of G st H is Subgroup of center G holds
H is normal Subgroup of G
proof
let G be Group; ::_thesis: for H being Subgroup of G st H is Subgroup of center G holds
H is normal Subgroup of G
let H be Subgroup of G; ::_thesis: ( H is Subgroup of center G implies H is normal Subgroup of G )
assume A1: H is Subgroup of center G ; ::_thesis: H is normal Subgroup of G
now__::_thesis:_for_a_being_Element_of_G_holds_H_*_a_c=_a_*_H
let a be Element of G; ::_thesis: H * a c= a * H
thus H * a c= a * H ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H * a or x in a * H )
assume x in H * a ; ::_thesis: x in a * H
then consider b being Element of G such that
A2: x = b * a and
A3: b in H by GROUP_2:104;
b in center G by A1, A3, GROUP_2:40;
then x = a * b by A2, Th77;
hence x in a * H by A3, GROUP_2:103; ::_thesis: verum
end;
end;
hence H is normal Subgroup of G by GROUP_3:119; ::_thesis: verum
end;
theorem :: GROUP_5:80
for G being Group holds center G is commutative
proof
let G be Group; ::_thesis: center G is commutative
let a, b be Element of (center G); :: according to GROUP_1:def_12 ::_thesis: a * b = b * a
reconsider x = a, y = b as Element of G by GROUP_2:42;
A1: a in center G by STRUCT_0:def_5;
thus a * b = x * y by GROUP_2:43
.= y * x by A1, Th77
.= b * a by GROUP_2:43 ; ::_thesis: verum
end;
theorem :: GROUP_5:81
for G being Group
for a being Element of G holds
( a in center G iff con_class a = {a} )
proof
let G be Group; ::_thesis: for a being Element of G holds
( a in center G iff con_class a = {a} )
let a be Element of G; ::_thesis: ( a in center G iff con_class a = {a} )
thus ( a in center G implies con_class a = {a} ) ::_thesis: ( con_class a = {a} implies a in center G )
proof
assume A1: a in center G ; ::_thesis: con_class a = {a}
thus con_class a c= {a} :: according to XBOOLE_0:def_10 ::_thesis: {a} c= con_class a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in con_class a or x in {a} )
assume x in con_class a ; ::_thesis: x in {a}
then consider b being Element of G such that
A2: b = x and
A3: a,b are_conjugated by GROUP_3:80;
consider c being Element of G such that
A4: a = b |^ c by A3, GROUP_3:def_7;
a = (c ") * (b * c) by A4, GROUP_1:def_3;
then c * a = b * c by GROUP_1:13;
then a * c = b * c by A1, Th77;
then a = b by GROUP_1:6;
hence x in {a} by A2, TARSKI:def_1; ::_thesis: verum
end;
a in con_class a by GROUP_3:83;
hence {a} c= con_class a by ZFMISC_1:31; ::_thesis: verum
end;
assume A5: con_class a = {a} ; ::_thesis: a in center G
now__::_thesis:_for_b_being_Element_of_G_holds_a_*_b_=_b_*_a
let b be Element of G; ::_thesis: a * b = b * a
a |^ b in con_class a by GROUP_3:82;
then a |^ b = a by A5, TARSKI:def_1;
then (b ") * (a * b) = a by GROUP_1:def_3;
hence a * b = b * a by GROUP_1:13; ::_thesis: verum
end;
hence a in center G by Th77; ::_thesis: verum
end;
theorem :: GROUP_5:82
for G being strict Group holds
( G is commutative Group iff center G = G )
proof
let G be strict Group; ::_thesis: ( G is commutative Group iff center G = G )
thus ( G is commutative Group implies center G = G ) ::_thesis: ( center G = G implies G is commutative Group )
proof
assume A1: G is commutative Group ; ::_thesis: center G = G
now__::_thesis:_for_a_being_Element_of_G_holds_a_in_center_G
let a be Element of G; ::_thesis: a in center G
for b being Element of G holds a * b = b * a by A1, Lm1;
hence a in center G by Th77; ::_thesis: verum
end;
hence center G = G by GROUP_2:62; ::_thesis: verum
end;
assume A2: center G = G ; ::_thesis: G is commutative Group
G is commutative
proof
let a, b be Element of G; :: according to GROUP_1:def_12 ::_thesis: a * b = b * a
a in G by STRUCT_0:def_5;
hence a * b = b * a by A2, Th77; ::_thesis: verum
end;
hence G is commutative Group ; ::_thesis: verum
end;