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