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 & 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 Def1;
defpred S₁[ set , set ] means ex J being strict Subgroup of G st
( J = F . $1 & $2 = h .: J );
A2: for k being Nat st k in Seg (len F) holds
ex x being Element of Subgroups (Image h) st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len F) implies ex x being Element of Subgroups (Image h) st S₁[k,x] )
assume k in Seg (len F) ; :: thesis: ex x being Element of Subgroups (Image h) st S₁[k,x]
then k in dom F by FINSEQ_1:def 3;
then F . k in Subgroups G by FINSEQ_2:13;
then F . k is strict Subgroup of G by GROUP_3:def 1;
then consider A being strict Subgroup of G such that
A3: A = F . k ;
h .: A is strict Subgroup of Image h by Th10;
then h .: A in Subgroups (Image h) by GROUP_3:def 1;
then consider x being Element of Subgroups (Image h) such that
A4: x = h .: A ;
thus ex x being Element of Subgroups (Image h) st S₁[k,x] by A3, A4; :: thesis: verum

end;

consider z being FinSequence of Subgroups (Image h) such that
A5: ( dom z = Seg (len F) & ( for j being Nat st j in Seg (len F) holds
S₁[j,z . j] ) ) from FINSEQ_1:sch 5(A2);
A6: Seg (len z) = Seg (len F) by A5, FINSEQ_1:def 3;
A7: len z = len F by A5, FINSEQ_1:def 3;
A8: dom F = Seg (len z) by A6, FINSEQ_1:def 3
.= dom z by FINSEQ_1:def 3 ;
( 1 <= 1 & 1 <= len F ) by A1, NAT_1:14;
then A9: 1 in Seg (len F) by FINSEQ_1:3;
A10: ( z . 1 = (Omega). (Image h) & z . (len z) = (1). (Image h) )

proof

consider A being strict Subgroup of G such that
A11: ( A = F . 1 & z . 1 = h .: A ) by A5, A9;
thus z . 1 = (Omega). (Image h) by A1, A11, Th12; :: thesis: z . (len z) = (1). (Image h)
len F in Seg (len F) by A1, FINSEQ_1:5;
then consider B being strict Subgroup of G such that
A12: ( B = F . (len F) & z . (len F) = h .: B ) by A5;
thus z . (len z) = (1). H by A1, A7, A12, Th12
.= (1). (Image h) by GROUP_2:75 ; :: thesis: verum

end;

A13: 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 A14: ( i in dom z & 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 A15: ( G1 = z . i & 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 ) )
then consider A being strict Subgroup of G such that
A16: ( A = F . i & G1 = h .: A ) by A5, A14;
consider B being strict Subgroup of G such that
A17: ( B = F . (i + 1) & G2 = h .: B ) by A5, A14, A15;
A18: B is strict normal Subgroup of A by A1, A8, A14, A16, A17;
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 A19: N = G2 ; :: thesis: G1 ./. N is commutative

now

let x, y be Element of (G1 ./. N); :: thesis: x * y = y * x
A20: ( x in G1 ./. N & y in G1 ./. N ) by STRUCT_0:def 5;
( x in the carrier of (G1 ./. N) & y in the carrier of (G1 ./. N) ) ;
then A21: ( x in Cosets N & y in Cosets N ) by GROUP_6:22;
consider a being Element of G1 such that
A22: ( x = a * N & x = N * a ) by A20, GROUP_6:28;
consider b being Element of G1 such that
A23: ( y = b * N & y = N * b ) by A20, GROUP_6:28;
reconsider x1 = x as Subset of G1 by A21;
reconsider y1 = y as Subset of G1 by A21;
A24: ( a in h .: A & b in h .: A ) by A16, STRUCT_0:def 5;
then consider a1 being Element of A such that
A25: a = (h | A) . a1 by GROUP_6:54;
consider b1 being Element of A such that
A26: b = (h | A) . b1 by A24, GROUP_6:54;
reconsider a1 = a1 as Element of G by GROUP_2:51;
reconsider b1 = b1 as Element of G by GROUP_2:51;
A27: a = h . a1 by A25, FUNCT_1:72;
A28: b = h . b1 by A26, FUNCT_1:72;
A29: a * N = (h . a1) * (h .: B) by A17, A19, A27, GROUP_6:2
.= h .: (a1 * B) by Th14 ;
A30: b * N = (h . b1) * (h .: B) by A17, A19, A28, GROUP_6:2
.= h .: (b1 * B) by Th14 ;
reconsider x2 = h .: (a1 * B) as Subset of G1 by A29;
reconsider y2 = h .: (b1 * B) as Subset of G1 by A30;
A31: (h .: (a1 * B)) * (h .: (b1 * B)) = h .: ((a1 * B) * (b1 * B)) by Th15;
A32: x2 * y2 = (h .: (a1 * B)) * (h .: (b1 * B))

