let G be strict commutative Group; 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 ;
( 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
;
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 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;
( 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) )
;
( 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
by A2, A4, A7, A9, A8, GROUP_6:71, GROUP_6: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;
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 ) )
;
verum
end;
hence
G is solvable
by A3, A2, A4; verum