:: GRSOLV_1 semantic presentation

begin

definition
let IT be Group;
attrIT is solvable  means :Def1: :: GRSOLV_1:def 1
 ex F being FinSequence of Subgroups 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 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;

:: deftheorem Def1 defines solvable GRSOLV_1:def_1_:_
 for IT being Group holds
( IT is solvable iff ex F being FinSequence of Subgroups 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 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 ) ) ) ) );

registration
cluster non empty strict Group-like associative solvable for multMagma ;
existence
 ex b1 being Group st
( b1 is solvable & b1 is strict )
proof
set G = the Group;
take H = (1). the Group; ::_thesis: ( H is solvable & H is strict )
thus  H is solvable ::_thesis: H is strict
proof
 rng <*H*> c= Subgroups H
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng <*H*> or x in Subgroups H )
A1: rng <*H*> = {H} by FINSEQ_1:39;
assume  x in rng <*H*> ; ::_thesis: x in Subgroups H
then  x = H by A1, TARSKI:def_1;
then  x is strict Subgroup of H by GROUP_2:54;
hence  x in Subgroups H by GROUP_3:def_1; ::_thesis: verum
end;
then reconsider F = <*H*> as FinSequence of Subgroups H by FINSEQ_1:def_4;
take  F ; :: according to GRSOLV_1:def_1 ::_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 Subgroup of H 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 ) ) ) )
A2: len F = 1 by FINSEQ_1:39;
A3: for i being Element of NAT st i in dom F & i + 1 in dom F holds
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 be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies 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 ) ) )
assume that
A4: i in dom F and
A5: i + 1 in dom F ; ::_thesis: 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 ) )
let G1, G2 be Subgroup of H; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) )
assume that
 G1 = F . i and
 G2 = F . (i + 1) ; ::_thesis: ( G2 is normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )
A6: dom F = {1} by A2, FINSEQ_1:2, FINSEQ_1:def_3;
then  i = 1 by A4, TARSKI:def_1;
hence  ( G2 is normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) by A5, A6, TARSKI:def_1; ::_thesis: verum
end;
F . (len F) = H by A2, FINSEQ_1:40
.= (1). H by GROUP_2:63 ;
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 Subgroup of H 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 A2, A3, FINSEQ_1:40; ::_thesis: verum
end;
thus  H is strict ; ::_thesis: verum
end;
end;

theorem Th1: :: GRSOLV_1:1
for G being strict Group
for 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 strict Group; ::_thesis: for H, F1, F2 being strict Subgroup of G st F1 is normal Subgroup of F2 holds
F1 /\ H is normal Subgroup of F2 /\ H
let H, F1, F2 be strict 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;

theorem :: GRSOLV_1:2
for G being strict Group
for F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1
proof
let G be strict Group; ::_thesis: for F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1
let F2 be strict Subgroup of G; ::_thesis: for F1 being strict normal Subgroup of F2
for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1
let F1 be strict normal Subgroup of F2; ::_thesis: for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1
let a, b be Element of F2; ::_thesis: (a * F1) * (b * F1) = (a * b) * F1
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 ; ::_thesis: verum
end;

theorem :: GRSOLV_1:3
for G being strict Group
for H, F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
proof
let G be strict Group; ::_thesis: for H, F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
let H, F2 be strict Subgroup of G; ::_thesis: for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
let F1 be strict normal Subgroup of F2; ::_thesis: for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
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 = 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); ::_thesis: f . (a * b) = (f . a) * (f . b)
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  f . (a * b) = (f . a) * (f . b) by A1, A7, A5, A6, GROUP_6:def_6; ::_thesis: verum
end;
then reconsider f = 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 being Element of G holds
( g in L iff g in H /\ F1 )
proof
let x be Element of G; ::_thesis: ( x in L iff x in H /\ F1 )
thus  ( x in L implies x in H /\ F1 ) ::_thesis: ( x in H /\ F1 implies x in L )
proof
assume A10: x in L ; ::_thesis: x in H /\ F1
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  x in H /\ F1 by A13, GROUP_2:82; ::_thesis: verum
end;
thus  ( x in H /\ F1 implies x in L ) ::_thesis: verum
proof
reconsider F19 = F1 as strict 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 ; ::_thesis: x in L
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  x in L by GROUP_6:41; ::_thesis: verum
end;
end;
hence  Ker f = H /\ F1 by GROUP_2:def_6; ::_thesis: verum
end;
reconsider G1 = Ker f as strict normal Subgroup of G2 ;
 G2 ./. G1, Image f are_isomorphic by GROUP_6:78;