proof

now

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
A33: ( z = z1 * z2 & z1 in x2 & z2 in y2 ) ;
reconsider z11 = z1 as Element of H by A33;
reconsider z22 = z2 as Element of H by A33;
z = z11 * z22 by A33, GROUP_2:52;
hence z in (h .: (a1 * B)) * (h .: (b1 * B)) by A33; :: thesis: verum

end;

then A34: x2 * y2 c= (h .: (a1 * B)) * (h .: (b1 * B)) by TARSKI:def 3;

now

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
A35: ( x in the carrier of G & x in (a1 * B) * (b1 * B) & z = h . x ) by A31, FUNCT_2:115;
reconsider x = x as Element of G by A35;
consider z1, z2 being Element of G such that
A36: ( x = z1 * z2 & z1 in a1 * B & z2 in b1 * B ) by A35;
A37: ( h . z1 in x2 & h . z2 in y2 ) by A36, FUNCT_2:43;
then reconsider z11 = h . z1 as Element of G1 ;
reconsider z22 = h . z2 as Element of G1 by A37;
z = (h . z1) * (h . z2) by A35, A36, GROUP_6:def 7
.= z11 * z22 by GROUP_2:52 ;
hence z in x2 * y2 by A37; :: thesis: verum

end;

then (h .: (a1 * B)) * (h .: (b1 * B)) c= x2 * y2 by TARSKI:def 3;
hence x2 * y2 = (h .: (a1 * B)) * (h .: (b1 * B)) by A34, XBOOLE_0:def 10; :: thesis: verum

end;

A38: (h .: (b1 * B)) * (h .: (a1 * B)) = h .: ((b1 * B) * (a1 * B)) by Th15;
A39: y2 * x2 = (h .: (b1 * B)) * (h .: (a1 * B))

proof

now

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
A40: ( z = z1 * z2 & z1 in y2 & z2 in x2 ) ;
reconsider z11 = z1 as Element of H by A40;
reconsider z22 = z2 as Element of H by A40;
z = z11 * z22 by A40, GROUP_2:52;
hence z in (h .: (b1 * B)) * (h .: (a1 * B)) by A40; :: thesis: verum

end;

then A41: y2 * x2 c= (h .: (b1 * B)) * (h .: (a1 * B)) by TARSKI:def 3;

now

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
A42: ( x in the carrier of G & x in (b1 * B) * (a1 * B) & z = h . x ) by A38, FUNCT_2:115;
reconsider x = x as Element of G by A42;
consider z1, z2 being Element of G such that
A43: ( x = z1 * z2 & z1 in b1 * B & z2 in a1 * B ) by A42;
A44: ( h . z1 in y2 & h . z2 in x2 ) by A43, FUNCT_2:43;
then reconsider z11 = h . z1 as Element of G1 ;
reconsider z22 = h . z2 as Element of G1 by A44;
z = (h . z1) * (h . z2) by A42, A43, GROUP_6:def 7
.= z11 * z22 by GROUP_2:52 ;
hence z in y2 * x2 by A44; :: thesis: verum

end;

then (h .: (b1 * B)) * (h .: (a1 * B)) c= y2 * x2 by TARSKI:def 3;
hence y2 * x2 = (h .: (b1 * B)) * (h .: (a1 * B)) by A41, XBOOLE_0:def 10; :: thesis: verum

end;

A45: (a1 * B) * (b1 * B) = (b1 * B) * (a1 * B)

proof

