let G be Group; ( ex F being FinSequence of the_normal_subgroups_of 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 normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G ./. G2 is cyclic Group ) ) ) implies G is nilpotent )
given F being FinSequence of the_normal_subgroups_of G such that A1:
( len F > 0 & F . 1 = (Omega). G & F . (len F) = (1). G )
and
A2:
for i being Element of NAT st i in dom F & i + 1 in dom F holds
for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G ./. G2 is cyclic Group )
; G is nilpotent
A3:
for i being Element of NAT st i in dom F & i + 1 in dom F holds
for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
proof
let i be
Element of
NAT ;
( i in dom F & i + 1 in dom F implies for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) )
assume A4:
(
i in dom F &
i + 1
in dom F )
;
for H1, H2 being strict normal Subgroup of G st H1 = F . i & H2 = F . (i + 1) holds
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
let H1,
H2 be
strict normal Subgroup of
G;
( H1 = F . i & H2 = F . (i + 1) implies ( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) ) )
assume A5:
(
H1 = F . i &
H2 = F . (i + 1) )
;
( H2 is strict Subgroup of H1 & H1 ./. ((H1,H2) `*`) is Subgroup of center (G ./. H2) )
then
H2 is
strict Subgroup of
H1
by A2, A4;
then A6:
H1 ./. ((H1,H2) `*`) is
Subgroup of
G ./. H2
by GROUP_6:28;
G ./. H2 is
commutative Group
by A2, A4, A5;
hence
(
H2 is
strict Subgroup of
H1 &
H1 ./. ((H1,H2) `*`) is
Subgroup of
center (G ./. H2) )
by A2, A4, A5, A6, GROUP_5:82;
verum
end;
take
F
; GRNILP_1:def 2 ( 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 normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) )
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 normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) ) )
by A1, A3; verum