hence  for G2 being strict Subgroup of G st G2 = H /\ F2 holds
for G1 being normal Subgroup of G2 st G1 = H /\ F1 holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic by A9; ::_thesis: verum
end;

theorem Th4: :: GRSOLV_1:4
for G being strict Group
for H, F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = F2 /\ H holds
for G1 being normal Subgroup of G2 st G1 = F1 /\ H holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
proof
let G be strict Group; ::_thesis: for H, F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = F2 /\ H holds
for G1 being normal Subgroup of G2 st G1 = F1 /\ H holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
let H, F2 be strict Subgroup of G; ::_thesis: for F1 being strict normal Subgroup of F2
for G2 being strict Subgroup of G st G2 = F2 /\ H holds
for G1 being normal Subgroup of G2 st G1 = F1 /\ H holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
let F1 be strict normal Subgroup of F2; ::_thesis: for G2 being strict Subgroup of G st G2 = F2 /\ H holds
for G1 being normal Subgroup of G2 st G1 = F1 /\ H holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic
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 = 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); ::_thesis: f . (a * b) = (f . a) * (f . b)
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  f . (a * b) = (f . a) * (f . b) by A1, A7, A5, A6, GROUP_6:def_6; ::_thesis: verum
end;
then reconsider f = 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 being Element of G holds
( g in L iff g in F1 /\ H )
proof
let x be Element of G; ::_thesis: ( x in L iff x in F1 /\ H )
thus  ( x in L implies x in F1 /\ H ) ::_thesis: ( x in F1 /\ H implies x in L )
proof
assume A10: x in L ; ::_thesis: x in F1 /\ H
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  x in F1 /\ H by A13, GROUP_2:82; ::_thesis: verum
end;
thus  ( x in F1 /\ H implies x in L ) ::_thesis: verum
proof
reconsider F19 = F1 as strict 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 ; ::_thesis: x in L
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  x in L by GROUP_6:41; ::_thesis: verum
end;
end;
hence  Ker f = F1 /\ H by GROUP_2:def_6; ::_thesis: verum
end;
reconsider G1 = Ker f as strict normal Subgroup of G2 ;
 G2 ./. G1, Image f are_isomorphic by GROUP_6:78;
hence  for G2 being strict Subgroup of G st G2 = F2 /\ H holds
for G1 being normal Subgroup of G2 st G1 = F1 /\ H holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic by A9; ::_thesis: verum
end;

theorem :: GRSOLV_1:5
for G being strict solvable Group
for H being strict Subgroup of G holds H is solvable
proof
let G be strict solvable Group; ::_thesis: for H being strict Subgroup of G holds H is solvable
let H be strict Subgroup of G; ::_thesis: H is solvable
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 being Element of NAT st i in dom F & i + 1 in dom F holds
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 S1[ set , set ] means  ex I being strict Subgroup of G st
( I = F . $1 & $2 = I /\ H );
A5: for k being Nat st k in Seg (len F) holds
ex x being Element of Subgroups H st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of Subgroups H st S1[k,x] )
assume  k in Seg (len F) ; ::_thesis: ex x being Element of Subgroups H st S1[k,x]
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 ; ::_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 Subgroups H such that
A6: ( 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(A5);
A7: for i being Element of NAT st i in dom R & i + 1 in dom R holds
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 be Element of NAT ; ::_thesis: ( i in dom R & i + 1 in dom R implies 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 ) ) )
assume that
A8: i in dom R and
A9: i + 1 in dom R ; ::_thesis: 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 ) )
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; ::_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 that
A14: H1 = R . i and
A15: 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 ) )
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; ::_thesis: ( N = H2 implies H1 ./. N is commutative )
assume  N = H2 ; ::_thesis: H1 ./. N is commutative
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__::_thesis:_for_a,_b_being_Element_of_(H1_./._N)_holds_the_multF_of_(H1_./._N)_._(a,b)_=_the_multF_of_(H1_./._N)_._(b,a)
let a, b be Element of (H1 ./. N); ::_thesis: the multF of (H1 ./. N) . (a,b) = the multF of (H1 ./. N) . (b,a)
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 ; ::_thesis: verum
end;
then  the multF of (H1 ./. N) is commutative by BINOP_1:def_2;
hence  H1 ./. N is commutative by GROUP_3:2; ::_thesis: verum
end;
 H2 = J1 /\ H by A15, A11;
