:: Solvable Groups :: by Katarzyna Zawadzka :: :: Received October 23, 1994 :: Copyright (c) 1994-2017 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 NUMBERS, SUBSET_1, GROUP_1, FINSEQ_1, GROUP_3, XXREAL_0, CARD_1, FUNCT_1, RLSUB_1, GROUP_2, RELAT_1, ARYTM_3, STRUCT_0, PRE_TOPC, GROUP_6, BINOP_1, TARSKI, XBOOLE_0, QC_LANG1, WELLORD1, NAT_1, FUNCT_2, ALGSTR_0, GRAPH_1, GRSOLV_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, STRUCT_0, ALGSTR_0, BINOP_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, GR_CY_1, FINSEQ_1, GROUP_1, GROUP_2, GROUP_3, GROUP_6, XXREAL_0; constructors BINOP_1, FINSUB_1, REALSET1, GROUP_6, GR_CY_1, RELSET_1; registrations XBOOLE_0, FUNCT_1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, GROUP_2, GROUP_3, GROUP_6, GR_CY_1, ORDINAL1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions TARSKI; equalities GROUP_2, RELAT_1, ALGSTR_0; expansions TARSKI; theorems FINSEQ_1, BINOP_1, GROUP_2, GROUP_3, TARSKI, GROUP_6, FINSEQ_2, FUNCT_1, FUNCT_2, RELAT_1, XBOOLE_0, XBOOLE_1, NAT_1, GROUP_1, STRUCT_0; schemes FINSEQ_1; begin reserve i for Element of NAT; definition let IT be Group; attr IT is solvable means :Def1: ex F being FinSequence of Subgroups 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 Subgroup of IT st G1 = F.i & G2 = F.(i+1) holds G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1 st N = G2 holds G1./.N is commutative; end; registration cluster solvable strict for Group; existence proof set G = the Group; take H=(1).G; thus H is solvable proof rng <*H*> c=Subgroups H proof let x be object; A1: rng <*H*> ={ H } by FINSEQ_1:39; assume x in rng<*H*>; then x=H by A1,TARSKI:def 1; then x is strict Subgroup of H by GROUP_2:54; hence thesis by GROUP_3:def 1; end; then reconsider F=<*H*> as FinSequence of Subgroups H by FINSEQ_1:def 4; take F; A2: len F=1 by FINSEQ_1:39; A3: for i st i in dom F & i+1 in dom F for G1,G2 being Subgroup of H st G1=F.i & G2=F.(i+1) holds G2 is normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative proof let i; assume that A4: i in dom F and A5: i+1 in dom F; let G1,G2 be Subgroup of H; assume that G1=F.i and G2=F.(i+1); A6: dom F={1} by A2,FINSEQ_1:2,def 3; then i=1 by A4,TARSKI:def 1; hence thesis by A5,A6,TARSKI:def 1; end; F.(len F)=H by A2,FINSEQ_1:40 .=(1).H by GROUP_2:63; hence thesis by A2,A3,FINSEQ_1:40; end; thus thesis; end; end; theorem Th1: for G being Group, H,F1,F2 being strict Subgroup of G st F1 is normal Subgroup of F2 holds F1 /\ H is normal Subgroup of F2 /\ H proof let G be Group; let H,F1,F2 be strict 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; theorem for G being Group for F2 being Subgroup of G for F1 being normal Subgroup of F2 for a,b being Element of F2 holds (a*F1)*(b*F1) = a*b*F1 proof let G be Group; let F2 be Subgroup of G; let F1 be normal Subgroup of F2; let a,b be Element of F2; A1: (nat_hom F1).a=(a*F1) & (nat_hom F1).b=(b*F1) by GROUP_6:def 8; A2: @((nat_hom F1).a)=(nat_hom F1).a & @((nat_hom F1).b)=(nat_hom F1).b by GROUP_6:def 5; thus a*b*F1 =(nat_hom F1).(a*b) by GROUP_6:def 8 .=((nat_hom F1).a) *((nat_hom F1).b) by GROUP_6:def 6 .=(a*F1 )*(b*F1) by A1,A2,GROUP_6:19; end; theorem for G being Group for H,F2 being Subgroup of G for F1 being normal Subgroup of F2 holds for G2 being Subgroup of G st G2 = H /\ F2 for G1 being normal Subgroup of G2 st G1 = H /\ F1 ex G3 being Subgroup of F2./.F1 st G2./.G1, G3 are_isomorphic proof let G be Group; let H,F2 be Subgroup of G; let F1 be normal Subgroup of F2; reconsider G2=H /\ F2 as strict Subgroup of G; consider f being Function such that A1: f=(nat_hom F1)|(the carrier of H); reconsider f1=nat_hom F1 as Function of the carrier of F2,the carrier of F2 ./.F1; A2: the carrier of F2=carr(F2) & the carrier of H= carr(H); dom f1=the carrier of F2 by FUNCT_2:def 1; then A3: dom f=(the carrier of F2) /\ (the carrier of H) by A1,RELAT_1:61 .=carr(F2/\ H) by A2,GROUP_2:81 .= the carrier of (H /\ F2); rng ((nat_hom F1)|(the carrier of H)) c=rng (nat_hom F1) by RELAT_1:70; then reconsider f as Function of the carrier of H/\F2,the carrier of F2./.F1 by A1,A3, FUNCT_2:2; for a,b being Element of H /\F2 holds f.(a * b) = f.a * f.b proof let a,b be Element of H /\F2; A4: the carrier of H /\F2=carr(H) /\ carr(F2) by GROUP_2:def 10; then reconsider a9=a, b9=b as Element of F2 by XBOOLE_0:def 4; b in carr(H) by A4,XBOOLE_0:def 4; then A5: ((nat_hom F1)|(the carrier of H)).b=(nat_hom F1).b by FUNCT_1:49; a*b in carr(H) by A4,XBOOLE_0:def 4; then A6: ((nat_hom F1)|(the carrier of H)).(a*b)=(nat_hom F1).(a*b) by FUNCT_1:49; H /\ F2 is Subgroup of F2 by GROUP_2:88; then A7: a*b=a9 *b9 by GROUP_2:43; a in carr(H) by A4,XBOOLE_0:def 4; then ((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a by FUNCT_1:49; hence thesis by A1,A7,A5,A6,GROUP_6:def 6; end; then reconsider f as Homomorphism of H/\F2,F2./.F1 by GROUP_6:def 6; A8: (the carrier of H) /\ (the carrier of F2) =carr(H/\ F2) by A2,GROUP_2:81 .= the carrier of (H /\ F2); A9: Ker f=H /\ F1 proof reconsider L=Ker f as Subgroup of G by GROUP_2:56; for g be Element of G holds g in L iff g in H /\ F1 proof let x be Element of G; thus x in L implies x in H /\ F1 proof assume A10: x in L; then x in carr(Ker f) by STRUCT_0:def 5; then reconsider a=x as Element of H/\F2; A11: the carrier of H /\F2=carr(H) /\ carr(F2) by GROUP_2:def 10; then reconsider a9=a as Element of F2 by XBOOLE_0:def 4; A12: a in carr(H) by A11,XBOOLE_0:def 4; then A13: a in H by STRUCT_0:def 5; ((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a by A12,FUNCT_1:49; then A14: f.a= a9 *F1 by A1,GROUP_6:def 8; f.a =1_(F2./.F1) by A10,GROUP_6:41 .=carr F1 by GROUP_6:24; then a9 in F1 by A14,GROUP_2:113; hence thesis by A13,GROUP_2:82; end; thus x in H /\ F1 implies x in L proof reconsider F19=F1 as Subgroup of G; A15: (the carrier of H) /\ (the carrier of F1) =carr(H) /\ carr(F19) .= the carrier of (H /\ F1) by GROUP_2:def 10; assume x in H /\ F1; then A16: x in carr(H /\F1) by STRUCT_0:def 5; the carrier of F1 c= the carrier of F2 by GROUP_2:def 5; then the carrier of (H /\ F1) c= the carrier of (H /\ F2) by A8,A15, XBOOLE_1:26; then reconsider a=x as Element of H/\F2 by A16; x in the carrier of F1 by A16,A15,XBOOLE_0:def 4; then A17: a in F1 by STRUCT_0:def 5; A18: the carrier of H /\F2=carr(H) /\ carr(F2) by GROUP_2:def 10; then reconsider a9=a as Element of F2 by XBOOLE_0:def 4; a in carr(H) by A18,XBOOLE_0:def 4; then ((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a by FUNCT_1:49; then f.a= a9 *F1 by A1,GROUP_6:def 8 .=carr F1 by A17,GROUP_2:113 .=1_(F2./.F1) by GROUP_6:24; hence thesis by GROUP_6:41; end; end; hence thesis by GROUP_2:def 6; end; reconsider G1=Ker f as normal Subgroup of G2; G2 ./. G1,Image f are_isomorphic by GROUP_6:78; hence thesis by A9; end; theorem Th4: for G being Group for H,F2 being Subgroup of G for F1 being normal Subgroup of F2 holds for G2 being Subgroup of G st G2 = F2/\H for G1 being normal Subgroup of G2 st G1 = F1/\H ex G3 being Subgroup of F2./.F1 st G2./.G1, G3 are_isomorphic proof let G be Group; let H,F2 be Subgroup of G; let F1 be normal Subgroup of F2; reconsider G2=F2 /\ H as strict Subgroup of G; consider f being Function such that A1: f=(nat_hom F1)|(the carrier of H); reconsider f1=nat_hom F1 as Function of the carrier of F2,the carrier of F2 ./.F1; A2: the carrier of F2=carr(F2) & the carrier of H= carr(H); dom f1=the carrier of F2 by FUNCT_2:def 1; then A3: dom f=(the carrier of F2) /\ (the carrier of H) by A1,RELAT_1:61 .=the carrier of (F2 /\ H) by A2,GROUP_2:def 10; rng ((nat_hom F1)|(the carrier of H)) c=rng (nat_hom F1) by RELAT_1:70; then reconsider f as Function of the carrier of F2 /\ H,the carrier of F2./.F1 by A1,A3, FUNCT_2:2; for a,b being Element of F2 /\ H holds f.(a * b) = f.a * f.b proof let a,b be Element of F2 /\ H; A4: the carrier of F2 /\ H=carr(H) /\ carr(F2) by GROUP_2:def 10; then reconsider a9=a, b9=b as Element of F2 by XBOOLE_0:def 4; b in carr(H) by A4,XBOOLE_0:def 4; then A5: ((nat_hom F1)|(the carrier of H)).b=(nat_hom F1).b by FUNCT_1:49; a*b in carr(H) by A4,XBOOLE_0:def 4; then A6: ((nat_hom F1)|(the carrier of H)).(a*b)=(nat_hom F1).(a*b) by FUNCT_1:49; F2 /\ H is Subgroup of F2 by GROUP_2:88; then A7: a*b=a9 *b9 by GROUP_2:43; a in carr(H) by A4,XBOOLE_0:def 4; then ((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a by FUNCT_1:49; hence thesis by A1,A7,A5,A6,GROUP_6:def 6; end; then reconsider f as Homomorphism of F2 /\ H,F2./.F1 by GROUP_6:def 6; A8: (the carrier of H) /\ (the carrier of F2) =carr(F2 /\ H) by A2,GROUP_2:81 .= the carrier of (F2 /\ H); A9: Ker f=F1 /\ H proof reconsider L=Ker f as Subgroup of G by GROUP_2:56; for g be Element of G holds g in L iff g in F1 /\ H proof let x be Element of G; thus x in L implies x in F1 /\ H proof assume A10: x in L; then x in carr(Ker f) by STRUCT_0:def 5; then reconsider a=x as Element of F2 /\ H; A11: the carrier of F2 /\ H=carr(H) /\ carr(F2) by GROUP_2:def 10; then reconsider a9=a as Element of F2 by XBOOLE_0:def 4; A12: a in carr(H) by A11,XBOOLE_0:def 4; then A13: a in H by STRUCT_0:def 5; ((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a by A12,FUNCT_1:49; then A14: f.a= a9 *F1 by A1,GROUP_6:def 8; f.a =1_(F2./.F1) by A10,GROUP_6:41 .=carr F1 by GROUP_6:24; then a9 in F1 by A14,GROUP_2:113; hence thesis by A13,GROUP_2:82; end; thus x in F1 /\ H implies x in L proof reconsider F19=F1 as Subgroup of G; A15: (the carrier of H) /\ (the carrier of F1) =carr(H) /\ carr(F19) .= the carrier of (F1 /\ H) by GROUP_2:def 10; assume x in F1 /\ H; then A16: x in carr(F1 /\ H) by STRUCT_0:def 5; the carrier of F1 c= the carrier of F2 by GROUP_2:def 5; then the carrier of (F1 /\ H) c= the carrier of (F2 /\ H) by A8,A15, XBOOLE_1:26; then reconsider a=x as Element of F2 /\ H by A16; x in the carrier of F1 by A16,A15,XBOOLE_0:def 4; then A17: a in F1 by STRUCT_0:def 5; A18: the carrier of F2 /\ H=carr(H) /\ carr(F2) by GROUP_2:def 10; then reconsider a9=a as Element of F2 by XBOOLE_0:def 4; a in carr(H) by A18,XBOOLE_0:def 4; then ((nat_hom F1)|(the carrier of H)).a=(nat_hom F1).a by FUNCT_1:49; then f.a= a9 *F1 by A1,GROUP_6:def 8 .=carr F1 by A17,GROUP_2:113 .=1_(F2./.F1) by GROUP_6:24; hence thesis by GROUP_6:41; end; end; hence thesis by GROUP_2:def 6; end; reconsider G1=Ker f as normal Subgroup of G2; G2 ./. G1,Image f are_isomorphic by GROUP_6:78; hence thesis by A9; end; theorem for G being strict solvable Group, H being strict Subgroup of G holds H is solvable proof let G be strict solvable Group; let H be strict Subgroup of G; consider F being FinSequence of Subgroups 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 Subgroup of G st G1=F.i & G2=F.(i+1) holds G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative by Def1; defpred P[set,set] means ex I being strict Subgroup of G st I=F.\$1 & \$2=I /\ H; A5: for k be Nat st k in Seg len F ex x being Element of Subgroups 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 Subgroups G by FINSEQ_2:11; then reconsider I=F.k as strict Subgroup of G by GROUP_3:def 1; reconsider x=I /\ H as strict Subgroup of H by GROUP_2:88; reconsider y=x as Element of Subgroups H by GROUP_3:def 1; take y; take I; thus thesis; end; consider R being FinSequence of Subgroups H such that A6: 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(A5); A7: for i st i in dom R & i+1 in dom R for H1,H2 being strict Subgroup of H 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 that A8: i in dom R and A9: i+1 in dom R; consider J being strict Subgroup of G such that A10: J=F.(i+1) and A11: R.(i+1)=J /\ H by A6,A9; consider I being strict Subgroup of G such that A12: I=F.i and A13: R.i=I /\ H by A6,A8; let H1,H2 be strict Subgroup of H; assume that A14: H1=R.i and A15: H2=R.(i+1); A16: i in dom F & i+1 in dom F by A6,A8,A9,FINSEQ_1:def 3; then reconsider J1=J as strict normal Subgroup of I by A4,A12,A10; A17: for N being strict normal Subgroup of H1 st N=H2 holds H1./.N is commutative proof let N be strict normal Subgroup of H1; assume N=H2; then consider G3 being Subgroup of I./.J1 such that A18: H1 ./. N, G3 are_isomorphic by A14,A15,A13,A11,Th4; consider h being Homomorphism of H1./. N,G3 such that A19: h is bijective by A18,GROUP_6:def 11; A20: h is one-to-one by A19,FUNCT_2:def 4; A21: I ./.J1 is commutative by A4,A12,A10,A16; now let a,b be Element of H1./.N; consider a9 being Element of G3 such that A22: a9=h.a; consider b9 being Element of G3 such that A23: b9=h.b; the multF of G3 is commutative by A21,GROUP_3:2; then A24: a9*b9=b9*a9 by BINOP_1:def 2; thus (the multF of H1./.N).(a,b)=h".(h.(a*b)) by A20,FUNCT_2:26 .=h".(h.b*h.a) by A22,A23,A24,GROUP_6:def 6 .=h".(h.(b*a)) by GROUP_6:def 6 .=(the multF of H1./.N).(b,a) by A20,FUNCT_2:26; end; then the multF of (H1./.N) is commutative by BINOP_1:def 2; hence thesis by GROUP_3:2; end; H2=J1/\H by A15,A11; hence thesis by A14,A13,A17,Th1; end; A25: len R=len F by A6,FINSEQ_1:def 3; A26: len R >0 by A1,A6,FINSEQ_1:def 3; A27: R.1=(Omega).H proof 1<=len R by A26,NAT_1:14; then 1 in Seg len F by A25,FINSEQ_1:1; then ex I being strict Subgroup of G st I=F.1 & R.1=I /\ H by A6; hence thesis by A2,GROUP_2:86; end; take R; R.(len R)= (1).H proof ex I being strict Subgroup of G st I=F.(len R) & R.(len R )=I /\ H by A1,A6 ,A25,FINSEQ_1:3; hence R.(len R)=(1).G by A3,A25,GROUP_2:85 .=(1).H by GROUP_2:63; end; hence thesis by A1,A6,A27,A7,FINSEQ_1:def 3; end; theorem for G being Group st ex F being FinSequence of Subgroups 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 Subgroup of G st G1=F.i & G2=F.(i+1) holds G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2 holds G1./.N is cyclic Group holds G is solvable proof let G be Group; given F being FinSequence of Subgroups 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 Subgroup of G st G1=F.i & G2=F.(i+1) holds G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2 holds G1./.N is cyclic Group ); take F; thus thesis by A1; end; theorem for G being strict commutative Group holds G is solvable proof let G be strict commutative Group; (Omega).G in Subgroups G & (1).G in Subgroups G by GROUP_3:def 1; then <*(Omega).G,(1).G*>is FinSequence of Subgroups G by FINSEQ_2:13; then consider F being FinSequence of Subgroups G such that A1: F=<*(Omega).G,(1).G*>; A2: F.1=(Omega).G by A1,FINSEQ_1:44; A3: len F=2 by A1,FINSEQ_1:44; A4: F.2=(1).G by A1,FINSEQ_1:44; for i st i in dom F & i+1 in dom F for G1,G2 being strict Subgroup of G st G1=F.i & G2=F.(i+1) holds G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative proof let i; assume that A5: i in dom F and A6: i+1 in dom F; now let G1,G2 be strict Subgroup of G; assume A7: G1=F.i & G2=F.(i+1); dom F={1,2} by A3,FINSEQ_1:2,def 3; then A8: i=1 or i=2 by A5,TARSKI:def 2; A9: i+1 in{1,2} by A3,A6,FINSEQ_1:2,def 3; for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative by A2,A4,A7,A9,A8,GROUP_6:71,77,TARSKI:def 2; hence G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative by A1,A2,A7,A9,A8,FINSEQ_1:44,TARSKI:def 2; end; hence thesis; end; hence thesis by A3,A2,A4; end; definition let G,H be Group; let g be Homomorphism of G,H; let A be Subgroup of G; func g|A -> Homomorphism of A,H equals g|(the carrier of A); coherence proof A1: the carrier of A c= the carrier of G by GROUP_2:def 5; then reconsider f=g|(the carrier of A) as Function of the carrier of A,the carrier of H by FUNCT_2:32; now A2: for a,b being Element of G holds (the multF of H).(g.a, g.b)=g.((the multF of G).(a,b)) proof let a,b be Element of G; thus (the multF of H).(g.a, g.b)=g.a * g.b .=g.(a*b) by GROUP_6:def 6 .=g.((the multF of G).(a,b)); end; let a,b be Element of A; A3: f.a=g.a & f.b=g.b by FUNCT_1:49; A4: (the multF of G).(a,b)=a*b proof reconsider b9=b as Element of G by A1; reconsider a9=a as Element of G by A1; thus (the multF of G).(a,b)=a9* b9 .=a*b by GROUP_2:43; end; a is Element of G & b is Element of G by A1; hence f.a * f.b = g.((the multF of G).(a,b))by A3,A2 .= f.(a * b) by A4,FUNCT_1:49; end; hence thesis by GROUP_6:def 6; end; end; definition let G,H be Group; let g be Homomorphism of G,H; let A be Subgroup of G; func g.:A -> strict Subgroup of H equals Image (g| A); coherence; end; theorem Th8: for G,H being Group, g being Homomorphism of G,H for A being Subgroup of G holds the carrier of (g.: A) = g.:(the carrier of A) proof let G,H be Group; let g be Homomorphism of G,H; let A be Subgroup of G; thus the carrier of (g.: A)=rng (g|A) by GROUP_6:44 .=g.:(the carrier of A) by RELAT_1:115; end; theorem Th9: for G,H being Group, h being Homomorphism of G,H holds for A being strict Subgroup of G holds Image(h|A) is strict Subgroup of Image h proof let G,H be Group; let h be Homomorphism of G,H; let A be strict Subgroup of G; A1: the carrier of A c= the carrier of G & h.:(the carrier of G) = the carrier of Image h by GROUP_2:def 5,GROUP_6:def 10; the carrier of Image (h|A)=rng (h|A) by GROUP_6:44 .=h.:(the carrier of A) by RELAT_1:115; hence thesis by A1,GROUP_2:57,RELAT_1:123; end; theorem for G,H being Group, h being Homomorphism of G,H holds for A being strict Subgroup of G holds h.:A is strict Subgroup of Image h by Th9; theorem Th11: for G,H being Group, h being Homomorphism of G,H holds h.:((1).G)=(1).H & h.:((Omega).G)=(Omega).(Image h) proof let G,H be Group; let h be Homomorphism of G,H; A1: dom h=the carrier of G by FUNCT_2:def 1; A2: the carrier of (1).H={1_H} by GROUP_2:def 7; the carrier of (1).G={1_G} by GROUP_2:def 7; then the carrier of h.:((1).G)=Im(h,1_G) by Th8 .={h.(1_G)} by A1,FUNCT_1:59 .= the carrier of (1).H by A2,GROUP_6:31; hence h.:((1).G)= (1).H by GROUP_2:59; the carrier of h.:((Omega).G)=h.:(the carrier of G) by Th8 .=the carrier of (Omega).(Image h) by GROUP_6:def 10; hence thesis by GROUP_2:59; end; theorem Th12: for G,H being Group, h being Homomorphism of G,H for A,B being Subgroup of G holds A is Subgroup of B implies h.:A is Subgroup of h.:B proof let G,H be Group; let h be Homomorphism of G,H; let A,B be Subgroup of G; assume A is Subgroup of B; then the carrier of A c= the carrier of B by GROUP_2:def 5; then A1: h.:(the carrier of A)c= h.:(the carrier of B ) by RELAT_1:123; the carrier of h.:B= h.:(the carrier of B) by Th8; then the carrier of h.:A c= the carrier of h.:B by A1,Th8; hence thesis by GROUP_2:57; end; theorem Th13: for G,H being strict Group, h being Homomorphism of G,H for A being strict Subgroup of G for a being Element of G holds h.a* h.:A=h.:(a*A) & h.:A * h.a=h.:(A*a) proof let G,H be strict Group; let h be Homomorphism of G,H; let A be strict Subgroup of G; let a be Element of G; now let x be object; assume x in h.:(a *A); then consider y being object such that A1: y in the carrier of G and A2: y in a*A and A3: x = h.y by FUNCT_2:64; reconsider y as Element of G by A1; consider b being Element of G such that A4: y=a* b and A5: b in A by A2,GROUP_2:103; b in the carrier of A by A5,STRUCT_0:def 5; then h.b in h.:(the carrier of A) by FUNCT_2:35; then h.b in the carrier of h.: A by Th8; then A6: h.b in h.:A by STRUCT_0:def 5; x=h.a *h.b by A3,A4,GROUP_6:def 6; hence x in h.a * h.:A by A6,GROUP_2:103; end; then A7: h.:(a * A) c= h.a *h.:A; now let x be object; assume x in h.a *h.:A; then consider b1 being Element of H such that A8: x = h.a * b1 and A9: b1 in h.:A by GROUP_2:103; consider b being Element of A such that A10: b1=(h|A).b by A9,GROUP_6:45; A11: b in A by STRUCT_0:def 5; reconsider b as Element of G by GROUP_2:42; b1=h.b by A10,FUNCT_1:49; then A12: x=h.(a*b) by A8,GROUP_6:def 6; a* b in a*A by A11,GROUP_2:103; hence x in h.:(a*A) by A12,FUNCT_2:35; end; then h.a *h.:A c= h.:(a * A); hence h.a *h.:A = h.:(a * A) by A7,XBOOLE_0:def 10; now let x be object; assume x in h.:(A* a); then consider y being object such that A13: y in the carrier of G and A14: y in A* a and A15: x = h.y by FUNCT_2:64; reconsider y as Element of G by A13; consider b being Element of G such that A16: y=b* a and A17: b in A by A14,GROUP_2:104; b in the carrier of A by A17,STRUCT_0:def 5; then h.b in h.:(the carrier of A) by FUNCT_2:35; then h.b in the carrier of h.: A by Th8; then A18: h.b in h.:A by STRUCT_0:def 5; x=h.b *h.a by A15,A16,GROUP_6:def 6; hence x in h.:A*h.a by A18,GROUP_2:104; end; then A19: h.:(A*a) c= h.:A*h.a; now let x be object; assume x in h.:A*h.a; then consider b1 being Element of H such that A20: x = b1*h.a and A21: b1 in h.:A by GROUP_2:104; consider b being Element of A such that A22: b1=(h|A).b by A21,GROUP_6:45; A23: b in A by STRUCT_0:def 5; reconsider b as Element of G by GROUP_2:42; b1=h.b by A22,FUNCT_1:49; then A24: x=h.(b*a) by A20,GROUP_6:def 6; b* a in A*a by A23,GROUP_2:104; hence x in h.:(A*a) by A24,FUNCT_2:35; end; then h.:A*h.a c= h.:(A* a); hence thesis by A19,XBOOLE_0:def 10; end; theorem Th14: for G,H being strict Group, h being Homomorphism of G,H for A,B being Subset of G holds h.:A* h.:B=h.:(A*B) proof let G,H be strict Group, h be Homomorphism of G,H; let A,B be Subset of G; now let z be object; assume z in h.:(A)*h.:(B); then consider z1,z2 being Element of H such that A1: z=z1 *z2 and A2: z1 in h.:(A) and A3: z2 in h.:(B); consider z4 being object such that A4: z4 in the carrier of G and A5: z4 in B and A6: z2=h.z4 by A3,FUNCT_2:64; reconsider z4 as Element of G by A4; consider z3 being object such that A7: z3 in the carrier of G and A8: z3 in A and A9: z1=h.z3 by A2,FUNCT_2:64; reconsider z3 as Element of G by A7; A10: z3 * z4 in (A) *(B) by A8,A5; z=h.(z3* z4) by A1,A9,A6,GROUP_6:def 6; hence z in h.:((A) *(B)) by A10,FUNCT_2:35; end; then A11: h.:(A)*h.:(B)c= h.:((A) *(B)); now let z be object; assume z in h.:((A) *(B)); then consider x being object such that A12: x in the carrier of G and A13: x in (A)*(B) and A14: z=h.x by FUNCT_2:64; reconsider x as Element of G by A12; consider z1,z2 being Element of G such that A15: x=z1 *z2 and A16: z1 in(A) & z2 in (B) by A13; A17: h.z1 in h.:(A) & h.z2 in h.:(B) by A16,FUNCT_2:35; z=h.z1 * h.z2 by A14,A15,GROUP_6:def 6; hence z in h.:(A)* h.:(B) by A17; end; then h.:((A) *(B)) c=h.:(A)*h.:(B); hence thesis by A11,XBOOLE_0:def 10; end; theorem Th15: for G,H being strict Group, h being Homomorphism of G,H for A,B being strict Subgroup of G holds A is strict normal Subgroup of B implies h.:A is strict normal Subgroup of h.:B proof let G,H be strict Group; let h be Homomorphism of G,H; let A,B be strict Subgroup of G; assume A is strict normal Subgroup of B; then reconsider A1=A as strict normal Subgroup of B; reconsider C=h.:A1 as strict Subgroup of h.:B by Th12; for b2 being Element of h.:B holds b2* C c= C * b2 proof let b2 be Element of h.:B; A1: b2 in h.:B by STRUCT_0:def 5; now consider b1 being Element of B such that A2: b2=(h|B).b1 by A1,GROUP_6:45; reconsider b1 as Element of G by GROUP_2:42; A3: b2=h.b1 by A2,FUNCT_1:49; reconsider b=b1 as Element of B; let x be object; assume x in b2* C; then consider g being Element of h.:B such that A4: x = b2 * g and A5: g in C by GROUP_2:103; consider g1 being Element of A1 such that A6: g=(h|A1).g1 by A5,GROUP_6:45; reconsider g1 as Element of G by GROUP_2:42; g=h.g1 by A6,FUNCT_1:49; then A7: x =h.b1 * h.g1 by A3,A4,GROUP_2:43 .=h.(b1 *g1) by GROUP_6:def 6; g1 in A1 by STRUCT_0:def 5; then A8: b1 * g1 in b1 * A1 by GROUP_2:103; A9: h.:(A1 * b1) = h.:A1 * h.b1 by Th13; b1 * A1=b * A1 by GROUP_6:2 .=A1 * b by GROUP_3:117 .=A1 * b1 by GROUP_6:2; then x in h.:(A1 *b1) by A7,A8,FUNCT_2:35; hence x in C* b2 by A3,A9,GROUP_6:2; end; hence thesis; end; hence thesis by GROUP_3:118; end; theorem for G,H being strict Group, h being Homomorphism of G,H holds G is solvable Group implies Image h is solvable proof let G,H be strict Group; let h be Homomorphism of G,H; assume G is solvable Group; then consider F being FinSequence of Subgroups 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 Subgroup of G st G1=F.i & G2=F.(i+1) holds G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative by Def1; 1 <= len F by A1,NAT_1:14; then A5: 1 in Seg len F by FINSEQ_1:1; defpred P[set,set] means ex J being strict 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 Subgroups 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 Subgroups G by FINSEQ_2:11; then F.k is strict Subgroup of G by GROUP_3:def 1; then consider A being strict Subgroup of G such that A7: A=F.k; h.:(A) is strict Subgroup of Image h by Th9; then h.:(A) in Subgroups Image h by GROUP_3:def 1; hence thesis by A7; end; consider z being FinSequence of Subgroups 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 G1,G2 being strict Subgroup of Image h st G1=z.i & G2=z.(i+1) holds G2 is strict normal Subgroup of G1 & for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative proof let i; assume that A11: i in dom z and A12: i+1 in dom z; let G1,G2 be strict Subgroup of Image h; assume that A13: G1=z.i and A14: G2=z.(i+1); consider A being strict Subgroup of G such that A15: A=F.i and A16: G1=h.:A by A8,A11,A13; consider B being strict Subgroup of G such that A17: B=F.(i+1) and A18: G2=h.:B by A8,A12,A14; A19: for N being normal Subgroup of G1 st N=G2 holds G1./.N is commutative proof let N be normal Subgroup of G1; assume A20: N=G2; now let x,y be Element of G1./.N; x in G1./.N by STRUCT_0:def 5; then consider a being Element of G1 such that A21: x= a* N and x=N* a by GROUP_6:23; y in G1./.N by STRUCT_0:def 5; then consider b being Element of G1 such that A22: y= b* N and y=N* b by GROUP_6:23; x in the carrier of G1./.N; then A23: x in Cosets N by GROUP_6:17; then reconsider x1=x as Subset of G1; b in h.:A by A16,STRUCT_0:def 5; then consider b1 being Element of A such that A24: b=(h|A).b1 by GROUP_6:45; reconsider b1 as Element of G by GROUP_2:42; b=h.b1 by A24,FUNCT_1:49; then A25: b * N= h.b1 * h.:B by A18,A20,GROUP_6:2 .=h .:(b1 *B ) by Th13; then reconsider y2=h.:(b1 *B) as Subset of G1; a in h.:A by A16,STRUCT_0:def 5; then consider a1 being Element of A such that A26: a=(h|A).a1 by GROUP_6:45; reconsider a1 as Element of G by GROUP_2:42; a=h.a1 by A26,FUNCT_1:49; then A27: a * N= h.a1 * h.:B by A18,A20,GROUP_6:2 .=h.:(a1*B) by Th13; then reconsider x2=h.:(a1 *B) as Subset of G1; now let z be object; assume z in x2*y2; then consider z1,z2 being Element of G1 such that A28: z=z1 *z2 and A29: z1 in x2 and A30: z2 in y2; reconsider z22=z2 as Element of H by A30; reconsider z11=z1 as Element of H by A29; z=z11 * z22 by A28,GROUP_2:43; hence z in h.:(a1 *B) *h.:(b1 * B) by A29,A30; end; then A31: x2 * y2 c= h.:(a1 *B) *h.:(b1 * B); A32: (a1*B)*(b1*B)=(b1 *B)*(a1*B) proof reconsider K=B as normal Subgroup of A by A4,A9,A11,A12,A15,A17; reconsider a2=a1,b2=b1 as Element of A; A33: a1*B=a2 *K by GROUP_6:2; then reconsider A1=a1 * B as Subset of A; A34: b1 *B=b2*K by GROUP_6:2; then reconsider B1=b1 * B as Subset of A; reconsider a12=a1 * B,b12=b1 * B as Element of Cosets K by A33,A34, GROUP_6:14; a2 * K is Element of A./.K by GROUP_6:22; then reconsider a11=a12 as Element of A./.K by GROUP_6:2; b2 * K is Element of A./.K by GROUP_6:22; then reconsider b11=b12 as Element of A./.K by GROUP_6:2; now let x be object; assume x in (a1 *B) *(b1 * B); then consider z1,z2 being Element of G such that A35: x=z1 *z2 and A36: z1 in(a1*B) & z2 in (b1*B); z1 in A1 & z2 in B1 by A36; then reconsider z11=z1, z22=z2 as Element of A; z1*z2=z11*z22 by GROUP_2:43; hence x in A1* B1 by A35,A36; end; then A37: (a1*B)*(b1 *B) c= A1*B1; now let x be object; assume x in (b1 *B) *(a1 * B); then consider z1,z2 being Element of G such that A38: x=z1 *z2 and A39: z1 in(b1*B) & z2 in (a1*B); z1 in B1 & z2 in A1 by A39; then reconsider z11=z1, z22=z2 as Element of A; z1*z2=z11*z22 by GROUP_2:43; hence x in B1*A1 by A38,A39; end; then A40: (b1*B)*(a1*B) c= B1*A1; now let x be object; assume x in B1*A1; then consider z1,z2 being Element of A such that A41: x=z1 *z2 and A42: z1 in B1 & z2 in A1; reconsider z11=z1, z22=z2 as Element of G by A42; z1*z2=z11*z22 by GROUP_2:43; hence x in (b1*B)*(a1*B)by A41,A42; end; then A43: B1*A1 c=(b1*B)*(a1*B); A44: A ./. K is commutative Group by A4,A9,A11,A12,A15,A17; A45: for a,b being Element of A./.K holds (the multF of A./.K).(a,b) = (the multF of A./.K).(b,a) by A44,BINOP_1:def 2,GROUP_3:2; A46: A1*B1=(CosOp K).(a11,b11) by GROUP_6:def 3 .=(the multF of A./.K).(a12,b12) by GROUP_6:18 .=(the multF of A./.K).(b11,a11) by A45 .=(CosOp K).(b12,a12) by GROUP_6:18 .=B1*A1 by GROUP_6:def 3; now let x be object; assume x in A1 * B1; then consider z1,z2 being Element of A such that A47: x=z1 *z2 and A48: z1 in A1 & z2 in B1; reconsider z11=z1, z22=z2 as Element of G by A48; z1*z2=z11*z22 by GROUP_2:43; hence x in (a1*B)*(b1 *B)by A47,A48; end; then A1*B1 c=(a1*B)*(b1 *B); then (a1*B)*(b1 *B)=A1*B1 by A37,XBOOLE_0:def 10; hence thesis by A46,A40,A43,XBOOLE_0:def 10; end; now let z be object; assume z in y2*x2; then consider z1,z2 being Element of G1 such that A49: z=z1 *z2 and A50: z1 in y2 and A51: z2 in x2; reconsider z22=z2 as Element of H by A51; reconsider z11=z1 as Element of H by A50; z=z11 * z22 by A49,GROUP_2:43; hence z in h.:(b1 *B) *h.:(a1 * B) by A50,A51; end; then A52: y2*x2 c= h.:(b1 *B) *h.:(a1 * B); A53: h.:(b1*B)*h.:(a1 * B)=h.:((b1 *B)*(a1 *B)) by Th14; now let z be object; assume z in h.:(b1 *B) *h.:(a1 * B); then consider x being object such that A54: x in the carrier of G and A55: x in (b1*B)*(a1*B) and A56: z=h.x by A53,FUNCT_2:64; reconsider x as Element of G by A54; consider z1,z2 being Element of G such that A57: x=z1 *z2 and A58: z1 in(b1*B) and A59: z2 in (a1*B) by A55; A60: h.z2 in x2 by A59,FUNCT_2:35; then reconsider z22=h.z2 as Element of G1; A61: h.z1 in y2 by A58,FUNCT_2:35; then reconsider z11=h.z1 as Element of G1; z=h.z1 * h.z2 by A56,A57,GROUP_6:def 6 .=z11 *z22 by GROUP_2:43; hence z in y2*x2 by A61,A60; end; then h.:(b1 *B) *h.:(a1 * B) c= y2*x2; then A62: y2*x2 =h.:(b1*B)* h.:(a1*B) by A52,XBOOLE_0:def 10; A63: h.:(a1*B)*h.:(b1 * B)=h.:((a1 *B)*(b1 *B)) by Th14; now let z be object; assume z in h.:(a1 *B) *h.:(b1 * B); then consider x being object such that A64: x in the carrier of G and A65: x in (a1*B)*(b1*B) and A66: z=h.x by A63,FUNCT_2:64; reconsider x as Element of G by A64; consider z1,z2 being Element of G such that A67: x=z1 *z2 and A68: z1 in(a1*B) and A69: z2 in (b1*B) by A65; A70: h.z2 in y2 by A69,FUNCT_2:35; then reconsider z22=h.z2 as Element of G1; A71: h.z1 in x2 by A68,FUNCT_2:35; then reconsider z11=h.z1 as Element of G1; z=h.z1 * h.z2 by A66,A67,GROUP_6:def 6 .=z11 *z22 by GROUP_2:43; hence z in x2* y2 by A71,A70; end; then h.:(a1 *B) *h.:(b1 * B) c= x2 * y2; then A72: x2*y2 =h.:(a1*B)* h.:(b1*B) by A31,XBOOLE_0:def 10; y in the carrier of G1./.N; then A73: y in Cosets N by GROUP_6:17; then reconsider y1=y as Subset of G1; thus x*y=(CosOp N).(x,y) by GROUP_6:18 .=y1*x1 by A23,A73,A21,A22,A27,A25,A63,A72,A53,A62,A32,GROUP_6:def 3 .=(CosOp N).(y,x) by A23,A73,GROUP_6:def 3 .=y *x by GROUP_6:18; end; hence thesis by GROUP_1:def 12; end; B is strict normal Subgroup of A by A4,A9,A11,A12,A15,A17; hence thesis by A16,A18,A19,Th15; end; take z; A74: len z= len F by A8,FINSEQ_1:def 3; z.1=(Omega).(Image h) & z.(len z)=(1).(Image h) proof ex A being strict Subgroup of G st A=F.1 & z.1=h.:(A) by A8,A5; hence z.1=(Omega).(Image h) by A2,Th11; ex B being strict Subgroup of G st B=F.(len F) & z.(len F )=h.:(B) by A1,A8 ,FINSEQ_1:3; hence z.(len z)=(1).H by A3,A74,Th11 .=(1).(Image h) by GROUP_2:63; end; hence thesis by A1,A8,A10,FINSEQ_1:def 3; end;