:: Nilpotent Groups :: by Dailu Li , Xiquan Liang and Yanhong Men :: :: Received November 10, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies REALSET1, FINSEQ_1, GROUP_3, FUNCT_1, RLSUB_1, GROUP_2, RELAT_1, GROUP_6, XBOOLE_0, QC_LANG1, GROUP_1, GRAPH_1, ARYTM_1, ARYTM_3, ZFMISC_1, NUMBERS, SUBSET_1, XXREAL_1, STRUCT_0, NEWTON, TARSKI, NAT_1, PARTFUN1, PRE_TOPC, XXREAL_0, CARD_1, GROUP_4, NATTRA_1, CARD_3, BINOP_1, GROUP_5, GRSOLV_1, GRNILP_1, BCIALG_2, ALGSTR_0; notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, ALGSTR_0, PARTFUN1, FINSEQ_1, ZFMISC_1, ORDINAL1, XXREAL_0, NUMBERS, REALSET1, DOMAIN_1, GROUP_1, GROUP_3, GR_CY_1, GRSOLV_1, GROUP_4, GROUP_5, GROUP_2, GROUP_6; constructors BINOP_1, BINARITH, GROUP_4, GROUP_5, GRSOLV_1, RELSET_1, GR_CY_1, REALSET1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, INT_1, FINSEQ_1, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, GROUP_6, GR_CY_1, ALGSTR_0, RELSET_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions GROUP_2, GROUP_6, TARSKI, FINSEQ_1, GROUP_4, ALGSTR_0, GROUP_3, GROUP_5, GRSOLV_1, REALSET1; theorems FINSEQ_1, GROUP_2, GROUP_3, TARSKI, GROUP_5, GROUP_6, FINSEQ_2, FUNCT_2, RELAT_1, XBOOLE_0, XBOOLE_1, NAT_1, GROUP_1, PARTFUN1, FINSEQ_3, SUBSET_1, GROUP_4, FUNCT_1, GRSOLV_1, STRUCT_0, GROUP_11, XTUPLE_0; schemes XBOOLE_0, FUNCT_1, FINSEQ_1, FINSEQ_2; begin reserve x,y for set, G for Group, A,B,H,H1,H2 for Subgroup of G, a,b,c for Element of G, F,F1 for FinSequence of the carrier of G, I,I1 for FinSequence of INT, i,j for Element of NAT; theorem a |^ b = a * [.a,b.] proof 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 thesis; end; theorem [.a,b.]" = [.a,b".]|^b proof 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; end; theorem [.a,b.]" = [.a",b.]|^a proof 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; end; theorem Th4: ([.a,b".]|^ b)" = [.b",a.]|^ b proof thus ([.a,b".]|^ b)" = [.a,b".]"|^ b by GROUP_3:26 .= [.b",a.]|^ b by GROUP_5:22; end; theorem Th5: [.a,b",c.] |^ b = [.[.a,b".]|^ b,c|^ b.] proof 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 thesis by A1; end; theorem Th6: [.a,b".]|^ b = [.b,a.] proof 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.]; end; theorem Th7: [.a,b",c.] |^ b = [.b,a,c|^ b.] proof [.a,b",c.] |^ b = [.[.a,b".]|^ b,c|^ b.] by Th5; hence thesis by Th6; end; theorem [.a,b,c|^ a.] * [.c,a,b|^ c.] * [.b,c,a|^ b.] = 1_G proof [.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 thesis by GROUP_5:46; end; theorem Th9: [.A,B.] is Subgroup of [.B,A.] proof now let a; assume a in [.A,B.]; then consider F,I 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 F(Nat) = (F/.$1)"; consider F1 such that A3: len F1 = len F and A4: for k be Nat st k in dom F1 holds F1.k = F(k) from FINSEQ_2:sch 1; A5: dom F1 = Seg len F by A3,FINSEQ_1:def 3; deffunc F(Nat) = @(- @(I/.$1)); consider I1 such that A6: len I1 = len F and A7: for k be Nat st k in dom I1 holds I1.k = F(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 J = 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 let k be Nat; assume A13: k in dom(F |^ I); then A14: k in dom F by A12,FINSEQ_1:def 3; J.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 J.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 = J.k by A14,GROUP_4:def 3; end; then A15: J = F |^ I by A11,FINSEQ_2:9; rng F1 c= commutators(B,A) proof let x; assume x in rng F1; then consider y such that A16: y in dom F1 and A17: F1.y = x by FUNCT_1:def 3; reconsider 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 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 thesis by A19,GROUP_5:52; end; hence a in [.B,A.] by A2,A3,A6,A15,GROUP_5:61; end; hence thesis by GROUP_2:58; end; definition let G,A,B; redefine func [.A,B.]; commutativity proof let A,B; [.A,B.] is Subgroup of [.B,A.] & [.B,A.] is Subgroup of [.A,B.] by Th9; hence thesis by GROUP_2:55; end; end; theorem Th10: B is Subgroup of A implies commutators(A,B) c= carr A proof assume A1: B is Subgroup of A; let x; assume x in commutators(A,B); then consider a,b 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 thesis by A2,A5,STRUCT_0:def 5; end; Lm1: gr carr A is Subgroup of A proof set A9 = multMagma(# the carrier of A, the multF of A #); the carrier of A9 c= the carrier of G & the multF of A9 = (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 thesis by A1,GROUP_2:56; end; theorem Th11: B is Subgroup of A implies [.A,B.] is Subgroup of A proof A1: gr carr A is Subgroup of A by Lm1; assume 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 thesis by A1,GROUP_2:56; end; theorem B is Subgroup of A implies [.B,A.] is Subgroup of A by Th11; Lm2: A is Subgroup of (Omega).G proof 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 thesis by GROUP_2:56; end; theorem [.H1, (Omega).G.] is Subgroup of H2 implies [.H1 /\ H,H.] is Subgroup of H2 /\ H proof assume A1: [.H1, (Omega).G.] is Subgroup of H2; 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 thesis by A2,GROUP_2:91; end; theorem [.H1,H2.] is Subgroup of [.H1,(Omega).G.] proof A1: H2 is Subgroup of (Omega).G by Lm2; H1 is Subgroup of H1 by GROUP_2:54; hence thesis by A1,GROUP_5:66; end; Lm3: for N being normal Subgroup of G holds [.N,H.] is Subgroup of N proof let N be normal Subgroup of G; 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 let a be Element of G; 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; end; then reconsider 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 thesis by A1,GROUP_2:56; end; theorem Th15: A is normal Subgroup of G iff [.A,(Omega).G.] is Subgroup of A proof thus A is normal Subgroup of G implies [.A,(Omega).G.] is Subgroup of A by Lm3; assume A1: [.A,(Omega).G.] is Subgroup of A; for b holds b * A c= A * b proof let b; let x; assume A2: x in b * A; then reconsider x as Element of G; consider Z be 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 thesis by A3,A5,A6,GROUP_2:104; end; hence thesis by GROUP_3:118; end; definition let G; func the_normal_subgroups_of G -> set means :Def1: x in it iff x is strict normal Subgroup of G; existence proof defpred P[set,set] means ex H being strict normal Subgroup of G st $2 = H & $1 = the carrier of H; defpred P[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 & P[x] from XBOOLE_0:sch 1; A2: for x,y1,y2 being set st P[x,y1] & P[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 & P[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; thus x in B implies ex y being set st [x,y] in f proof assume A4: x in B; 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; thus thesis by A3,A4,A5; end; given y be set such that A6: [x,y] in f; thus thesis by A3,A6; 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; thus y in rng f implies y is strict normal Subgroup of G proof assume y in rng f; then consider x be 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 thesis; end; assume y is strict normal Subgroup of G; 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 thesis by A9,FUNCT_1:def 3; end; hence thesis; end; uniqueness proof defpred P[set] means $1 is strict normal Subgroup of G; let A1,A2 be set; assume A10: for x being set holds x in A1 iff P[x]; assume A11: for x being set holds x in A2 iff P[x]; thus thesis from XBOOLE_0:sch 2(A10,A11); end; end; registration let G; cluster the_normal_subgroups_of G -> non empty; coherence proof the strict normal Subgroup of G in the_normal_subgroups_of G by Def1; hence thesis; end; end; theorem Th16: for F being FinSequence of the_normal_subgroups_of G for j st j in dom F holds F.j is strict normal Subgroup of G proof let F be FinSequence of the_normal_subgroups_of G; let j; assume j in dom F; then F.j in rng F by FUNCT_1:3; hence thesis by Def1; end; theorem Th17: the_normal_subgroups_of G c= Subgroups G proof let x; assume x in the_normal_subgroups_of G; then x is strict normal Subgroup of G by Def1; hence thesis by GROUP_3:def 1; end; theorem Th18: for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G proof let F be FinSequence of the_normal_subgroups_of G; the_normal_subgroups_of G c= Subgroups G by Th17; then rng F c= Subgroups G by XBOOLE_1:1; hence thesis by FINSEQ_1:def 4; end; definition let IT be Group; attr IT is nilpotent means :Def2: 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 st i in dom F & i+1 in dom F 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; registration cluster nilpotent strict for Group; existence proof set G = the Group; take H = (1).G; thus H is nilpotent proof rng <*H*> c= the_normal_subgroups_of H proof let x be set; assume A1: x in rng<*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 thesis by Def1; end; then reconsider F = <*H*> as FinSequence of the_normal_subgroups_of H by FINSEQ_1:def 4; take F; 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 st i in dom F & i+1 in dom F 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; assume A4: i in dom F & i+1 in dom F; let G1,G2 be strict normal Subgroup of H; assume G1=F.i & G2=F.(i+1); dom F={1} by A2,FINSEQ_1:2,def 3; then i=1 & i+1=1 by A4,TARSKI:def 1; hence thesis; end; hence thesis by A3,FINSEQ_1:40; end; thus thesis; end; end; theorem Th19: for G1 being Subgroup of G,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 G1 be Subgroup of G; let N be strict normal Subgroup of G; assume that A1: N is Subgroup of G1 and A2: 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; A4: commutators (G1,(Omega).G) c= carr N proof now let x be Element of G; assume x in commutators (G1,(Omega).G); then consider a,b 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; end; hence thesis by SUBSET_1:2; end; gr carr N = N by GROUP_4:31; hence thesis by A4,GROUP_4:32; end; theorem Th20: for G1 being Subgroup of G, 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 G1 be Subgroup of G; let N be normal Subgroup of G; assume that A1: N is strict Subgroup of G1 and A2: [.G1,(Omega).G.] is strict 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; for S1 be Element of G./.N st S1 in J holds S1 in center (G./.N) proof let S1 be Element of G./.N; assume A4: S1 in J; for S be Element of G./.N holds S1 * S = S * S1 proof let S be Element of G./.N; 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 thesis by A10,A11,A12; end; hence thesis by GROUP_5:77; end; hence thesis by GROUP_2:58; end; theorem Th21: 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 st i in dom F & i+1 in dom F 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; A1: now assume G is nilpotent; 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 st i in dom R & i+1 in dom R 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 st i in dom F & i+1 in dom F 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; assume A4: i in dom F & i+1 in dom F; let G1,G2 be strict normal Subgroup of G; assume A5: G1 = F.i & G2 = F.(i+1); 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 let N be strict normal Subgroup of G; assume A7: N = G2 & N is strict Subgroup of G1; 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; end; hence thesis by A6; end; hence thesis by A2,A4,A5; end; take F; thus len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G & for i st i in dom F & i+1 in dom F 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; end; now 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 st i in dom F & i+1 in dom F 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; A9: for i st i in dom F & i+1 in dom F 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; assume A10: i in dom F & i+1 in dom F; let G1,G2 be strict normal Subgroup of G; assume A11: G1 = F.i & G2 = F.(i+1); then A12: G2 is strict Subgroup of G1 by A8,A10; [.G1, (Omega).G.] is strict Subgroup of G2 by A8,A10,A11; hence thesis by A12,Th20; end; take F; len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G & for i st i in dom F & i+1 in dom F 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; end; hence thesis by A1; end; theorem Th22: 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; let H,G1 be Subgroup of G; let G2 be strict normal Subgroup of G; let H1 be Subgroup of H; let H2 be normal Subgroup of H; 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; 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 be Element of H./.H2 st T in J holds T in center (H./.H2) proof let T be Element of H./.H2; assume A7: T in J; for S be Element of H./.H2 holds S * T = T * S proof let S be Element of H./.H2; 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 thesis by A11,A12; end; hence thesis by GROUP_5:77; end; hence thesis by GROUP_2:58; end; Lm4: (Omega).G /\ H = (Omega).H proof 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; the multMagma of ((Omega).G qua Subgroup of G) /\ H = the multMagma of H /\ ((Omega).G qua Subgroup of 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 .= the multMagma of H9 /\ ((Omega).G9 qua Subgroup of G9) .= the multMagma of ((Omega).G9 qua Subgroup of G9) /\ H9; hence thesis by GROUP_2:86; end; Lm5: 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 F1 be strict Subgroup of G; let H,F2 be Subgroup of G; reconsider F=F2 /\ H as Subgroup of F2 by GROUP_2:88; assume A1: F1 is normal Subgroup of F2; then A2: (F1 /\ H) = ((F1 /\ F2) /\ H) by GROUP_2:89 .= F1 /\ (F2 /\ H) by GROUP_2:84; reconsider F1 as normal Subgroup of F2 by A1; F1/\F is normal Subgroup of F; hence thesis by A2,GROUP_6:3; end; registration let G be nilpotent Group; cluster -> nilpotent for Subgroup of G; coherence proof let H be Subgroup of G; 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 st i in dom F & i+1 in dom F 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 P[set,set] means ex I being strict normal Subgroup of G st I=F.$1 & $2=I/\H; A3: for k be Nat st k in Seg len F ex x being Element of the_normal_subgroups_of H st P[k,x] proof let k be Nat; assume k in Seg len F; 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; take I; thus thesis; end; consider R being FinSequence of the_normal_subgroups_of H such that A4: dom R=Seg len F & for i be Nat st i in Seg len F holds P[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; 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; end; A9: for i st i in dom R & i+1 in dom R 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; assume A10: i in dom R & i+1 in dom R; let H1,H2 be strict normal Subgroup of H; assume A11: H1 = R.i & H2 = R.(i+1); 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 thesis by A13,A15,A12,A11,Th22,Lm5; end; take R; thus thesis by A1,A4,A7,A8,A9,FINSEQ_1:def 3; end; end; registration cluster commutative -> nilpotent for Group; correctness proof let G be Group; assume A1: G is commutative; (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 st i in dom F & i+1 in dom F 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; assume A4: i in dom F & i+1 in dom F; now let G1,G2 be Subgroup of G; assume A5: G1 = F.i & G2 = F.(i+1); A6: dom F={1,2} by A3,FINSEQ_1:2,def 3; A7: i in {1,2} & i+1 in {1,2} by A3,A4,FINSEQ_1:2,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 thesis by A5,A9,GROUP_2:65; end; hence thesis; end; hence thesis by A3,Th21; end; cluster cyclic -> nilpotent for Group; coherence; end; theorem Th23: for G,H being strict Group, 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; let h be Homomorphism of G,H; let A be strict Subgroup of G; let a,b be Element of G; 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; 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; end; theorem Th24: for G,H being strict Group, 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; let h being Homomorphism of G,H; let A be strict Subgroup of G; let a,b be Element of G; let H1 be Subgroup of Image h; let a1,b1 be Element of Image h; assume that A1: a1 = h.a and A2: b1 = h.b and A3: H1 = 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.c = h.a * h.b by GROUP_6:def 6; A6: h.:(c * A) = h.c * h.:A by GRSOLV_1:13; c1 * H1 = h.c * h.:A proof now let x; assume x in c1 * H1; then consider Z being Element of Image h such that A7: x = c1 * 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 as Element of G by GROUP_2:42; Z = h.Z1 by A9,FUNCT_1:49; then A11: x = h.c * h.Z1 by A4,A5,A7,GROUP_2:43 .= h.(c * Z1) by GROUP_6:def 6; c * Z1 in c * A by A10,GROUP_2:103; hence x in h.c * h.:A by A11,A6,FUNCT_2:35; end; then A12: c1 * H1 c= h.c * h.:A by TARSKI:def 3; now let x; assume x in h.c * h.:A; then consider y being set such that A13: y in the carrier of G and A14: y in c * A and A15: x = h.y by A6,FUNCT_2:64; reconsider y as Element of G by A13; consider Z being Element of G such that A16: y= c * 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.c * h.Z by A15,A16,GROUP_6:def 6; then x = c1 * Z1 by A4,A5,GROUP_2:43; hence x in c1 * H1 by A18,GROUP_2:103; end; then h.c * h.:A c= c1 * H1 by TARSKI:def 3; hence thesis by A12,XBOOLE_0:def 10; end; hence thesis by GROUP_6:def 6; end; theorem Th25: for G,H being strict Group,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; let h be Homomorphism of G,H; let G1 be strict Subgroup of G; let G2 be strict normal Subgroup of G; let H1 be strict Subgroup of Image h; let H2 be strict normal Subgroup of Image h; 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; 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 be 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; assume A6: T in J; for S be Element of Image h./.H2 holds S * T = T * S proof let S be Element of Image h./.H2; 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 thesis by A10,A11,A17,A18; end; hence thesis by GROUP_5:77; end; hence thesis by GROUP_2:58; end; theorem Th26: for G,H being strict Group, h being Homomorphism of G,H holds 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; let h be Homomorphism of G,H; let A be strict normal Subgroup of G; 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; A1: b in Image h by STRUCT_0:def 5; now consider b1 being Element of G such that A2: b = h.b1 by A1,GROUP_6:45; let x be set; assume x in b * C; 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 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; end; hence thesis by TARSKI:def 3; end; hence thesis by GROUP_3:118; end; registration let G be strict nilpotent Group, H be strict Group, h be Homomorphism of G,H; cluster Image h -> nilpotent; coherence 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 st i in dom F & i+1 in dom F 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 P[set,set] means ex J being strict normal Subgroup of G st J = F.$1 & $2 = h.:(J); A6: for k be Nat st k in Seg len F ex x being Element of the_normal_subgroups_of Image h st P[k,x] proof let k be Nat; assume k in Seg len F; 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 thesis by A7; end; consider Z being FinSequence of the_normal_subgroups_of Image h such that A8: dom Z = Seg len F & for j be Nat st j in Seg len F holds P[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 st i in dom Z & i+1 in dom Z 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; assume A11: i in dom Z & i+1 in dom Z; let H1,H2 be strict normal Subgroup of Image h; assume that A12: H1=Z.i and A13: H2=Z.(i+1); 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 thesis by A16,A19,A18,Th25,GRSOLV_1:12; end; take Z; 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; 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; end; hence thesis by A1,A8,A10,FINSEQ_1:def 3; end; end; registration let G be strict nilpotent Group, N be strict normal Subgroup of G; cluster G./.N -> nilpotent; coherence proof Image nat_hom N = G./.N by GROUP_6:48; hence thesis; end; end; theorem 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 st i in dom F & i+1 in dom F 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; 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 st i in dom F & i+1 in dom F for G1 being strict normal Subgroup of G st G1 = F.i holds [.G1, (Omega).G.] = F.(i+1); for i st i in dom F & i+1 in dom F 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; assume A3: i in dom F & i+1 in dom F; let H1,H2 be strict normal Subgroup of G; assume H1 = F.i & H2 = F.(i+1); then H2 = [.H1, (Omega).G.] by A2,A3; hence thesis by Th15,GROUP_2:54; end; hence thesis by A1,Th21; end; theorem 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 st i in dom F & i+1 in dom F 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; 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 st i in dom F & i+1 in dom F 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; A3: for i st i in dom F & i+1 in dom F 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; assume A4: i in dom F & i+1 in dom F; let H1,H2 be strict normal Subgroup of G; assume A5: H1 = F.i & H2 = F.(i+1); 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 thesis by A2,A4,A5,A6,GROUP_5:82; end; take F; thus thesis by A1,A3; end; theorem 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 st i in dom F & i+1 in dom F 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; 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 st i in dom F & i+1 in dom F 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; A3: for i st i in dom F & i+1 in dom F 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; assume A4: i in dom F & i+1 in dom F; let H1,H2 be strict normal Subgroup of G; assume A5: H1 = F.i & H2 = F.(i+1); 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 thesis by A2,A4,A5,A6,GROUP_5:82; end; take F; thus thesis by A1,A3; end; registration cluster nilpotent -> solvable for Group; correctness proof let G be Group; assume G is nilpotent; 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 st i in dom F & i+1 in dom F 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 st i in dom R & i+1 in dom R 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; assume A3: i in dom R & i+1 in dom R; 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; assume A5: H1 = R.i & H2 = R.(i+1); for N being normal Subgroup of H1 st N = H2 holds H1./.N is commutative proof let N be normal Subgroup of H1; assume A6: N = H2; 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; end; hence thesis by A1,A3,A5,A4,GROUP_6:8; end; take R; thus thesis by A1,A2; end; end;