hence  ( H2 is strict normal Subgroup of H1 & ( for N being normal Subgroup of H1 st N = H2 holds
H1 ./. N is commutative ) ) by A14, A13, A17, Th1; ::_thesis: verum
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  R . 1 = (Omega). H by A2, GROUP_2:86; ::_thesis: verum
end;
take  R ; :: according to GRSOLV_1:def_1 ::_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 Subgroup of H st G1 = R . i & G2 = R . (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 ) ) ) )
 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 ;
::_thesis: verum
end;
hence  ( 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 Subgroup of H st G1 = R . i & G2 = R . (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 A1, A6, A27, A7, FINSEQ_1:def_3; ::_thesis: verum
end;

theorem :: GRSOLV_1:6
for G being strict Group st ex F being FinSequence of Subgroups 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 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 strict Group; ::_thesis: ( ex F being FinSequence of Subgroups 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 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 ) ) ) ) implies G is solvable )
given F being FinSequence of Subgroups 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 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 ) ) ) ) ; ::_thesis: G is solvable
take  F ; :: according to GRSOLV_1:def_1 ::_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 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 ) ) ) )
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 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 A1; ::_thesis: verum
end;

theorem :: GRSOLV_1:7
for G being strict commutative Group holds G is solvable
proof
let G be strict commutative Group; ::_thesis: G is solvable
 ( (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 being Element of NAT st i in dom F & i + 1 in dom F holds
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 be Element of NAT ; ::_thesis: ( i in dom F & i + 1 in dom F implies 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 ) ) )
assume that
A5: i in dom F and
A6: i + 1 in dom F ; ::_thesis: 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 ) )
now__::_thesis:_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_)_)
let G1, G2 be strict Subgroup of G; ::_thesis: ( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) )
assume A7: ( G1 = F . i & G2 = F . (i + 1) ) ; ::_thesis: ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )
 dom F = {1,2} by A3, FINSEQ_1:2, FINSEQ_1: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, FINSEQ_1:def_3;
 for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative
proof
let N be normal Subgroup of G1; ::_thesis: ( N = G2 implies G1 ./. N is commutative )
assume  N = G2 ; ::_thesis: G1 ./. N is commutative
then  G1,G1 ./. N are_isomorphic by A2, A4, A7, A9, A8, GROUP_6:71, TARSKI:def_2;
hence  G1 ./. N is commutative by GROUP_6:77; ::_thesis: verum
end;
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; ::_thesis: verum
end;
hence  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 ) ) ; ::_thesis: verum
end;
hence  G is solvable by A3, A2, A4, Def1; ::_thesis: verum
end;

definition
let G, H be Group;
let g be Homomorphism of G,H;
let A be Subgroup of G;
funcg | A ->  Homomorphism of A,H equals :: GRSOLV_1:def 2
g | the carrier of A;
coherence
 g | the carrier of A is Homomorphism of A,H
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__::_thesis:_for_a,_b_being_Element_of_A_holds_(f_._a)_*_(f_._b)_=_f_._(a_*_b)
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; ::_thesis: the multF of H . ((g . a),(g . b)) = g . ( the multF of G . (a,b))
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)) ; ::_thesis: verum
end;
let a, b be Element of A; ::_thesis: (f . a) * (f . b) = f . (a * b)
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, TARSKI:def_3;
reconsider a9 = a as Element of G by A1, TARSKI:def_3;
thus  the multF of G . (a,b) = a9 * b9
.= a * b by GROUP_2:43 ; ::_thesis: verum
end;
 ( a is Element of G & b is Element of G ) by A1, TARSKI:def_3;
hence (f . a) * (f . b) = g . ( the multF of G . (a,b)) by A3, A2
.= f . (a * b) by A4, FUNCT_1:49 ;
::_thesis: verum
end;
hence  g | the carrier of A is Homomorphism of A,H by GROUP_6:def_6; ::_thesis: verum
end;
end;

:: deftheorem  defines | GRSOLV_1:def_2_:_
 for G, H being Group