reconsider K = B as normal Subgroup of A by A1, A8, A14, A16, A17;
reconsider a2 = a1, b2 = b1 as Element of A ;
A46: A ./. K is commutative Group by A1, A8, A14, A16, A17;
A47: 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 A46, 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;

A48: ( a1 * B = a2 * K & b1 * B = b2 * K ) by GROUP_6:2;
A49: a2 * K is Element of (A ./. K) by GROUP_6:27;
A50: b2 * K is Element of (A ./. K) by GROUP_6:27;
reconsider a12 = a1 * B, b12 = b1 * B as Element of Cosets K by A48, GROUP_6:16;
reconsider a11 = a12 as Element of (A ./. K) by A49, GROUP_6:2;
reconsider b11 = b12 as Element of (A ./. K) by A50, GROUP_6:2;
reconsider A1 = a1 * B as Subset of A by A48;
reconsider B1 = b1 * B as Subset of A by A48;
A51: A1 * B1 = (CosOp K) . a11,b11 by GROUP_6:def 4
.= the multF of (A ./. K) . a12,b12 by GROUP_6:23
.= the multF of (A ./. K) . b11,a11 by A47
.= (CosOp K) . b12,a12 by GROUP_6:23
.= B1 * A1 by GROUP_6:def 4 ;
A52: (a1 * B) * (b1 * B) = A1 * B1

proof

now

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
A53: ( x = z1 * z2 & z1 in a1 * B & z2 in b1 * B ) ;
( z1 in A1 & z2 in B1 ) by A53;
then reconsider z11 = z1, z22 = z2 as Element of A ;
z1 * z2 = z11 * z22 by GROUP_2:52;
hence x in A1 * B1 by A53; :: thesis: verum

end;

then A54: (a1 * B) * (b1 * B) c= A1 * B1 by TARSKI:def 3;

now

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
A55: ( x = z1 * z2 & z1 in A1 & z2 in B1 ) ;
reconsider z11 = z1, z22 = z2 as Element of G by A55;
z1 * z2 = z11 * z22 by GROUP_2:52;
hence x in (a1 * B) * (b1 * B) by A55; :: thesis: verum

end;

then A1 * B1 c= (a1 * B) * (b1 * B) by TARSKI:def 3;
hence (a1 * B) * (b1 * B) = A1 * B1 by A54, XBOOLE_0:def 10; :: thesis: verum

end;

(b1 * B) * (a1 * B) = B1 * A1

proof

now

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
A56: ( x = z1 * z2 & z1 in b1 * B & z2 in a1 * B ) ;
( z1 in B1 & z2 in A1 ) by A56;
then reconsider z11 = z1, z22 = z2 as Element of A ;
z1 * z2 = z11 * z22 by GROUP_2:52;
hence x in B1 * A1 by A56; :: thesis: verum

end;

then A57: (b1 * B) * (a1 * B) c= B1 * A1 by TARSKI:def 3;

now

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
A58: ( x = z1 * z2 & z1 in B1 & z2 in A1 ) ;
reconsider z11 = z1, z22 = z2 as Element of G by A58;
z1 * z2 = z11 * z22 by GROUP_2:52;
hence x in (b1 * B) * (a1 * B) by A58; :: thesis: verum

end;

then B1 * A1 c= (b1 * B) * (a1 * B) by TARSKI:def 3;
hence (b1 * B) * (a1 * B) = B1 * A1 by A57, XBOOLE_0:def 10; :: thesis: verum

end;

hence (a1 * B) * (b1 * B) = (b1 * B) * (a1 * B) by A51, A52; :: thesis: verum

end;

thus x * y = (CosOp N) . x,y by GROUP_6:23
.= y1 * x1 by A21, A22, A23, A29, A30, A31, A32, A38, A39, A45, GROUP_6:def 4
.= (CosOp N) . y,x by A21, GROUP_6:def 4
.= y * x by GROUP_6:23 ; :: thesis: verum

end;

hence G1 ./. N is commutative by GROUP_1:def 16; :: 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 A16, A17, A18, Th16; :: 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 ) ) ) )
thus ( 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, A5, A10, A13, FINSEQ_1:def 3; :: thesis: verum