:: GRNILP_1 semantic presentation begin theorem :: GRNILP_1:1 for G being Group for a, b being Element of G holds a |^ b = a * [.a,b.] proof let G be Group; ::_thesis: for a, b being Element of G holds a |^ b = a * [.a,b.] let a, b be Element of G; ::_thesis: a |^ b = a * [.a,b.] a * [.a,b.] = a * (((a ") * (b ")) * (a * b)) by GROUP_1:def_3 .= a * ((a ") * ((b ") * (a * b))) by GROUP_1:def_3 .= (a * (a ")) * ((b ") * (a * b)) by GROUP_1:def_3 .= (1_ G) * ((b ") * (a * b)) by GROUP_1:def_5 .= (b ") * (a * b) by GROUP_1:def_4 .= ((b ") * a) * b by GROUP_1:def_3 ; hence a |^ b = a * [.a,b.] ; ::_thesis: verum end; theorem :: GRNILP_1:2 for G being Group for a, b being Element of G holds [.a,b.] " = [.a,(b ").] |^ b proof let G be Group; ::_thesis: for a, b being Element of G holds [.a,b.] " = [.a,(b ").] |^ b let a, b be Element of G; ::_thesis: [.a,b.] " = [.a,(b ").] |^ b thus [.a,b.] " = (((a ") * (b ")) * (a * b)) " by GROUP_1:def_3 .= ((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)) by GROUP_1:def_3 .= (b ") * (((a ") * b) * a) by GROUP_1:def_3 .= ((b ") * (((a ") * b) * a)) * (1_ G) by GROUP_1:def_4 .= ((b ") * (((a ") * b) * a)) * ((b ") * b) by GROUP_1:def_5 .= (((b ") * (((a ") * b) * a)) * (b ")) * b by GROUP_1:def_3 .= [.a,(b ").] |^ b by GROUP_1:def_3 ; ::_thesis: verum end; theorem :: GRNILP_1:3 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 ") * (b ")) * (a * b)) " by GROUP_1:def_3 .= ((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)) by GROUP_1:def_3 .= (b ") * (((a ") * b) * a) by GROUP_1:def_3 .= (1_ G) * ((b ") * (((a ") * b) * a)) by GROUP_1:def_4 .= ((a ") * a) * ((b ") * (((a ") * b) * a)) by GROUP_1:def_5 .= (a ") * (a * ((b ") * (((a ") * b) * a))) by GROUP_1:def_3 .= (a ") * ((a * (b ")) * (((a ") * b) * a)) by GROUP_1:def_3 .= (a ") * (((a * (b ")) * ((a ") * b)) * a) by GROUP_1:def_3 .= ((a ") * ((a * (b ")) * ((a ") * b))) * a by GROUP_1:def_3 .= [.(a "),b.] |^ a by GROUP_5:16 ; ::_thesis: verum end; theorem Th4: :: GRNILP_1:4 for G being Group for a, b being Element of G holds ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b proof let G be Group; ::_thesis: for a, b being Element of G holds ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b let a, b be Element of G; ::_thesis: ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b thus ([.a,(b ").] |^ b) " = ([.a,(b ").] ") |^ b by GROUP_3:26 .= [.(b "),a.] |^ b by GROUP_5:22 ; ::_thesis: verum end; theorem Th5: :: GRNILP_1:5 for G being Group for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).] proof let G be Group; ::_thesis: for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).] let a, b, c be Element of G; ::_thesis: [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).] A1: [.a,(b "),c.] |^ b = ((b ") * ((((([.a,(b ").] ") * (1_ G)) * (c ")) * [.a,(b ").]) * c)) * b by GROUP_1:def_4 .= ((b ") * ((((([.a,(b ").] ") * (b * (b "))) * (c ")) * [.a,(b ").]) * c)) * b by GROUP_1:def_5 .= ((b ") * (((((([.a,(b ").] ") * b) * (b ")) * (c ")) * [.a,(b ").]) * c)) * b by GROUP_1:def_3 .= ((b ") * ((((([.a,(b ").] ") * b) * (b ")) * (c ")) * ([.a,(b ").] * c))) * b by GROUP_1:def_3 .= ((b ") * (((([.a,(b ").] ") * b) * (b ")) * ((c ") * ([.a,(b ").] * c)))) * b by GROUP_1:def_3 .= ((b ") * ((([.a,(b ").] ") * b) * ((b ") * ((c ") * ([.a,(b ").] * c))))) * b by GROUP_1:def_3 .= (((b ") * (([.a,(b ").] ") * b)) * ((b ") * ((c ") * ([.a,(b ").] * c)))) * b by GROUP_1:def_3 .= ((([.a,(b ").] ") |^ b) * ((b ") * ((c ") * ([.a,(b ").] * c)))) * b by GROUP_1:def_3 .= (([.a,(b ").] ") |^ b) * (((b ") * ((c ") * ([.a,(b ").] * c))) * b) by GROUP_1:def_3 .= (([.a,(b ").] ") |^ b) * (([.a,(b ").] |^ c) |^ b) by GROUP_1:def_3 .= ([.(b "),a.] |^ b) * (([.a,(b ").] |^ c) |^ b) by GROUP_5:22 .= ([.(b "),a.] |^ b) * ([.a,(b ").] |^ (c * b)) by GROUP_3:24 ; [.([.a,(b ").] |^ b),(c |^ b).] = ((([.(b "),a.] |^ b) * ((c |^ b) ")) * ([.a,(b ").] |^ b)) * (c |^ b) by Th4 .= ((([.(b "),a.] |^ b) * ((c ") |^ b)) * ([.a,(b ").] |^ b)) * (c |^ b) by GROUP_3:26 .= ((([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * b)) * ((b ") * (c * b)) by GROUP_1:def_3 .= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * ((((b ") * [.a,(b ").]) * b) * ((b ") * (c * b))) by GROUP_1:def_3 .= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * (b * ((b ") * (c * b)))) by GROUP_1:def_3 .= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * ((b * (b ")) * (c * b))) by GROUP_1:def_3 .= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * ((1_ G) * (c * b))) by GROUP_1:def_5 .= (([.(b "),a.] |^ b) * (((b ") * (c ")) * b)) * (((b ") * [.a,(b ").]) * (c * b)) by GROUP_1:def_4 .= ([.(b "),a.] |^ b) * ((((b ") * (c ")) * b) * (((b ") * [.a,(b ").]) * (c * b))) by GROUP_1:def_3 .= ([.(b "),a.] |^ b) * (((b ") * (c ")) * (b * (((b ") * [.a,(b ").]) * (c * b)))) by GROUP_1:def_3 .= ([.(b "),a.] |^ b) * (((b ") * (c ")) * ((b * ((b ") * [.a,(b ").])) * (c * b))) by GROUP_1:def_3 .= ([.(b "),a.] |^ b) * (((b ") * (c ")) * (((b * (b ")) * [.a,(b ").]) * (c * b))) by GROUP_1:def_3 .= ([.(b "),a.] |^ b) * (((b ") * (c ")) * (((1_ G) * [.a,(b ").]) * (c * b))) by GROUP_1:def_5 .= ([.(b "),a.] |^ b) * (((b ") * (c ")) * ([.a,(b ").] * (c * b))) by GROUP_1:def_4 .= ([.(b "),a.] |^ b) * ((((b ") * (c ")) * [.a,(b ").]) * (c * b)) by GROUP_1:def_3 .= ([.(b "),a.] |^ b) * ([.a,(b ").] |^ (c * b)) by GROUP_1:17 ; hence [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).] by A1; ::_thesis: verum end; theorem Th6: :: GRNILP_1:6 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 = (b ") * (((((a ") * ((b ") ")) * a) * (b ")) * b) by GROUP_1:def_3 .= (b ") * ((((a ") * ((b ") ")) * a) * ((b ") * b)) by GROUP_1:def_3 .= (b ") * ((((a ") * ((b ") ")) * a) * (1_ G)) by GROUP_1:def_5 .= (b ") * (((a ") * ((b ") ")) * a) by GROUP_1:def_4 .= (b ") * ((a ") * (b * a)) by GROUP_1:def_3 .= ((b ") * (a ")) * (b * a) by GROUP_1:def_3 .= (((b ") * (a ")) * b) * a by GROUP_1:def_3 .= [.b,a.] ; ::_thesis: verum end; theorem Th7: :: GRNILP_1:7 for G being Group for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.b,a,(c |^ b).] proof let G be Group; ::_thesis: for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.b,a,(c |^ b).] let a, b, c be Element of G; ::_thesis: [.a,(b "),c.] |^ b = [.b,a,(c |^ b).] [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).] by Th5; hence [.a,(b "),c.] |^ b = [.b,a,(c |^ b).] by Th6; ::_thesis: verum end; theorem :: GRNILP_1:8 for G being Group for a, b, c being Element of G holds ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G proof let G be Group; ::_thesis: for a, b, c being Element of G holds ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G let a, b, c be Element of G; ::_thesis: ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G ( [.a,b,(c |^ a).] = [.b,(a "),c.] |^ a & [.c,a,(b |^ c).] = [.a,(c "),b.] |^ c & [.b,c,(a |^ b).] = [.c,(b "),a.] |^ b ) by Th7; hence ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G by GROUP_5:46; ::_thesis: verum end; theorem Th9: :: GRNILP_1:9 for G being Group for A, B being Subgroup of G holds [.A,B.] is Subgroup of [.B,A.] proof let G be Group; ::_thesis: for A, B being Subgroup of G holds [.A,B.] is Subgroup of [.B,A.] let A, B be Subgroup of G; ::_thesis: [.A,B.] is Subgroup of [.B,A.] now__::_thesis:_for_a_being_Element_of_G_st_a_in_[.A,B.]_holds_ a_in_[.B,A.] let a be Element of G; ::_thesis: ( a in [.A,B.] implies a in [.B,A.] ) assume a in [.A,B.] ; ::_thesis: a in [.B,A.] 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 (A,B) and A2: a = Product (F |^ I) by GROUP_5:61; 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 F1 = Seg (len F) by A3, FINSEQ_1:def_3; deffunc H2( Nat) -> Element of INT = @ (- (@ (I /. $1))); consider I1 being FinSequence of INT such that A6: len I1 = len F and A7: for k being Nat st k in dom I1 holds I1 . k = H2(k) from FINSEQ_2:sch_1(); A8: dom F = Seg (len F) by FINSEQ_1:def_3; A9: dom F1 = dom F by A3, FINSEQ_3:29; A10: dom I1 = dom F by A6, FINSEQ_3:29; set J = F1 |^ I1; A11: ( len (F1 |^ I1) = len F & len (F |^ I) = len F ) by A3, GROUP_4:def_3; then A12: dom (F |^ I) = Seg (len F) by FINSEQ_1:def_3; 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 A13: k in dom (F |^ I) ; ::_thesis: (F |^ I) . k = (F1 |^ I1) . k then A14: k in dom F by A12, FINSEQ_1:def_3; ( (F1 |^ I1) . k = (F1 /. k) |^ (@ (I1 /. k)) & F1 /. k = F1 . k & F1 . k = (F /. k) " & I1 . k = I1 /. k & @ (I1 /. k) = I1 /. k & I1 . k = @ (- (@ (I /. k))) & @ (- (@ (I /. k))) = - (@ (I /. k)) ) by A4, A7, A8, A9, A10, A13, A12, GROUP_4:def_3, PARTFUN1:def_6; then (F1 |^ I1) . k = (((F /. k) ") |^ (@ (I /. k))) " by GROUP_1:36 .= (((F /. k) |^ (@ (I /. k))) ") " by GROUP_1:37 .= (F /. k) |^ (@ (I /. k)) ; hence (F |^ I) . k = (F1 |^ I1) . k by A14, GROUP_4:def_3; ::_thesis: verum end; then A15: F1 |^ I1 = F |^ I by A11, FINSEQ_2:9; rng F1 c= commutators (B,A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F1 or x in commutators (B,A) ) assume x in rng F1 ; ::_thesis: x in commutators (B,A) then consider y being set such that A16: y in dom F1 and A17: F1 . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A16; y in dom F by A3, A16, FINSEQ_3:29; then F . y in rng F by FUNCT_1:def_3; then consider b, c being Element of G such that A18: F . y = [.b,c.] and A19: ( b in A & c in B ) by A1, GROUP_5:52; ( x = (F /. y) " & F /. y = F . y ) by A16, A4, A8, A17, A5, PARTFUN1:def_6; then x = [.c,b.] by A18, GROUP_5:22; hence x in commutators (B,A) by A19, GROUP_5:52; ::_thesis: verum end; hence a in [.B,A.] by A2, A3, A6, A15, GROUP_5:61; ::_thesis: verum end; hence [.A,B.] is Subgroup of [.B,A.] by GROUP_2:58; ::_thesis: verum end; definition let G be Group; let A, B be Subgroup of G; :: original: [. redefine func[.A,B.] -> Subgroup of G; commutativity for A, B being Subgroup of G holds [.A,B.] = [.B,A.] proof let A, B be Subgroup of G; ::_thesis: [.A,B.] = [.B,A.] ( [.A,B.] is Subgroup of [.B,A.] & [.B,A.] is Subgroup of [.A,B.] ) by Th9; hence [.A,B.] = [.B,A.] by GROUP_2:55; ::_thesis: verum end; end; theorem Th10: :: GRNILP_1:10 for G being Group for B, A being Subgroup of G st B is Subgroup of A holds commutators (A,B) c= carr A proof let G be Group; ::_thesis: for B, A being Subgroup of G st B is Subgroup of A holds commutators (A,B) c= carr A let B, A be Subgroup of G; ::_thesis: ( B is Subgroup of A implies commutators (A,B) c= carr A ) assume A1: B is Subgroup of A ; ::_thesis: commutators (A,B) c= carr A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in commutators (A,B) or x in carr A ) assume x in commutators (A,B) ; ::_thesis: x in carr A then consider a, b being Element of G such that A2: ( x = [.a,b.] & a in A & b in B ) by GROUP_5:52; A3: b in A by A1, A2, GROUP_2:40; then A4: a * b in A by A2, GROUP_2:50; ( a " in A & b " in A ) by A2, A3, GROUP_2:51; then (a ") * (b ") in A by GROUP_2:50; then A5: ((a ") * (b ")) * (a * b) in A by A4, GROUP_2:50; [.a,b.] = ((a ") * (b ")) * (a * b) by GROUP_1:def_3; hence x in carr A by A2, A5, STRUCT_0:def_5; ::_thesis: verum end; Lm1: for G being Group for A being Subgroup of G holds gr (carr A) is Subgroup of A proof let G be Group; ::_thesis: for A being Subgroup of G holds gr (carr A) is Subgroup of A let A be Subgroup of G; ::_thesis: gr (carr A) is Subgroup of A set A9 = multMagma(# the carrier of A, the multF of A #); ( the carrier of multMagma(# the carrier of A, the multF of A #) c= the carrier of G & the multF of multMagma(# the carrier of A, the multF of A #) = the multF of G || the carrier of A ) by GROUP_2:def_5; then reconsider A9 = multMagma(# the carrier of A, the multF of A #) as strict Subgroup of G by GROUP_2:def_5; A1: gr (carr A) is Subgroup of A9 by GROUP_4:def_4; A9 is Subgroup of A by GROUP_2:57; hence gr (carr A) is Subgroup of A by A1, GROUP_2:56; ::_thesis: verum end; theorem Th11: :: GRNILP_1:11 for G being Group for B, A being Subgroup of G st B is Subgroup of A holds [.A,B.] is Subgroup of A proof let G be Group; ::_thesis: for B, A being Subgroup of G st B is Subgroup of A holds [.A,B.] is Subgroup of A let B, A be Subgroup of G; ::_thesis: ( B is Subgroup of A implies [.A,B.] is Subgroup of A ) A1: gr (carr A) is Subgroup of A by Lm1; assume B is Subgroup of A ; ::_thesis: [.A,B.] is Subgroup of A then commutators (A,B) c= carr A by Th10; then [.A,B.] is Subgroup of gr (carr A) by GROUP_4:32; hence [.A,B.] is Subgroup of A by A1, GROUP_2:56; ::_thesis: verum end; theorem :: GRNILP_1:12 for G being Group for B, A being Subgroup of G st B is Subgroup of A holds [.B,A.] is Subgroup of A by Th11; Lm2: for G being Group for A being Subgroup of G holds A is Subgroup of (Omega). G proof let G be Group; ::_thesis: for A being Subgroup of G holds A is Subgroup of (Omega). G let A be Subgroup of G; ::_thesis: A is Subgroup of (Omega). G dom the multF of G c= [: the carrier of G, the carrier of G:] ; then the multF of G = the multF of ((Omega). G) || the carrier of ((Omega). G) by RELAT_1:68; then G is Subgroup of (Omega). G by GROUP_2:def_5; hence A is Subgroup of (Omega). G by GROUP_2:56; ::_thesis: verum end; theorem :: GRNILP_1:13 for G being Group for H1, H2, H being Subgroup of G st [.H1,((Omega). G).] is Subgroup of H2 holds [.(H1 /\ H),H.] is Subgroup of H2 /\ H proof let G be Group; ::_thesis: for H1, H2, H being Subgroup of G st [.H1,((Omega). G).] is Subgroup of H2 holds [.(H1 /\ H),H.] is Subgroup of H2 /\ H let H1, H2, H be Subgroup of G; ::_thesis: ( [.H1,((Omega). G).] is Subgroup of H2 implies [.(H1 /\ H),H.] is Subgroup of H2 /\ H ) assume A1: [.H1,((Omega). G).] is Subgroup of H2 ; ::_thesis: [.(H1 /\ H),H.] is Subgroup of H2 /\ H H1 /\ H is Subgroup of H by GROUP_2:88; then A2: [.(H1 /\ H),H.] is Subgroup of H by Th11; A3: H is Subgroup of (Omega). G by Lm2; H1 /\ H is Subgroup of H1 by GROUP_2:88; then [.(H1 /\ H),H.] is Subgroup of [.H1,((Omega). G).] by A3, GROUP_5:66; then [.(H1 /\ H),H.] is Subgroup of H2 by A1, GROUP_2:56; hence [.(H1 /\ H),H.] is Subgroup of H2 /\ H by A2, GROUP_2:91; ::_thesis: verum end; theorem :: GRNILP_1:14 for G being Group for H1, H2 being Subgroup of G holds [.H1,H2.] is Subgroup of [.H1,((Omega). G).] proof let G be Group; ::_thesis: for H1, H2 being Subgroup of G holds [.H1,H2.] is Subgroup of [.H1,((Omega). G).] let H1, H2 be Subgroup of G; ::_thesis: [.H1,H2.] is Subgroup of [.H1,((Omega). G).] A1: H2 is Subgroup of (Omega). G by Lm2; H1 is Subgroup of H1 by GROUP_2:54; hence [.H1,H2.] is Subgroup of [.H1,((Omega). G).] by A1, GROUP_5:66; ::_thesis: verum end; Lm3: for G being Group for H being Subgroup of G for N being normal Subgroup of G holds [.N,H.] is Subgroup of N proof let G be Group; ::_thesis: for H being Subgroup of G for N being normal Subgroup of G holds [.N,H.] is Subgroup of N let H be Subgroup of G; ::_thesis: for N being normal Subgroup of G holds [.N,H.] is Subgroup of N let N be normal Subgroup of G; ::_thesis: [.N,H.] is Subgroup of N ( the carrier of N c= the carrier of G & the multF of N = the multF of G || the carrier of N ) by GROUP_2:def_5; then reconsider N9 = multMagma(# the carrier of N, the multF of N #) as strict Subgroup of G by GROUP_2:def_5; now__::_thesis:_for_a_being_Element_of_G_holds_N9_|^_a_=_multMagma(#_the_carrier_of_N9,_the_multF_of_N9_#) let a be Element of G; ::_thesis: N9 |^ a = multMagma(# the carrier of N9, the multF of N9 #) the carrier of (N |^ a) = (carr N) |^ a by GROUP_3:def_6 .= (carr N9) |^ a .= the carrier of (N9 |^ a) by GROUP_3:def_6 ; hence N9 |^ a = N |^ a by GROUP_2:59 .= multMagma(# the carrier of N9, the multF of N9 #) by GROUP_3:def_13 ; ::_thesis: verum end; then reconsider N9 = N9 as strict normal Subgroup of G by GROUP_3:def_13; [.N9,H.] = [.N,H.] ; then A1: [.N,H.] is Subgroup of N9 by GROUP_5:67; N9 is Subgroup of N by GROUP_2:57; hence [.N,H.] is Subgroup of N by A1, GROUP_2:56; ::_thesis: verum end; theorem Th15: :: GRNILP_1:15 for G being Group for A being Subgroup of G holds ( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A ) proof let G be Group; ::_thesis: for A being Subgroup of G holds ( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A ) let A be Subgroup of G; ::_thesis: ( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A ) thus ( A is normal Subgroup of G implies [.A,((Omega). G).] is Subgroup of A ) by Lm3; ::_thesis: ( [.A,((Omega). G).] is Subgroup of A implies A is normal Subgroup of G ) assume A1: [.A,((Omega). G).] is Subgroup of A ; ::_thesis: A is normal Subgroup of G for b being Element of G holds b * A c= A * b proof let b be Element of G; ::_thesis: b * A c= A * b let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in b * A or x in A * b ) assume A2: x in b * A ; ::_thesis: x in A * b then reconsider x = x as Element of G ; consider Z being Element of G such that A3: ( x = b * Z & Z in A ) by A2, GROUP_2:103; A4: Z " in A by A3, GROUP_2:51; b " in (Omega). G by STRUCT_0:def_5; then [.(b "),(Z ").] in [.((Omega). G),A.] by A4, GROUP_5:65; then [.(b "),(Z ").] in A by A1, GROUP_2:40; then A5: (((b * Z) * (b ")) * (Z ")) * Z in A by A3, GROUP_2:50; A6: (((b * Z) * (b ")) * (Z ")) * Z = ((b * Z) * (b ")) * ((Z ") * Z) by GROUP_1:def_3 .= ((b * Z) * (b ")) * (1_ G) by GROUP_1:def_5 .= (b * Z) * (b ") by GROUP_1:def_4 ; ((b * Z) * (b ")) * b = (b * Z) * ((b ") * b) by GROUP_1:def_3 .= (b * Z) * (1_ G) by GROUP_1:def_5 .= b * Z by GROUP_1:def_4 ; hence x in A * b by A3, A5, A6, GROUP_2:104; ::_thesis: verum end; hence A is normal Subgroup of G by GROUP_3:118; ::_thesis: verum end; definition let G be Group; func the_normal_subgroups_of G -> set means :Def1: :: GRNILP_1:def 1 for x being set holds ( x in it iff x is strict normal Subgroup of G ); existence ex b1 being set st for x being set holds ( x in b1 iff x is strict normal Subgroup of G ) proof defpred S1[ set , set ] means ex H being strict normal Subgroup of G st ( $2 = H & $1 = the carrier of H ); defpred S2[ set ] means ex H being strict normal Subgroup of G st $1 = the carrier of H; consider B being set such that A1: for x being set holds ( x in B iff ( x in bool the carrier of G & S2[x] ) ) from XBOOLE_0:sch_1(); A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds y1 = y2 by GROUP_2:59; consider f being Function such that A3: for x, y being set holds ( [x,y] in f iff ( x in B & S1[x,y] ) ) from FUNCT_1:sch_1(A2); for x being set holds ( x in B iff ex y being set st [x,y] in f ) proof let x be set ; ::_thesis: ( x in B iff ex y being set st [x,y] in f ) thus ( x in B implies ex y being set st [x,y] in f ) ::_thesis: ( ex y being set st [x,y] in f implies x in B ) proof assume A4: x in B ; ::_thesis: ex y being set st [x,y] in f then consider H being strict normal Subgroup of G such that A5: x = the carrier of H by A1; reconsider y = H as set ; take y ; ::_thesis: [x,y] in f thus [x,y] in f by A3, A4, A5; ::_thesis: verum end; given y being set such that A6: [x,y] in f ; ::_thesis: x in B thus x in B by A3, A6; ::_thesis: verum end; then A7: B = dom f by XTUPLE_0:def_12; for y being set holds ( y in rng f iff y is strict normal Subgroup of G ) proof let y be set ; ::_thesis: ( y in rng f iff y is strict normal Subgroup of G ) thus ( y in rng f implies y is strict normal Subgroup of G ) ::_thesis: ( y is strict normal Subgroup of G implies y in rng f ) proof assume y in rng f ; ::_thesis: y is strict normal Subgroup of G then consider x being set such that A8: ( x in dom f & y = f . x ) by FUNCT_1:def_3; [x,y] in f by A8, FUNCT_1:def_2; then ex H being strict normal Subgroup of G st ( y = H & x = the carrier of H ) by A3; hence y is strict normal Subgroup of G ; ::_thesis: verum end; assume y is strict normal Subgroup of G ; ::_thesis: y in rng f then reconsider H = y as strict normal Subgroup of G ; reconsider x = the carrier of H as set ; the carrier of H c= the carrier of G by GROUP_2:def_5; then A9: x in dom f by A1, A7; then [x,y] in f by A3, A7; then y = f . x by A9, FUNCT_1:def_2; hence y in rng f by A9, FUNCT_1:def_3; ::_thesis: verum end; hence ex b1 being set st for x being set holds ( x in b1 iff x is strict normal Subgroup of G ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is strict normal Subgroup of G ) ) & ( for x being set holds ( x in b2 iff x is strict normal Subgroup of G ) ) holds b1 = b2 proof defpred S1[ set ] means $1 is strict normal Subgroup of G; let A1, A2 be set ; ::_thesis: ( ( for x being set holds ( x in A1 iff x is strict normal Subgroup of G ) ) & ( for x being set holds ( x in A2 iff x is strict normal Subgroup of G ) ) implies A1 = A2 ) assume A10: for x being set holds ( x in A1 iff S1[x] ) ; ::_thesis: ( ex x being set st ( ( x in A2 implies x is strict normal Subgroup of G ) implies ( x is strict normal Subgroup of G & not x in A2 ) ) or A1 = A2 ) assume A11: for x being set holds ( x in A2 iff S1[x] ) ; ::_thesis: A1 = A2 thus A1 = A2 from XBOOLE_0:sch_2(A10, A11); ::_thesis: verum end; end; :: deftheorem Def1 defines the_normal_subgroups_of GRNILP_1:def_1_:_ for G being Group for b2 being set holds ( b2 = the_normal_subgroups_of G iff for x being set holds ( x in b2 iff x is strict normal Subgroup of G ) ); registration let G be Group; cluster the_normal_subgroups_of G -> non empty ; coherence not the_normal_subgroups_of G is empty proof the strict normal Subgroup of G in the_normal_subgroups_of G by Def1; hence not the_normal_subgroups_of G is empty ; ::_thesis: verum end; end; theorem Th16: :: GRNILP_1:16 for G being Group for F being FinSequence of the_normal_subgroups_of G for j being Element of NAT st j in dom F holds F . j is strict normal Subgroup of G proof let G be Group; ::_thesis: for F being FinSequence of the_normal_subgroups_of G for j being Element of NAT st j in dom F holds F . j is strict normal Subgroup of G let F be FinSequence of the_normal_subgroups_of G; ::_thesis: for j being Element of NAT st j in dom F holds F . j is strict normal Subgroup of G let j be Element of NAT ; ::_thesis: ( j in dom F implies F . j is strict normal Subgroup of G ) assume j in dom F ; ::_thesis: F . j is strict normal Subgroup of G then F . j in rng F by FUNCT_1:3; hence F . j is strict normal Subgroup of G by Def1; ::_thesis: verum end; theorem Th17: :: GRNILP_1:17 for G being Group holds the_normal_subgroups_of G c= Subgroups G proof let G be Group; ::_thesis: the_normal_subgroups_of G c= Subgroups G let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_normal_subgroups_of G or x in Subgroups G ) assume x in the_normal_subgroups_of G ; ::_thesis: x in Subgroups G then x is strict normal Subgroup of G by Def1; hence x in Subgroups G by GROUP_3:def_1; ::_thesis: verum end; theorem Th18: :: GRNILP_1:18 for G being Group for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G proof let G be Group; ::_thesis: for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G let F be FinSequence of the_normal_subgroups_of G; ::_thesis: F is FinSequence of Subgroups G the_normal_subgroups_of G c= Subgroups G by Th17; then rng F c= Subgroups G by XBOOLE_1:1; hence F is FinSequence of Subgroups G by FINSEQ_1:def_4; ::_thesis: verum end; definition let IT be Group; attrIT is nilpotent means :Def2: :: GRNILP_1:def 2 ex F being FinSequence of the_normal_subgroups_of IT st ( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (IT ./. G2) ) ) ); end; :: deftheorem Def2 defines nilpotent GRNILP_1:def_2_:_ for IT being Group holds ( IT is nilpotent iff ex F being FinSequence of the_normal_subgroups_of IT st ( len F > 0 & F . 1 = (Omega). IT & F . (len F) = (1). IT & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of IT st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (IT ./. G2) ) ) ) ); registration cluster non empty strict unital Group-like associative nilpotent for multMagma ; existence ex b1 being Group st ( b1 is nilpotent & b1 is strict ) proof set G = the Group; take H = (1). the Group; ::_thesis: ( H is nilpotent & H is strict ) thus H is nilpotent ::_thesis: H is strict proof rng <*H*> c= the_normal_subgroups_of H proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng <*H*> or x in the_normal_subgroups_of H ) assume A1: x in rng <*H*> ; ::_thesis: x in the_normal_subgroups_of H rng <*H*> = {H} by FINSEQ_1:39; then x = H by A1, TARSKI:def_1; then x is strict normal Subgroup of H by GROUP_2:54, GROUP_6:8; hence x in the_normal_subgroups_of H by Def1; ::_thesis: verum end; then reconsider F = <*H*> as FinSequence of the_normal_subgroups_of H by FINSEQ_1:def_4; take F ; :: according to GRNILP_1:def_2 ::_thesis: ( len F > 0 & F . 1 = (Omega). H & F . (len F) = (1). H & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) ) A2: len F = 1 by FINSEQ_1:39; then A3: F . (len F) = H by FINSEQ_1:40 .= (1). H by GROUP_2:63 ; for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) proof let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) let G1, G2 be strict normal Subgroup of H; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) assume ( G1 = F . i & G2 = F . (i + 1) ) ; ::_thesis: ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) dom F = {1} by A2, FINSEQ_1:2, FINSEQ_1:def_3; then ( i = 1 & i + 1 = 1 ) by A4, TARSKI:def_1; hence ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ; ::_thesis: verum end; hence ( len F > 0 & F . 1 = (Omega). H & F . (len F) = (1). H & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of H st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) ) by A3, FINSEQ_1:40; ::_thesis: verum end; thus H is strict ; ::_thesis: verum end; end; theorem Th19: :: GRNILP_1:19 for G being Group for G1 being Subgroup of G for N being strict normal Subgroup of G st N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) holds [.G1,((Omega). G).] is Subgroup of N proof let G be Group; ::_thesis: for G1 being Subgroup of G for N being strict normal Subgroup of G st N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) holds [.G1,((Omega). G).] is Subgroup of N let G1 be Subgroup of G; ::_thesis: for N being strict normal Subgroup of G st N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) holds [.G1,((Omega). G).] is Subgroup of N let N be strict normal Subgroup of G; ::_thesis: ( N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) implies [.G1,((Omega). G).] is Subgroup of N ) assume that A1: N is Subgroup of G1 and A2: G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) ; ::_thesis: [.G1,((Omega). G).] is Subgroup of N A3: (G1,N) `*` = N by A1, GROUP_6:def_1; reconsider J = G1 ./. ((G1,N) `*`) as Subgroup of G ./. N by A1, GROUP_6:28; reconsider I = N as normal Subgroup of G1 by A3; A4: commutators (G1,((Omega). G)) c= carr N proof now__::_thesis:_for_x_being_Element_of_G_st_x_in_commutators_(G1,((Omega)._G))_holds_ x_in_carr_N let x be Element of G; ::_thesis: ( x in commutators (G1,((Omega). G)) implies x in carr N ) assume x in commutators (G1,((Omega). G)) ; ::_thesis: x in carr N then consider a, b being Element of G such that A5: ( x = [.a,b.] & a in G1 & b in (Omega). G ) by GROUP_5:52; reconsider c = a as Element of G1 by A5, STRUCT_0:def_5; reconsider S9 = c * I as Element of J by A3, GROUP_6:22; A6: S9 in J by STRUCT_0:def_5; reconsider T = b * N as Element of (G ./. N) by GROUP_6:14; reconsider d = c as Element of G ; d * N = c * I by GROUP_6:2; then reconsider S = S9 as Element of (G ./. N) by GROUP_6:14; S in center (G ./. N) by A2, A6, GROUP_2:40; then A7: S * T = T * S by GROUP_5:77; A8: ( S = d * N & T = b * N & @ S = S & @ T = T ) by GROUP_6:2; then A9: S * T = (d * N) * (b * N) by GROUP_6:def_3 .= d * (N * (b * N)) by GROUP_3:10 .= d * ((N * b) * N) by GROUP_3:13 .= d * ((b * N) * N) by GROUP_3:117 .= d * (b * N) by GROUP_6:5 .= (d * b) * N by GROUP_2:105 ; T * S = (b * N) * (d * N) by A8, GROUP_6:def_3 .= b * (N * (d * N)) by GROUP_3:10 .= b * ((N * d) * N) by GROUP_3:13 .= b * ((d * N) * N) by GROUP_3:117 .= b * (d * N) by GROUP_6:5 .= (b * d) * N by GROUP_2:105 ; then A10: ((d ") * (b ")) * ((d * b) * N) = (((d ") * (b ")) * (b * d)) * N by A7, A9, GROUP_2:105 .= ((d ") * ((b ") * (b * d))) * N by GROUP_1:def_3 .= ((d ") * (((b ") * b) * d)) * N by GROUP_1:def_3 .= ((d ") * ((1_ G) * d)) * N by GROUP_1:def_5 .= ((d ") * d) * N by GROUP_1:def_4 .= (1_ G) * N by GROUP_1:def_5 .= carr N by GROUP_2:109 ; ((d ") * (b ")) * ((d * b) * N) = (((d ") * (b ")) * (d * b)) * N by GROUP_2:105 .= [.d,b.] * N by GROUP_5:16 ; then [.d,b.] in N by A10, GROUP_2:113; hence x in carr N by A5, STRUCT_0:def_5; ::_thesis: verum end; hence commutators (G1,((Omega). G)) c= carr N by SUBSET_1:2; ::_thesis: verum end; gr (carr N) = N by GROUP_4:31; hence [.G1,((Omega). G).] is Subgroup of N by A4, GROUP_4:32; ::_thesis: verum end; theorem Th20: :: GRNILP_1:20 for G being Group for G1 being Subgroup of G for N being normal Subgroup of G st N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N holds G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) proof let G be Group; ::_thesis: for G1 being Subgroup of G for N being normal Subgroup of G st N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N holds G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) let G1 be Subgroup of G; ::_thesis: for N being normal Subgroup of G st N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N holds G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) let N be normal Subgroup of G; ::_thesis: ( N is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of N implies G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) ) assume that A1: N is strict Subgroup of G1 and A2: [.G1,((Omega). G).] is strict Subgroup of N ; ::_thesis: G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) A3: (G1,N) `*` = N by A1, GROUP_6:def_1; reconsider J = G1 ./. ((G1,N) `*`) as Subgroup of G ./. N by A1, GROUP_6:28; reconsider I = N as normal Subgroup of G1 by A3; for S1 being Element of (G ./. N) st S1 in J holds S1 in center (G ./. N) proof let S1 be Element of (G ./. N); ::_thesis: ( S1 in J implies S1 in center (G ./. N) ) assume A4: S1 in J ; ::_thesis: S1 in center (G ./. N) for S being Element of (G ./. N) holds S1 * S = S * S1 proof let S be Element of (G ./. N); ::_thesis: S1 * S = S * S1 consider a being Element of G such that A5: ( S = a * N & S = N * a ) by GROUP_6:21; consider c being Element of G1 such that A6: ( S1 = c * I & S1 = I * c ) by A3, A4, GROUP_6:23; reconsider d = c as Element of G by GROUP_2:42; A7: d in G1 by STRUCT_0:def_5; a in (Omega). G by STRUCT_0:def_5; then [.d,a.] in [.G1,((Omega). G).] by A7, GROUP_5:65; then A8: [.d,a.] in N by A2, GROUP_2:40; A9: ( @ S = S & @ S1 = S1 & c * I = d * N & N * d = I * c ) by GROUP_6:2; then A10: S * S1 = (a * N) * (d * N) by A5, A6, GROUP_6:def_3 .= (a * d) * N by GROUP_11:1 ; A11: S1 * S = (d * N) * (a * N) by A5, A6, A9, GROUP_6:def_3 .= (d * a) * N by GROUP_11:1 ; A12: ((a * d) * [.d,a.]) * N = (a * d) * ([.d,a.] * N) by GROUP_2:32 .= (a * d) * N by A8, GROUP_2:113 ; ((a * d) * [.d,a.]) * N = ((a * d) * (((d ") * (a ")) * (d * a))) * N by GROUP_1:def_3 .= (((a * d) * ((d ") * (a "))) * (d * a)) * N by GROUP_1:def_3 .= ((a * (d * ((d ") * (a ")))) * (d * a)) * N by GROUP_1:def_3 .= ((a * ((d * (d ")) * (a "))) * (d * a)) * N by GROUP_1:def_3 .= ((a * ((1_ G) * (a "))) * (d * a)) * N by GROUP_1:def_5 .= ((a * (a ")) * (d * a)) * N by GROUP_1:def_4 .= ((1_ G) * (d * a)) * N by GROUP_1:def_5 .= (d * a) * N by GROUP_1:def_4 ; hence S1 * S = S * S1 by A10, A11, A12; ::_thesis: verum end; hence S1 in center (G ./. N) by GROUP_5:77; ::_thesis: verum end; hence G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) by GROUP_2:58; ::_thesis: verum end; theorem Th21: :: GRNILP_1:21 for G being Group holds ( G is nilpotent iff ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) ) proof let G be Group; ::_thesis: ( G is nilpotent iff ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) ) A1: now__::_thesis:_(_G_is_nilpotent_implies_ex_F_being_FinSequence_of_the_normal_subgroups_of_G_st_ (_len_F_>_0_&_F_._1_=_(Omega)._G_&_F_._(len_F)_=_(1)._G_&_(_for_i_being_Element_of_NAT_st_i_in_dom_F_&_i_+_1_in_dom_F_holds_ for_G1,_G2_being_strict_normal_Subgroup_of_G_st_G1_=_F_._i_&_G2_=_F_._(i_+_1)_holds_ (_G2_is_Subgroup_of_G1_&_[.G1,((Omega)._G).]_is_Subgroup_of_G2_)_)_)_) assume G is nilpotent ; ::_thesis: ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) then consider R being FinSequence of the_normal_subgroups_of G such that A2: ( len R > 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for i being Element of NAT st i in dom R & i + 1 in dom R holds for H1, H2 being strict normal Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) ) ) by Def2; reconsider F = R as FinSequence of the_normal_subgroups_of G ; A3: for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) proof let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) ) assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) let G1, G2 be strict normal Subgroup of G; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) ) assume A5: ( G1 = F . i & G2 = F . (i + 1) ) ; ::_thesis: ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) then A6: ( G2 is strict Subgroup of G1 & ( for N being strict normal Subgroup of G st N = G2 & N is strict Subgroup of G1 holds G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) ) ) by A2, A4; [.G1,((Omega). G).] is strict Subgroup of G2 proof now__::_thesis:_for_N_being_strict_normal_Subgroup_of_G_st_N_=_G2_&_N_is_strict_Subgroup_of_G1_holds_ [.G1,((Omega)._G).]_is_strict_Subgroup_of_G2 let N be strict normal Subgroup of G; ::_thesis: ( N = G2 & N is strict Subgroup of G1 implies [.G1,((Omega). G).] is strict Subgroup of G2 ) assume A7: ( N = G2 & N is strict Subgroup of G1 ) ; ::_thesis: [.G1,((Omega). G).] is strict Subgroup of G2 then G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) by A2, A4, A5; hence [.G1,((Omega). G).] is strict Subgroup of G2 by A7, Th19; ::_thesis: verum end; hence [.G1,((Omega). G).] is strict Subgroup of G2 by A6; ::_thesis: verum end; hence ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) by A2, A4, A5; ::_thesis: verum end; take F = F; ::_thesis: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) thus ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) by A2, A3; ::_thesis: verum end; now__::_thesis:_(_ex_F_being_FinSequence_of_the_normal_subgroups_of_G_st_ (_len_F_>_0_&_F_._1_=_(Omega)._G_&_F_._(len_F)_=_(1)._G_&_(_for_i_being_Element_of_NAT_st_i_in_dom_F_&_i_+_1_in_dom_F_holds_ for_G1,_G2_being_strict_normal_Subgroup_of_G_st_G1_=_F_._i_&_G2_=_F_._(i_+_1)_holds_ (_G2_is_Subgroup_of_G1_&_[.G1,((Omega)._G).]_is_Subgroup_of_G2_)_)_)_implies_ex_F_being_FinSequence_of_the_normal_subgroups_of_G_st_G_is_nilpotent_) given F being FinSequence of the_normal_subgroups_of G such that A8: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) ; ::_thesis: ex F being FinSequence of the_normal_subgroups_of G st G is nilpotent A9: for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) proof let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) assume A10: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) let G1, G2 be strict normal Subgroup of G; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) assume A11: ( G1 = F . i & G2 = F . (i + 1) ) ; ::_thesis: ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) then A12: G2 is strict Subgroup of G1 by A8, A10; [.G1,((Omega). G).] is strict Subgroup of G2 by A8, A10, A11; hence ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) by A12, Th20; ::_thesis: verum end; take F = F; ::_thesis: G is nilpotent ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) by A8, A9; hence G is nilpotent by Def2; ::_thesis: verum end; hence ( G is nilpotent iff ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) ) by A1; ::_thesis: verum end; theorem Th22: :: GRNILP_1:22 for G being Group for H, G1 being Subgroup of G for G2 being strict normal Subgroup of G for H1 being Subgroup of H for H2 being normal Subgroup of H st G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = G1 /\ H & H2 = G2 /\ H holds H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) proof let G be Group; ::_thesis: for H, G1 being Subgroup of G for G2 being strict normal Subgroup of G for H1 being Subgroup of H for H2 being normal Subgroup of H st G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = G1 /\ H & H2 = G2 /\ H holds H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) let H, G1 be Subgroup of G; ::_thesis: for G2 being strict normal Subgroup of G for H1 being Subgroup of H for H2 being normal Subgroup of H st G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = G1 /\ H & H2 = G2 /\ H holds H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) let G2 be strict normal Subgroup of G; ::_thesis: for H1 being Subgroup of H for H2 being normal Subgroup of H st G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = G1 /\ H & H2 = G2 /\ H holds H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) let H1 be Subgroup of H; ::_thesis: for H2 being normal Subgroup of H st G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = G1 /\ H & H2 = G2 /\ H holds H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) let H2 be normal Subgroup of H; ::_thesis: ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = G1 /\ H & H2 = G2 /\ H implies H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) assume that A1: G2 is Subgroup of G1 and A2: G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) and A3: ( H1 = G1 /\ H & H2 = G2 /\ H ) ; ::_thesis: H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) A4: [.G1,((Omega). G).] is Subgroup of G2 by A1, A2, Th19; A5: H2 is strict Subgroup of H1 by A1, A3, GROUP_2:92; then A6: (H1,H2) `*` = H2 by GROUP_6:def_1; then reconsider I = H2 as normal Subgroup of H1 ; reconsider J = H1 ./. ((H1,H2) `*`) as Subgroup of H ./. H2 by A5, GROUP_6:28; for T being Element of (H ./. H2) st T in J holds T in center (H ./. H2) proof let T be Element of (H ./. H2); ::_thesis: ( T in J implies T in center (H ./. H2) ) assume A7: T in J ; ::_thesis: T in center (H ./. H2) for S being Element of (H ./. H2) holds S * T = T * S proof let S be Element of (H ./. H2); ::_thesis: S * T = T * S consider h being Element of H such that A8: ( S = h * H2 & S = H2 * h ) by GROUP_6:21; consider h1 being Element of H1 such that A9: ( T = h1 * I & T = I * h1 ) by A6, A7, GROUP_6:23; reconsider h2 = h1 as Element of H by GROUP_2:42; A10: ( @ S = S & @ T = T & h1 * I = h2 * H2 ) by GROUP_6:2; then A11: S * T = (h * H2) * (h2 * H2) by A8, A9, GROUP_6:def_3 .= (h * h2) * H2 by GROUP_11:1 ; A12: T * S = (h2 * H2) * (h * H2) by A8, A9, A10, GROUP_6:def_3 .= (h2 * h) * H2 by GROUP_11:1 ; A13: [.h2,h.] in H by STRUCT_0:def_5; reconsider a = h as Element of G by GROUP_2:42; A14: a in (Omega). G by STRUCT_0:def_5; H1 is Subgroup of G1 by A3, GROUP_2:88; then reconsider b = h1 as Element of G1 by GROUP_2:42; reconsider c = b as Element of G by GROUP_2:42; b in G1 by STRUCT_0:def_5; then [.c,a.] in [.G1,((Omega). G).] by A14, GROUP_5:65; then A15: [.c,a.] in G2 by A4, GROUP_2:40; A16: a " = h " by GROUP_2:48; c " = h2 " by GROUP_2:48; then A17: (h2 ") * (h ") = (c ") * (a ") by A16, GROUP_2:43; h2 * h = c * a by GROUP_2:43; then A18: ((h2 ") * (h ")) * (h2 * h) = ((c ") * (a ")) * (c * a) by A17, GROUP_2:43; A19: [.h2,h.] = ((h2 ") * (h ")) * (h2 * h) by GROUP_5:16; [.c,a.] = ((c ") * (a ")) * (c * a) by GROUP_5:16; then [.h2,h.] in H2 by A3, A13, A15, A18, A19, GROUP_2:82; then (h * h2) * H2 = (h * h2) * ([.h2,h.] * H2) by GROUP_2:113 .= (h * h2) * ((((h2 ") * (h ")) * (h2 * h)) * H2) by GROUP_5:16 .= ((h * h2) * (((h2 ") * (h ")) * (h2 * h))) * H2 by GROUP_2:32 .= (((h * h2) * ((h2 ") * (h "))) * (h2 * h)) * H2 by GROUP_1:def_3 .= ((h * (h2 * ((h2 ") * (h ")))) * (h2 * h)) * H2 by GROUP_1:def_3 .= ((h * ((h2 * (h2 ")) * (h "))) * (h2 * h)) * H2 by GROUP_1:def_3 .= ((h * ((1_ H) * (h "))) * (h2 * h)) * H2 by GROUP_1:def_5 .= ((h * (h ")) * (h2 * h)) * H2 by GROUP_1:def_4 .= ((1_ H) * (h2 * h)) * H2 by GROUP_1:def_5 .= (h2 * h) * H2 by GROUP_1:def_4 ; hence S * T = T * S by A11, A12; ::_thesis: verum end; hence T in center (H ./. H2) by GROUP_5:77; ::_thesis: verum end; hence H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) by GROUP_2:58; ::_thesis: verum end; Lm4: for G being Group for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H proof let G be Group; ::_thesis: for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H let H be Subgroup of G; ::_thesis: ((Omega). G) /\ H = (Omega). H reconsider G9 = (Omega). G as strict Group ; ( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def_5; then reconsider H9 = (Omega). H as strict Subgroup of G9 by GROUP_2:def_5; ( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def_5; then A1: H is Subgroup of (Omega). G by GROUP_2:def_5; multMagma(# the carrier of (((Omega). G) /\ H), the multF of (((Omega). G) /\ H) #) = multMagma(# the carrier of (H /\ ((Omega). G)), the multF of (H /\ ((Omega). G)) #) .= multMagma(# the carrier of (H /\ ((Omega). G)), the multF of (H /\ ((Omega). G)) #) .= multMagma(# the carrier of H, the multF of H #) by A1, GROUP_2:89 .= multMagma(# the carrier of (H9 /\ ((Omega). G9)), the multF of (H9 /\ ((Omega). G9)) #) by GROUP_2:89 .= multMagma(# the carrier of (H9 /\ ((Omega). G9)), the multF of (H9 /\ ((Omega). G9)) #) .= multMagma(# the carrier of (((Omega). G9) /\ H9), the multF of (((Omega). G9) /\ H9) #) ; hence ((Omega). G) /\ H = (Omega). H by GROUP_2:86; ::_thesis: verum end; Lm5: for G being Group for F1 being strict Subgroup of G for H, F2 being Subgroup of G st F1 is normal Subgroup of F2 holds F1 /\ H is normal Subgroup of F2 /\ H proof let G be Group; ::_thesis: for F1 being strict Subgroup of G for H, F2 being Subgroup of G st F1 is normal Subgroup of F2 holds F1 /\ H is normal Subgroup of F2 /\ H let F1 be strict Subgroup of G; ::_thesis: for H, F2 being Subgroup of G st F1 is normal Subgroup of F2 holds F1 /\ H is normal Subgroup of F2 /\ H let H, F2 be Subgroup of G; ::_thesis: ( F1 is normal Subgroup of F2 implies F1 /\ H is normal Subgroup of F2 /\ H ) reconsider F = F2 /\ H as Subgroup of F2 by GROUP_2:88; assume A1: F1 is normal Subgroup of F2 ; ::_thesis: F1 /\ H is normal Subgroup of F2 /\ H then A2: F1 /\ H = (F1 /\ F2) /\ H by GROUP_2:89 .= F1 /\ (F2 /\ H) by GROUP_2:84 ; reconsider F1 = F1 as normal Subgroup of F2 by A1; F1 /\ F is normal Subgroup of F ; hence F1 /\ H is normal Subgroup of F2 /\ H by A2, GROUP_6:3; ::_thesis: verum end; registration let G be nilpotent Group; cluster -> nilpotent for Subgroup of G; coherence for b1 being Subgroup of G holds b1 is nilpotent proof let H be Subgroup of G; ::_thesis: H is nilpotent consider F being FinSequence of the_normal_subgroups_of G such that A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G ) and A2: for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) by Def2; defpred S1[ set , set ] means ex I being strict normal Subgroup of G st ( I = F . G & c2 = I /\ H ); A3: for k being Nat st k in Seg (len F) holds ex x being Element of the_normal_subgroups_of H st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of the_normal_subgroups_of H st S1[k,x] ) assume k in Seg (len F) ; ::_thesis: ex x being Element of the_normal_subgroups_of H st S1[k,x] then k in dom F by FINSEQ_1:def_3; then F . k in the_normal_subgroups_of G by FINSEQ_2:11; then reconsider I = F . k as strict normal Subgroup of G by Def1; reconsider x = I /\ H as strict Subgroup of H ; reconsider y = x as Element of the_normal_subgroups_of H by Def1; take y ; ::_thesis: S1[k,y] take I ; ::_thesis: ( I = F . k & y = I /\ H ) thus ( I = F . k & y = I /\ H ) ; ::_thesis: verum end; consider R being FinSequence of the_normal_subgroups_of H such that A4: ( dom R = Seg (len F) & ( for i being Nat st i in Seg (len F) holds S1[i,R . i] ) ) from FINSEQ_1:sch_5(A3); A5: len R = len F by A4, FINSEQ_1:def_3; A6: len R > 0 by A1, A4, FINSEQ_1:def_3; A7: R . 1 = (Omega). H proof 1 <= len R by A6, NAT_1:14; then 1 in Seg (len F) by A5; then ex I being strict normal Subgroup of G st ( I = F . 1 & R . 1 = I /\ H ) by A4; hence R . 1 = (Omega). H by A1, Lm4; ::_thesis: verum end; A8: R . (len R) = (1). H proof ex I being strict normal Subgroup of G st ( I = F . (len R) & R . (len R) = I /\ H ) by A1, A4, A5, FINSEQ_1:3; hence R . (len R) = (1). G by A1, A5, GROUP_2:85 .= (1). H by GROUP_2:63 ; ::_thesis: verum end; A9: for i being Element of NAT st i in dom R & i + 1 in dom R holds for H1, H2 being strict normal Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) proof let i be Element of NAT ; ::_thesis: ( i in dom R & i + 1 in dom R implies for H1, H2 being strict normal Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) ) assume A10: ( i in dom R & i + 1 in dom R ) ; ::_thesis: for H1, H2 being strict normal Subgroup of H st H1 = R . i & H2 = R . (i + 1) holds ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) let H1, H2 be strict normal Subgroup of H; ::_thesis: ( H1 = R . i & H2 = R . (i + 1) implies ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) ) assume A11: ( H1 = R . i & H2 = R . (i + 1) ) ; ::_thesis: ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) consider I being strict normal Subgroup of G such that A12: ( I = F . i & R . i = I /\ H ) by A4, A10; consider J being strict normal Subgroup of G such that A13: ( J = F . (i + 1) & R . (i + 1) = J /\ H ) by A4, A10; A14: ( i in dom F & i + 1 in dom F ) by A4, A10, FINSEQ_1:def_3; then A15: J is strict normal Subgroup of I by A12, A13, A2, GROUP_6:8; I ./. ((I,J) `*`) is Subgroup of center (G ./. J) by A14, A12, A13, A2; hence ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (H ./. H2) ) by A13, A15, A12, A11, Th22, Lm5; ::_thesis: verum end; take R ; :: according to GRNILP_1:def_2 ::_thesis: ( len R > 0 & R . 1 = (Omega). H & R . (len R) = (1). H & ( for i being Element of NAT st i in dom R & i + 1 in dom R holds for G1, G2 being strict normal Subgroup of H st G1 = R . i & G2 = R . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) ) thus ( len R > 0 & R . 1 = (Omega). H & R . (len R) = (1). H & ( for i being Element of NAT st i in dom R & i + 1 in dom R holds for G1, G2 being strict normal Subgroup of H st G1 = R . i & G2 = R . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (H ./. G2) ) ) ) by A1, A4, A7, A8, A9, FINSEQ_1:def_3; ::_thesis: verum end; end; registration cluster non empty Group-like associative commutative -> nilpotent for multMagma ; correctness coherence for b1 being Group st b1 is commutative holds b1 is nilpotent ; proof let G be Group; ::_thesis: ( G is commutative implies G is nilpotent ) assume A1: G is commutative ; ::_thesis: G is nilpotent ( (Omega). G in the_normal_subgroups_of G & (1). G in the_normal_subgroups_of G ) by Def1; then <*((Omega). G),((1). G)*> is FinSequence of the_normal_subgroups_of G by FINSEQ_2:13; then consider F being FinSequence of the_normal_subgroups_of G such that A2: F = <*((Omega). G),((1). G)*> ; A3: ( len F = 2 & F . 1 = (Omega). G & F . 2 = (1). G ) by A2, FINSEQ_1:44; for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) proof let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) now__::_thesis:_for_G1,_G2_being_Subgroup_of_G_st_G1_=_F_._i_&_G2_=_F_._(i_+_1)_holds_ for_G1,_G2_being_strict_normal_Subgroup_of_G_st_G1_=_F_._i_&_G2_=_F_._(i_+_1)_holds_ (_G2_is_Subgroup_of_G1_&_[.G1,((Omega)._G).]_is_Subgroup_of_G2_) let G1, G2 be Subgroup of G; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ) assume A5: ( G1 = F . i & G2 = F . (i + 1) ) ; ::_thesis: for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) A6: dom F = {1,2} by A3, FINSEQ_1:2, FINSEQ_1:def_3; A7: ( i in {1,2} & i + 1 in {1,2} ) by A3, A4, FINSEQ_1:2, FINSEQ_1:def_3; A8: ( i = 1 or i = 2 ) by A4, A6, TARSKI:def_2; commutators (G1,((Omega). G)) = {(1_ G)} by A1, GROUP_5:57; then A9: [.G1,((Omega). G).] = gr ({(1_ G)} \ {(1_ G)}) by GROUP_4:35 .= gr ({} the carrier of G) by XBOOLE_1:37 .= (1). G by GROUP_4:30 ; ( G1 = (Omega). G & G2 = (1). G ) by A2, A5, A7, A8, FINSEQ_1:44, TARSKI:def_2; hence for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) by A5, A9, GROUP_2:65; ::_thesis: verum end; hence for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & [.G1,((Omega). G).] is Subgroup of G2 ) ; ::_thesis: verum end; hence G is nilpotent by A3, Th21; ::_thesis: verum end; cluster non empty Group-like associative cyclic -> nilpotent for multMagma ; coherence for b1 being Group st b1 is cyclic holds b1 is nilpotent ; end; theorem Th23: :: GRNILP_1:23 for G, H being strict Group for h being Homomorphism of G,H for A being strict Subgroup of G for a, b being Element of G holds ( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) ) proof let G, H be strict Group; ::_thesis: for h being Homomorphism of G,H for A being strict Subgroup of G for a, b being Element of G holds ( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) ) let h be Homomorphism of G,H; ::_thesis: for A being strict Subgroup of G for a, b being Element of G holds ( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) ) let A be strict Subgroup of G; ::_thesis: for a, b being Element of G holds ( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) ) let a, b be Element of G; ::_thesis: ( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) ) thus ((h . a) * (h . b)) * (h .: A) = (h . (a * b)) * (h .: A) by GROUP_6:def_6 .= h .: ((a * b) * A) by GRSOLV_1:13 ; ::_thesis: ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) thus ((h .: A) * (h . a)) * (h . b) = (h .: A) * ((h . a) * (h . b)) by GROUP_2:107 .= (h .: A) * (h . (a * b)) by GROUP_6:def_6 .= h .: (A * (a * b)) by GRSOLV_1:13 .= h .: ((A * a) * b) by GROUP_2:107 ; ::_thesis: verum end; theorem Th24: :: GRNILP_1:24 for G, H being strict Group for h being Homomorphism of G,H for A being strict Subgroup of G for a, b being Element of G for H1 being Subgroup of Image h for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) proof let G, H be strict Group; ::_thesis: for h being Homomorphism of G,H for A being strict Subgroup of G for a, b being Element of G for H1 being Subgroup of Image h for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) let h be Homomorphism of G,H; ::_thesis: for A being strict Subgroup of G for a, b being Element of G for H1 being Subgroup of Image h for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) let A be strict Subgroup of G; ::_thesis: for a, b being Element of G for H1 being Subgroup of Image h for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) let a, b be Element of G; ::_thesis: for H1 being Subgroup of Image h for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) let H1 be Subgroup of Image h; ::_thesis: for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) let a1, b1 be Element of (Image h); ::_thesis: ( a1 = h . a & b1 = h . b & H1 = h .: A implies (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) ) assume that A1: a1 = h . a and A2: b1 = h . b and A3: H1 = h .: A ; ::_thesis: (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) A4: a1 * b1 = (h . a) * (h . b) by A1, A2, GROUP_2:43; set c1 = a1 * b1; set c = a * b; A5: h . (a * b) = (h . a) * (h . b) by GROUP_6:def_6; A6: h .: ((a * b) * A) = (h . (a * b)) * (h .: A) by GRSOLV_1:13; (a1 * b1) * H1 = (h . (a * b)) * (h .: A) proof now__::_thesis:_for_x_being_set_st_x_in_(a1_*_b1)_*_H1_holds_ x_in_(h_._(a_*_b))_*_(h_.:_A) let x be set ; ::_thesis: ( x in (a1 * b1) * H1 implies x in (h . (a * b)) * (h .: A) ) assume x in (a1 * b1) * H1 ; ::_thesis: x in (h . (a * b)) * (h .: A) then consider Z being Element of (Image h) such that A7: x = (a1 * b1) * Z and A8: Z in H1 by GROUP_2:103; consider Z1 being Element of A such that A9: Z = (h | A) . Z1 by A3, A8, GROUP_6:45; A10: Z1 in A by STRUCT_0:def_5; reconsider Z1 = Z1 as Element of G by GROUP_2:42; Z = h . Z1 by A9, FUNCT_1:49; then A11: x = (h . (a * b)) * (h . Z1) by A4, A5, A7, GROUP_2:43 .= h . ((a * b) * Z1) by GROUP_6:def_6 ; (a * b) * Z1 in (a * b) * A by A10, GROUP_2:103; hence x in (h . (a * b)) * (h .: A) by A11, A6, FUNCT_2:35; ::_thesis: verum end; then A12: (a1 * b1) * H1 c= (h . (a * b)) * (h .: A) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_(h_._(a_*_b))_*_(h_.:_A)_holds_ x_in_(a1_*_b1)_*_H1 let x be set ; ::_thesis: ( x in (h . (a * b)) * (h .: A) implies x in (a1 * b1) * H1 ) assume x in (h . (a * b)) * (h .: A) ; ::_thesis: x in (a1 * b1) * H1 then consider y being set such that A13: y in the carrier of G and A14: y in (a * b) * A and A15: x = h . y by A6, FUNCT_2:64; reconsider y = y as Element of G by A13; consider Z being Element of G such that A16: y = (a * b) * Z and A17: Z in A by A14, GROUP_2:103; Z in the carrier of A by A17, STRUCT_0:def_5; then h . Z in h .: the carrier of A by FUNCT_2:35; then h . Z in the carrier of (h .: A) by GRSOLV_1:8; then A18: h . Z in H1 by A3, STRUCT_0:def_5; then h . Z in Image h by GROUP_2:40; then reconsider Z1 = h . Z as Element of (Image h) by STRUCT_0:def_5; x = (h . (a * b)) * (h . Z) by A15, A16, GROUP_6:def_6; then x = (a1 * b1) * Z1 by A4, A5, GROUP_2:43; hence x in (a1 * b1) * H1 by A18, GROUP_2:103; ::_thesis: verum end; then (h . (a * b)) * (h .: A) c= (a1 * b1) * H1 by TARSKI:def_3; hence (a1 * b1) * H1 = (h . (a * b)) * (h .: A) by A12, XBOOLE_0:def_10; ::_thesis: verum end; hence (a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A) by GROUP_6:def_6; ::_thesis: verum end; theorem Th25: :: GRNILP_1:25 for G, H being strict Group for h being Homomorphism of G,H for G1 being strict Subgroup of G for G2 being strict normal Subgroup of G for H1 being strict Subgroup of Image h for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) proof let G, H be strict Group; ::_thesis: for h being Homomorphism of G,H for G1 being strict Subgroup of G for G2 being strict normal Subgroup of G for H1 being strict Subgroup of Image h for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) let h be Homomorphism of G,H; ::_thesis: for G1 being strict Subgroup of G for G2 being strict normal Subgroup of G for H1 being strict Subgroup of Image h for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) let G1 be strict Subgroup of G; ::_thesis: for G2 being strict normal Subgroup of G for H1 being strict Subgroup of Image h for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) let G2 be strict normal Subgroup of G; ::_thesis: for H1 being strict Subgroup of Image h for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) let H1 be strict Subgroup of Image h; ::_thesis: for H2 being strict normal Subgroup of Image h st G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 holds H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) let H2 be strict normal Subgroup of Image h; ::_thesis: ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) & H1 = h .: G1 & H2 = h .: G2 implies H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) assume that A1: G2 is strict Subgroup of G1 and A2: G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) and A3: ( H1 = h .: G1 & H2 = h .: G2 ) ; ::_thesis: H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) A4: H2 is strict Subgroup of H1 by A1, A3, GRSOLV_1:12; then A5: (H1,H2) `*` = H2 by GROUP_6:def_1; then reconsider I = H2 as normal Subgroup of H1 ; reconsider J = H1 ./. ((H1,H2) `*`) as Subgroup of (Image h) ./. H2 by A4, GROUP_6:28; for T being Element of ((Image h) ./. H2) st T in J holds T in center ((Image h) ./. H2) proof let T be Element of ((Image h) ./. H2); ::_thesis: ( T in J implies T in center ((Image h) ./. H2) ) assume A6: T in J ; ::_thesis: T in center ((Image h) ./. H2) for S being Element of ((Image h) ./. H2) holds S * T = T * S proof let S be Element of ((Image h) ./. H2); ::_thesis: S * T = T * S consider g being Element of (Image h) such that A7: ( S = g * H2 & S = H2 * g ) by GROUP_6:21; consider h1 being Element of H1 such that A8: ( T = h1 * I & T = I * h1 ) by A5, A6, GROUP_6:23; reconsider h2 = h1 as Element of (Image h) by GROUP_2:42; A9: ( @ S = S & @ T = T & h1 * I = h2 * H2 ) by GROUP_6:2; then A10: S * T = (g * H2) * (h2 * H2) by A7, A8, GROUP_6:def_3 .= (g * h2) * H2 by GROUP_11:1 ; A11: T * S = (h2 * H2) * (g * H2) by A7, A8, A9, GROUP_6:def_3 .= (h2 * g) * H2 by GROUP_11:1 ; g in Image h by STRUCT_0:def_5; then consider a being Element of G such that A12: g = h . a by GROUP_6:45; A13: a in (Omega). G by STRUCT_0:def_5; h1 in H1 by STRUCT_0:def_5; then consider a1 being Element of G1 such that A14: h1 = (h | G1) . a1 by A3, GROUP_6:45; A15: a1 in G1 by STRUCT_0:def_5; reconsider a2 = a1 as Element of G by GROUP_2:42; A16: h2 = h . a2 by A14, FUNCT_1:49; then A17: (g * h2) * H2 = ((h . a) * (h . a2)) * (h .: G2) by A12, A3, Th24 .= h .: ((a * a2) * G2) by Th23 ; A18: (h2 * g) * H2 = ((h . a2) * (h . a)) * (h .: G2) by A12, A16, A3, Th24 .= h .: ((a2 * a) * G2) by Th23 ; A19: [.G1,((Omega). G).] is strict Subgroup of G2 by A1, A2, Th19; [.a2,a.] in [.G1,((Omega). G).] by A13, A15, GROUP_5:65; then [.a2,a.] in G2 by A19, GROUP_2:40; then (a * a2) * G2 = (a * a2) * ([.a2,a.] * G2) by GROUP_2:113 .= (a * a2) * ((((a2 ") * (a ")) * (a2 * a)) * G2) by GROUP_5:16 .= ((a * a2) * (((a2 ") * (a ")) * (a2 * a))) * G2 by GROUP_2:32 .= (((a * a2) * ((a2 ") * (a "))) * (a2 * a)) * G2 by GROUP_1:def_3 .= ((a * (a2 * ((a2 ") * (a ")))) * (a2 * a)) * G2 by GROUP_1:def_3 .= ((a * ((a2 * (a2 ")) * (a "))) * (a2 * a)) * G2 by GROUP_1:def_3 .= ((a * ((1_ G) * (a "))) * (a2 * a)) * G2 by GROUP_1:def_5 .= ((a * (a ")) * (a2 * a)) * G2 by GROUP_1:def_4 .= ((1_ G) * (a2 * a)) * G2 by GROUP_1:def_5 .= (a2 * a) * G2 by GROUP_1:def_4 ; hence S * T = T * S by A10, A11, A17, A18; ::_thesis: verum end; hence T in center ((Image h) ./. H2) by GROUP_5:77; ::_thesis: verum end; hence H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) by GROUP_2:58; ::_thesis: verum end; theorem Th26: :: GRNILP_1:26 for G, H being strict Group for h being Homomorphism of G,H for A being strict normal Subgroup of G holds h .: A is strict normal Subgroup of Image h proof let G, H be strict Group; ::_thesis: for h being Homomorphism of G,H for A being strict normal Subgroup of G holds h .: A is strict normal Subgroup of Image h let h be Homomorphism of G,H; ::_thesis: for A being strict normal Subgroup of G holds h .: A is strict normal Subgroup of Image h let A be strict normal Subgroup of G; ::_thesis: h .: A is strict normal Subgroup of Image h reconsider C = h .: A as strict Subgroup of Image h by GRSOLV_1:9; for b being Element of (Image h) holds b * C c= C * b proof let b be Element of (Image h); ::_thesis: b * C c= C * b A1: b in Image h by STRUCT_0:def_5; now__::_thesis:_for_x_being_set_st_x_in_b_*_C_holds_ x_in_C_*_b consider b1 being Element of G such that A2: b = h . b1 by A1, GROUP_6:45; let x be set ; ::_thesis: ( x in b * C implies x in C * b ) assume x in b * C ; ::_thesis: x in C * b then consider g being Element of (Image h) such that A3: x = b * g and A4: g in C by GROUP_2:103; consider g1 being Element of A such that A5: g = (h | A) . g1 by A4, GROUP_6:45; reconsider g1 = g1 as Element of G by GROUP_2:42; g = h . g1 by A5, FUNCT_1:49; then A6: x = (h . b1) * (h . g1) by A2, A3, GROUP_2:43 .= h . (b1 * g1) by GROUP_6:def_6 ; g1 in A by STRUCT_0:def_5; then A7: b1 * g1 in b1 * A by GROUP_2:103; A8: h .: (A * b1) = (h .: A) * (h . b1) by GRSOLV_1:13; b1 * A = A * b1 by GROUP_3:117; then x in (h .: A) * (h . b1) by A6, A7, A8, FUNCT_2:35; hence x in C * b by A2, GROUP_6:2; ::_thesis: verum end; hence b * C c= C * b by TARSKI:def_3; ::_thesis: verum end; hence h .: A is strict normal Subgroup of Image h by GROUP_3:118; ::_thesis: verum end; registration let G be strict nilpotent Group; let H be strict Group; let h be Homomorphism of G,H; cluster Image h -> nilpotent ; coherence Image h is nilpotent proof consider F being FinSequence of the_normal_subgroups_of G such that A1: len F > 0 and A2: F . 1 = (Omega). G and A3: F . (len F) = (1). G and A4: for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) by Def2; 1 <= len F by A1, NAT_1:14; then A5: 1 in Seg (len F) ; defpred S1[ set , set ] means ex J being strict normal Subgroup of G st ( J = F . G & H = h .: J ); A6: for k being Nat st k in Seg (len F) holds ex x being Element of the_normal_subgroups_of (Image h) st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of the_normal_subgroups_of (Image h) st S1[k,x] ) assume k in Seg (len F) ; ::_thesis: ex x being Element of the_normal_subgroups_of (Image h) st S1[k,x] then k in dom F by FINSEQ_1:def_3; then F . k in the_normal_subgroups_of G by FINSEQ_2:11; then F . k is strict normal Subgroup of G by Def1; then consider A being strict normal Subgroup of G such that A7: A = F . k ; h .: A is strict normal Subgroup of Image h by Th26; then h .: A in the_normal_subgroups_of (Image h) by Def1; hence ex x being Element of the_normal_subgroups_of (Image h) st S1[k,x] by A7; ::_thesis: verum end; consider Z being FinSequence of the_normal_subgroups_of (Image h) such that A8: ( dom Z = Seg (len F) & ( for j being Nat st j in Seg (len F) holds S1[j,Z . j] ) ) from FINSEQ_1:sch_5(A6); Seg (len Z) = Seg (len F) by A8, FINSEQ_1:def_3; then A9: dom F = Seg (len Z) by FINSEQ_1:def_3 .= dom Z by FINSEQ_1:def_3 ; A10: for i being Element of NAT st i in dom Z & i + 1 in dom Z holds for H1, H2 being strict normal Subgroup of Image h st H1 = Z . i & H2 = Z . (i + 1) holds ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) proof let i be Element of NAT ; ::_thesis: ( i in dom Z & i + 1 in dom Z implies for H1, H2 being strict normal Subgroup of Image h st H1 = Z . i & H2 = Z . (i + 1) holds ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) ) assume A11: ( i in dom Z & i + 1 in dom Z ) ; ::_thesis: for H1, H2 being strict normal Subgroup of Image h st H1 = Z . i & H2 = Z . (i + 1) holds ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) let H1, H2 be strict normal Subgroup of Image h; ::_thesis: ( H1 = Z . i & H2 = Z . (i + 1) implies ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) ) assume that A12: H1 = Z . i and A13: H2 = Z . (i + 1) ; ::_thesis: ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) A14: ( i in dom F & i + 1 in dom F ) by A8, A11, FINSEQ_1:def_3; consider G1 being strict normal Subgroup of G such that A15: G1 = F . i and A16: H1 = h .: G1 by A8, A11, A12; consider G2 being strict normal Subgroup of G such that A17: G2 = F . (i + 1) and A18: H2 = h .: G2 by A8, A11, A13; A19: G2 is strict Subgroup of G1 by A4, A9, A11, A15, A17; G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) by A14, A15, A17, A4; hence ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center ((Image h) ./. H2) ) by A16, A19, A18, Th25, GRSOLV_1:12; ::_thesis: verum end; take Z ; :: according to GRNILP_1:def_2 ::_thesis: ( len Z > 0 & Z . 1 = (Omega). (Image h) & Z . (len Z) = (1). (Image h) & ( for i being Element of NAT st i in dom Z & i + 1 in dom Z holds for G1, G2 being strict normal Subgroup of Image h st G1 = Z . i & G2 = Z . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center ((Image h) ./. G2) ) ) ) A20: len Z = len F by A8, FINSEQ_1:def_3; ( Z . 1 = (Omega). (Image h) & Z . (len Z) = (1). (Image h) ) proof ex G1 being strict normal Subgroup of G st ( G1 = F . 1 & Z . 1 = h .: G1 ) by A8, A5; hence Z . 1 = (Omega). (Image h) by A2, GRSOLV_1:11; ::_thesis: Z . (len Z) = (1). (Image h) ex G2 being strict normal Subgroup of G st ( G2 = F . (len F) & Z . (len F) = h .: G2 ) by A1, A8, FINSEQ_1:3; hence Z . (len Z) = (1). H by A3, A20, GRSOLV_1:11 .= (1). (Image h) by GROUP_2:63 ; ::_thesis: verum end; hence ( len Z > 0 & Z . 1 = (Omega). (Image h) & Z . (len Z) = (1). (Image h) & ( for i being Element of NAT st i in dom Z & i + 1 in dom Z holds for G1, G2 being strict normal Subgroup of Image h st G1 = Z . i & G2 = Z . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center ((Image h) ./. G2) ) ) ) by A1, A8, A10, FINSEQ_1:def_3; ::_thesis: verum end; end; registration let G be strict nilpotent Group; let N be strict normal Subgroup of G; clusterG ./. N -> nilpotent ; coherence G ./. N is nilpotent proof Image (nat_hom N) = G ./. N by GROUP_6:48; hence G ./. N is nilpotent ; ::_thesis: verum end; end; theorem :: GRNILP_1:27 for G being Group st ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1 being strict normal Subgroup of G st G1 = F . i holds [.G1,((Omega). G).] = F . (i + 1) ) ) holds G is nilpotent proof let G be Group; ::_thesis: ( ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1 being strict normal Subgroup of G st G1 = F . i holds [.G1,((Omega). G).] = F . (i + 1) ) ) implies G is nilpotent ) given F being FinSequence of the_normal_subgroups_of G such that A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G ) and A2: for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1 being strict normal Subgroup of G st G1 = F . i holds [.G1,((Omega). G).] = F . (i + 1) ; ::_thesis: G is nilpotent for i being Element of NAT st i in dom F & i + 1 in dom F holds for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) proof let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) ) assume A3: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) let H1, H2 be strict normal Subgroup of G; ::_thesis: ( H1 = F . i & H2 = F . (i + 1) implies ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) ) assume ( H1 = F . i & H2 = F . (i + 1) ) ; ::_thesis: ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) then H2 = [.H1,((Omega). G).] by A2, A3; hence ( H2 is Subgroup of H1 & [.H1,((Omega). G).] is Subgroup of H2 ) by Th15, GROUP_2:54; ::_thesis: verum end; hence G is nilpotent by A1, Th21; ::_thesis: verum end; theorem :: GRNILP_1:28 for G being Group st ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G ./. G2 is commutative Group ) ) ) holds G is nilpotent proof let G be Group; ::_thesis: ( ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G ./. G2 is commutative Group ) ) ) implies G is nilpotent ) given F being FinSequence of the_normal_subgroups_of G such that A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G ) and A2: for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G ./. G2 is commutative Group ) ; ::_thesis: G is nilpotent A3: for i being Element of NAT st i in dom F & i + 1 in dom F holds for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) proof let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) ) assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) let H1, H2 be strict normal Subgroup of G; ::_thesis: ( H1 = F . i & H2 = F . (i + 1) implies ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) ) assume A5: ( H1 = F . i & H2 = F . (i + 1) ) ; ::_thesis: ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) then H2 is Subgroup of H1 by A2, A4; then A6: H1 ./. ((H1,H2) `*`) is Subgroup of G ./. H2 by GROUP_6:28; G ./. H2 is commutative Group by A2, A4, A5; hence ( H2 is Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) by A2, A4, A5, A6, GROUP_5:82; ::_thesis: verum end; take F ; :: according to GRNILP_1:def_2 ::_thesis: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) thus ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) by A1, A3; ::_thesis: verum end; theorem :: GRNILP_1:29 for G being Group st ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G ./. G2 is cyclic Group ) ) ) holds G is nilpotent proof let G be Group; ::_thesis: ( ex F being FinSequence of the_normal_subgroups_of G st ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G ./. G2 is cyclic Group ) ) ) implies G is nilpotent ) given F being FinSequence of the_normal_subgroups_of G such that A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G ) and A2: for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G ./. G2 is cyclic Group ) ; ::_thesis: G is nilpotent A3: for i being Element of NAT st i in dom F & i + 1 in dom F holds for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) proof let i be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) ) assume A4: ( i in dom F & i + 1 in dom F ) ; ::_thesis: for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) let H1, H2 be strict normal Subgroup of G; ::_thesis: ( H1 = F . i & H2 = F . (i + 1) implies ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) ) assume A5: ( H1 = F . i & H2 = F . (i + 1) ) ; ::_thesis: ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) then H2 is strict Subgroup of H1 by A2, A4; then A6: H1 ./. ((H1,H2) `*`) is Subgroup of G ./. H2 by GROUP_6:28; G ./. H2 is commutative Group by A2, A4, A5; hence ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) by A2, A4, A5, A6, GROUP_5:82; ::_thesis: verum end; take F ; :: according to GRNILP_1:def_2 ::_thesis: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) thus ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) by A1, A3; ::_thesis: verum end; registration cluster non empty Group-like associative nilpotent -> solvable for multMagma ; correctness coherence for b1 being Group st b1 is nilpotent holds b1 is solvable ; proof let G be Group; ::_thesis: ( G is nilpotent implies G is solvable ) assume G is nilpotent ; ::_thesis: G is solvable then consider F being FinSequence of the_normal_subgroups_of G such that A1: ( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G & ( for i being Element of NAT st i in dom F & i + 1 in dom F holds for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds ( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) ) by Def2; reconsider R = F as FinSequence of Subgroups G by Th18; A2: for i being Element of NAT st i in dom R & i + 1 in dom R holds for H1, H2 being Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds H1 ./. N is commutative ) ) proof let i be Element of NAT ; ::_thesis: ( i in dom R & i + 1 in dom R implies for H1, H2 being Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds H1 ./. N is commutative ) ) ) assume A3: ( i in dom R & i + 1 in dom R ) ; ::_thesis: for H1, H2 being Subgroup of G st H1 = R . i & H2 = R . (i + 1) holds ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds H1 ./. N is commutative ) ) then A4: ( F . i is strict normal Subgroup of G & F . (i + 1) is strict normal Subgroup of G ) by Th16; let H1, H2 be Subgroup of G; ::_thesis: ( H1 = R . i & H2 = R . (i + 1) implies ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds H1 ./. N is commutative ) ) ) assume A5: ( H1 = R . i & H2 = R . (i + 1) ) ; ::_thesis: ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds H1 ./. N is commutative ) ) for N being normal Subgroup of H1 st N = H2 holds H1 ./. N is commutative proof let N be normal Subgroup of H1; ::_thesis: ( N = H2 implies H1 ./. N is commutative ) assume A6: N = H2 ; ::_thesis: H1 ./. N is commutative then reconsider N9 = N as strict normal Subgroup of G by A5, A4; A7: H1 ./. ((H1,N9) `*`) is Subgroup of center (G ./. N9) by A1, A3, A5, A6, A4; center (G ./. N9) is commutative by GROUP_5:80; hence H1 ./. N is commutative by A7, GROUP_6:def_1; ::_thesis: verum end; hence ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds H1 ./. N is commutative ) ) by A1, A3, A5, A4, GROUP_6:8; ::_thesis: verum end; take R ; :: according to GRSOLV_1:def_1 ::_thesis: ( not len R <= 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for b1 being Element of NAT holds ( not b1 in dom R or not K403(b1,1) in dom R or for b2, b3 being Subgroup of G holds ( not b2 = R . b1 or not b3 = R . K403(b1,1) or ( b3 is Subgroup of b2 & ( for b4 being Subgroup of b2 holds ( not b4 = b3 or b2 ./. b4 is commutative ) ) ) ) ) ) ) thus ( not len R <= 0 & R . 1 = (Omega). G & R . (len R) = (1). G & ( for b1 being Element of NAT holds ( not b1 in dom R or not K403(b1,1) in dom R or for b2, b3 being Subgroup of G holds ( not b2 = R . b1 or not b3 = R . K403(b1,1) or ( b3 is Subgroup of b2 & ( for b4 being Subgroup of b2 holds ( not b4 = b3 or b2 ./. b4 is commutative ) ) ) ) ) ) ) by A1, A2; ::_thesis: verum end; end;