for g being Homomorphism of G,H
for A being Subgroup of G holds g | A = g | the carrier of A;

definition
let G, H be strict Group;
let g be Homomorphism of G,H;
let A be Subgroup of G;
funcg .: A ->  strict Subgroup of H equals :: GRSOLV_1:def 3
 Image (g | A);
coherence
 Image (g | A) is strict Subgroup of H ;
end;

:: deftheorem  defines .: GRSOLV_1:def_3_:_
 for G, H being strict Group
for g being Homomorphism of G,H
for A being Subgroup of G holds g .: A = Image (g | A);

theorem Th8: :: GRSOLV_1:8
for G, H being strict Group
for g being Homomorphism of G,H
for A being strict Subgroup of G holds the carrier of (g .: A) = g .: the carrier of A
proof
let G, H be strict Group; ::_thesis: for g being Homomorphism of G,H
for A being strict Subgroup of G holds the carrier of (g .: A) = g .: the carrier of A
let g be Homomorphism of G,H; ::_thesis: for A being strict Subgroup of G holds the carrier of (g .: A) = g .: the carrier of A
let A be strict Subgroup of G; ::_thesis: the carrier of (g .: A) = g .: the carrier of A
thus  the carrier of (g .: A) = rng (g | A) by GROUP_6:44
.= g .: the carrier of A by RELAT_1:115 ; ::_thesis: verum
end;

theorem Th9: :: GRSOLV_1:9
for G, H being strict Group
for h being Homomorphism of G,H
for A being strict Subgroup of G holds Image (h | A) is strict Subgroup of Image h
proof
let G, H be strict Group; ::_thesis: for h being Homomorphism of G,H
for A being strict Subgroup of G holds Image (h | A) is strict Subgroup of Image h
let h be Homomorphism of G,H; ::_thesis: for A being strict Subgroup of G holds Image (h | A) is strict Subgroup of Image h
let A be strict Subgroup of G; ::_thesis: Image (h | A) is strict Subgroup of Image h
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  Image (h | A) is strict Subgroup of Image h by A1, GROUP_2:57, RELAT_1:123; ::_thesis: verum
end;

theorem :: GRSOLV_1:10
for G, H being strict Group
for h being Homomorphism of G,H
for A being strict Subgroup of G holds h .: A is strict Subgroup of Image h by Th9;

