let G be strict solvable Group; for H being strict Subgroup of G holds H is solvable
let H be strict Subgroup of G; 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]
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 ;
( 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
;
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;
( 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)
;
( 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;
( N = H2 implies H1 ./. N is commutative )
assume
N = H2
;
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 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);
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
;
verum end;
then
the
multF of
(H1 ./. N) is
commutative
by BINOP_1:def 2;
hence
H1 ./. N is
commutative
by GROUP_3:2;
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;
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
take
R
; GRSOLV_1:def 1 ( 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
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; verum