theorem Th11: :: GRSOLV_1:11
for G, H being strict Group
for h being Homomorphism of G,H holds
( h .: ((1). G) = (1). H & h .: ((Omega). G) = (Omega). (Image h) )
proof
let G, H be strict Group; ::_thesis: for h being Homomorphism of G,H holds
( h .: ((1). G) = (1). H & h .: ((Omega). G) = (Omega). (Image h) )
let h be Homomorphism of G,H; ::_thesis: ( h .: ((1). G) = (1). H & h .: ((Omega). G) = (Omega). (Image 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; ::_thesis: h .: ((Omega). G) = (Omega). (Image h)
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  h .: ((Omega). G) = (Omega). (Image h) by GROUP_2:59; ::_thesis: verum
end;

theorem Th12: :: GRSOLV_1:12
for G, H being strict Group
for h being Homomorphism of G,H
for A, B being strict Subgroup of G st A is Subgroup of B holds
h .: A is Subgroup of h .: B
proof
let G, H be strict Group; ::_thesis: for h being Homomorphism of G,H
for A, B being strict Subgroup of G st A is Subgroup of B holds
h .: A is Subgroup of h .: B
let h be Homomorphism of G,H; ::_thesis: for A, B being strict Subgroup of G st A is Subgroup of B holds
h .: A is Subgroup of h .: B
let A, B be strict Subgroup of G; ::_thesis: ( A is Subgroup of B implies h .: A is Subgroup of h .: B )
assume  A is Subgroup of B ; ::_thesis: h .: A is Subgroup of h .: 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  h .: A is Subgroup of h .: B by GROUP_2:57; ::_thesis: verum
end;

theorem Th13: :: GRSOLV_1:13
for G, H being strict Group
for 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; ::_thesis: for 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) )
let h be Homomorphism of G,H; ::_thesis: 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) )
let A be strict Subgroup of G; ::_thesis: for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
let a be Element of G; ::_thesis: ( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )
now__::_thesis:_for_x_being_set_st_x_in_h_.:_(a_*_A)_holds_
x_in_(h_._a)_*_(h_.:_A)
let x be set ; ::_thesis: ( x in h .: (a * A) implies x in (h . a) * (h .: A) )
assume  x in h .: (a * A) ; ::_thesis: x in (h . a) * (h .: A)
then consider y being set  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 = 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; ::_thesis: verum
end;
then A7: h .: (a * A) c= (h . a) * (h .: A) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_(h_._a)_*_(h_.:_A)_holds_
x_in_h_.:_(a_*_A)
let x be set ; ::_thesis: ( x in (h . a) * (h .: A) implies x in h .: (a * A) )
assume  x in (h . a) * (h .: A) ; ::_thesis: x in h .: (a * 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 = 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; ::_thesis: verum
end;
then  (h . a) * (h .: A) c= h .: (a * A) by TARSKI:def_3;
hence  (h . a) * (h .: A) = h .: (a * A) by A7, XBOOLE_0:def_10; ::_thesis: (h .: A) * (h . a) = h .: (A * a)
now__::_thesis:_for_x_being_set_st_x_in_h_.:_(A_*_a)_holds_
x_in_(h_.:_A)_*_(h_._a)
let x be set ; ::_thesis: ( x in h .: (A * a) implies x in (h .: A) * (h . a) )
assume  x in h .: (A * a) ; ::_thesis: x in (h .: A) * (h . a)
then consider y being set  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 = 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; ::_thesis: verum
end;
then A19: h .: (A * a) c= (h .: A) * (h . a) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_(h_.:_A)_*_(h_._a)_holds_
x_in_h_.:_(A_*_a)
let x be set ; ::_thesis: ( x in (h .: A) * (h . a) implies x in h .: (A * a) )
assume  x in (h .: A) * (h . a) ; ::_thesis: x in h .: (A * 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 = 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; ::_thesis: verum
end;
then  (h .: A) * (h . a) c= h .: (A * a) by TARSKI:def_3;
hence  (h .: A) * (h . a) = h .: (A * a) by A19, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th14: :: GRSOLV_1:14
for G, H being strict Group
for 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; ::_thesis: for h being Homomorphism of G,H
for A, B being Subset of G holds (h .: A) * (h .: B) = h .: (A * B)
let h be Homomorphism of G,H; ::_thesis: for A, B being Subset of G holds (h .: A) * (h .: B) = h .: (A * B)
let A, B be Subset of G; ::_thesis: (h .: A) * (h .: B) = h .: (A * B)
now__::_thesis:_for_z_being_set_st_z_in_(h_.:_A)_*_(h_.:_B)_holds_
z_in_h_.:_(A_*_B)
let z be set ; ::_thesis: ( z in (h .: A) * (h .: B) implies z in h .: (A * B) )
assume  z in (h .: A) * (h .: B) ; ::_thesis: z in h .: (A * 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 set  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 = z4 as Element of G by A4;
consider z3 being set  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 = 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; ::_thesis: verum
end;
then A11: (h .: A) * (h .: B) c= h .: (A * B) by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_h_.:_(A_*_B)_holds_
z_in_(h_.:_A)_*_(h_.:_B)
let z be set ; ::_thesis: ( z in h .: (A * B) implies z in (h .: A) * (h .: B) )
assume  z in h .: (A * B) ; ::_thesis: z in (h .: A) * (h .: B)
then consider x being set  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 = 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; ::_thesis: verum
end;
then  h .: (A * B) c= (h .: A) * (h .: B) by TARSKI:def_3;
hence  (h .: A) * (h .: B) = h .: (A * B) by A11, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th15: :: GRSOLV_1:15
for G, H being strict Group
for h being Homomorphism of G,H
for A, B being strict Subgroup of G st A is strict normal Subgroup of B holds
h .: A is strict normal Subgroup of h .: B
proof
let G, H be strict Group; ::_thesis: for h being Homomorphism of G,H
for A, B being strict Subgroup of G st A is strict normal Subgroup of B holds
h .: A is strict normal Subgroup of h .: B
let h be Homomorphism of G,H; ::_thesis: for A, B being strict Subgroup of G st A is strict normal Subgroup of B holds
h .: A is strict normal Subgroup of h .: B
let A, B be strict Subgroup of G; ::_thesis: ( A is strict normal Subgroup of B implies h .: A is strict normal Subgroup of h .: B )
assume  A is strict normal Subgroup of B ; ::_thesis: h .: A is strict normal Subgroup of h .: 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); ::_thesis: b2 * C c= C * b2
A1: b2 in h .: B by STRUCT_0:def_5;
now__::_thesis:_for_x_being_set_st_x_in_b2_*_C_holds_
x_in_C_*_b2
consider b1 being Element of B such that
A2: b2 = (h | B) . b1 by A1, GROUP_6:45;
reconsider b1 = 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 set ; ::_thesis: ( x in b2 * C implies x in C * b2 )
assume  x in b2 * C ; ::_thesis: x in C * b2
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 = 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; ::_thesis: verum
end;
hence  b2 * C c= C * b2 by TARSKI:def_3; ::_thesis: verum
end;
hence  h .: A is strict normal Subgroup of h .: B by GROUP_3:118; ::_thesis: verum
end;

theorem :: GRSOLV_1:16
for G, H being strict Group
for h being Homomorphism of G,H st G is solvable Group holds
Image h is solvable
proof
let G, H be strict Group; ::_thesis: for h being Homomorphism of G,H st G is solvable Group holds
Image h is solvable
let h be Homomorphism of G,H; ::_thesis: ( G is solvable Group implies Image h is solvable )
assume  G is solvable Group ; ::_thesis: Image h is solvable
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 being Element of NAT st i in dom F & i + 1 in dom F holds
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 S1[ set , set ] means  ex J being strict Subgroup of G st
( J = F . $1 & $2 = h .: J );
A6: for k being Nat st k in Seg (len F) holds
ex x being Element of Subgroups (Image h) st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of Subgroups (Image h) st S1[k,x] )
assume  k in Seg (len F) ; ::_thesis: ex x being Element of Subgroups (Image h) st S1[k,x]
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  ex x being Element of Subgroups (Image h) st S1[k,x] by A7; ::_thesis: verum
end;
consider z being FinSequence of Subgroups (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 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 be Element of NAT ; ::_thesis: ( i in dom z & i + 1 in dom z implies 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 ) ) )
assume that
A11: i in dom z and
A12: i + 1 in dom z ; ::_thesis: 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 ) )
let G1, G2 be strict Subgroup of Image h; ::_thesis: ( G1 = z . i & G2 = z . (i + 1) implies ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) )
assume that
A13: G1 = z . i and
A14: G2 = z . (i + 1) ; ::_thesis: ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) )
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; ::_thesis: ( N = G2 implies G1 ./. N is commutative )
assume A20: N = G2 ; ::_thesis: G1 ./. N is commutative
now__::_thesis:_for_x,_y_being_Element_of_(G1_./._N)_holds_x_*_y_=_y_*_x
let x, y be Element of (G1 ./. N); ::_thesis: x * y = y * x
 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 = 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 = 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__::_thesis:_for_z_being_set_st_z_in_x2_*_y2_holds_
z_in_(h_.:_(a1_*_B))_*_(h_.:_(b1_*_B))
let z be set ; ::_thesis: ( z in x2 * y2 implies z in (h .: (a1 * B)) * (h .: (b1 * B)) )
assume  z in x2 * y2 ; ::_thesis: z in (h .: (a1 * B)) * (h .: (b1 * B))
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; ::_thesis: verum
end;
then A31: x2 * y2 c= (h .: (a1 * B)) * (h .: (b1 * B)) by TARSKI:def_3;
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__::_thesis:_for_x_being_set_st_x_in_(a1_*_B)_*_(b1_*_B)_holds_
x_in_A1_*_B1
let x be set ; ::_thesis: ( x in (a1 * B) * (b1 * B) implies x in A1 * B1 )
assume  x in (a1 * B) * (b1 * B) ; ::_thesis: x in A1 * B1
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; ::_thesis: verum
end;
then A37: (a1 * B) * (b1 * B) c= A1 * B1 by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_(b1_*_B)_*_(a1_*_B)_holds_
x_in_B1_*_A1
let x be set ; ::_thesis: ( x in (b1 * B) * (a1 * B) implies x in B1 * A1 )
assume  x in (b1 * B) * (a1 * B) ; ::_thesis: x in B1 * A1
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; ::_thesis: verum
end;
then A40: (b1 * B) * (a1 * B) c= B1 * A1 by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_B1_*_A1_holds_
x_in_(b1_*_B)_*_(a1_*_B)
let x be set ; ::_thesis: ( x in B1 * A1 implies x in (b1 * B) * (a1 * B) )
assume  x in B1 * A1 ; ::_thesis: x in (b1 * B) * (a1 * B)
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; ::_thesis: verum
end;
then A43: B1 * A1 c= (b1 * B) * (a1 * B) by TARSKI:def_3;
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)
proof
let a, b be Element of (A ./. K); ::_thesis: the multF of (A ./. K) . (a,b) = the multF of (A ./. K) . (b,a)
 the multF of (A ./. K) is commutative by A44, GROUP_3:2;
hence  the multF of (A ./. K) . (a,b) = the multF of (A ./. K) . (b,a) by BINOP_1:def_2; ::_thesis: verum
end;
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__::_thesis:_for_x_being_set_st_x_in_A1_*_B1_holds_
x_in_(a1_*_B)_*_(b1_*_B)
let x be set ; ::_thesis: ( x in A1 * B1 implies x in (a1 * B) * (b1 * B) )
assume  x in A1 * B1 ; ::_thesis: x in (a1 * B) * (b1 * B)
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; ::_thesis: verum
end;
then  A1 * B1 c= (a1 * B) * (b1 * B) by TARSKI:def_3;
then  (a1 * B) * (b1 * B) = A1 * B1 by A37, XBOOLE_0:def_10;
hence  (a1 * B) * (b1 * B) = (b1 * B) * (a1 * B) by A46, A40, A43, XBOOLE_0:def_10; ::_thesis: verum
end;
now__::_thesis:_for_z_being_set_st_z_in_y2_*_x2_holds_
z_in_(h_.:_(b1_*_B))_*_(h_.:_(a1_*_B))
let z be set ; ::_thesis: ( z in y2 * x2 implies z in (h .: (b1 * B)) * (h .: (a1 * B)) )
assume  z in y2 * x2 ; ::_thesis: z in (h .: (b1 * B)) * (h .: (a1 * B))
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; ::_thesis: verum
end;
then A52: y2 * x2 c= (h .: (b1 * B)) * (h .: (a1 * B)) by TARSKI:def_3;
A53: (h .: (b1 * B)) * (h .: (a1 * B)) = h .: ((b1 * B) * (a1 * B)) by Th14;
now__::_thesis:_for_z_being_set_st_z_in_(h_.:_(b1_*_B))_*_(h_.:_(a1_*_B))_holds_
z_in_y2_*_x2
let z be set ; ::_thesis: ( z in (h .: (b1 * B)) * (h .: (a1 * B)) implies z in y2 * x2 )
assume  z in (h .: (b1 * B)) * (h .: (a1 * B)) ; ::_thesis: z in y2 * x2
then consider x being set  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 = 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; ::_thesis: verum
end;
then  (h .: (b1 * B)) * (h .: (a1 * B)) c= y2 * x2 by TARSKI:def_3;
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__::_thesis:_for_z_being_set_st_z_in_(h_.:_(a1_*_B))_*_(h_.:_(b1_*_B))_holds_
z_in_x2_*_y2
let z be set ; ::_thesis: ( z in (h .: (a1 * B)) * (h .: (b1 * B)) implies z in x2 * y2 )
assume  z in (h .: (a1 * B)) * (h .: (b1 * B)) ; ::_thesis: z in x2 * y2
then consider x being set  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 = 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; ::_thesis: verum
end;
then  (h .: (a1 * B)) * (h .: (b1 * B)) c= x2 * y2 by TARSKI:def_3;
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 ; ::_thesis: verum
end;
hence  G1 ./. N is commutative by GROUP_1:def_12; ::_thesis: verum
end;
 B is strict normal Subgroup of A by A4, A9, A11, A12, A15, A17;
hence  ( G2 is strict normal Subgroup of G1 & ( for N being normal Subgroup of G1 st N = G2 holds
G1 ./. N is commutative ) ) by A16, A18, A19, Th15; ::_thesis: verum
end;
take  z ; :: according to GRSOLV_1:def_1 ::_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 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 ) ) ) )
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; ::_thesis: z . (len z) = (1). (Image h)
 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 ;
::_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 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 ) ) ) ) by A1, A8, A10, FINSEQ_1:def_3; ::_thesis: verum
end;