let G be Group; ( G is nilpotent iff 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 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) )
A1:
now ( G is nilpotent implies 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 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) )assume
G is
nilpotent
;
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 & [.G1,((Omega). G).] is Subgroup of G2 ) ) )then consider R being
FinSequence of
the_normal_subgroups_of G such that A2:
(
len R > 0 &
R . 1
= (Omega). G &
R . (len R) = (1). G & ( for
i being
Element of
NAT st
i in dom R &
i + 1
in dom R holds
for
H1,
H2 being
strict normal Subgroup of
G st
H1 = R . i &
H2 = R . (i + 1) holds
(
H2 is
Subgroup of
H1 &
H1 ./. ((H1,H2) `*`) is
Subgroup of
center (G ./. H2) ) ) )
;
reconsider F =
R as
FinSequence of
the_normal_subgroups_of G ;
A3:
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
strict Subgroup of
G1 &
[.G1,((Omega). G).] is
strict Subgroup of
G2 )
proof
let i be
Element of
NAT ;
( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) )
assume A4:
(
i in dom F &
i + 1
in dom F )
;
for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 )
let G1,
G2 be
strict normal Subgroup of
G;
( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 ) )
assume A5:
(
G1 = F . i &
G2 = F . (i + 1) )
;
( G2 is strict Subgroup of G1 & [.G1,((Omega). G).] is strict Subgroup of G2 )
then A6:
(
G2 is
strict Subgroup of
G1 & ( for
N being
strict normal Subgroup of
G st
N = G2 &
N is
strict Subgroup of
G1 holds
G1 ./. ((G1,N) `*`) is
Subgroup of
center (G ./. N) ) )
by A2, A4;
[.G1,((Omega). G).] is
strict Subgroup of
G2
hence
(
G2 is
strict Subgroup of
G1 &
[.G1,((Omega). G).] is
strict Subgroup of
G2 )
by A2, A4, A5;
verum
end; take F =
F;
( 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,((Omega). G).] is Subgroup of 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,((Omega). G).] is
Subgroup of
G2 ) ) )
by A2, A3;
verum end;
now ( 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 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) implies ex F being FinSequence of the_normal_subgroups_of G st G is nilpotent )given F being
FinSequence of
the_normal_subgroups_of G such that A8:
(
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,((Omega). G).] is
Subgroup of
G2 ) ) )
;
ex F being FinSequence of the_normal_subgroups_of G st G is nilpotent A9:
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
strict Subgroup of
G1 &
G1 ./. ((G1,G2) `*`) is
Subgroup of
center (G ./. G2) )
proof
let i be
Element of
NAT ;
( i in dom F & i + 1 in dom F implies for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) )
assume A10:
(
i in dom F &
i + 1
in dom F )
;
for G1, G2 being strict normal Subgroup of G st G1 = F . i & G2 = F . (i + 1) holds
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) )
let G1,
G2 be
strict normal Subgroup of
G;
( G1 = F . i & G2 = F . (i + 1) implies ( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) ) )
assume A11:
(
G1 = F . i &
G2 = F . (i + 1) )
;
( G2 is strict Subgroup of G1 & G1 ./. ((G1,G2) `*`) is Subgroup of center (G ./. G2) )
then A12:
G2 is
strict Subgroup of
G1
by A8, A10;
[.G1,((Omega). G).] is
strict Subgroup of
G2
by A8, A10, A11;
hence
(
G2 is
strict Subgroup of
G1 &
G1 ./. ((G1,G2) `*`) is
Subgroup of
center (G ./. G2) )
by A12, Th20;
verum
end; take F =
F;
G is nilpotent
(
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 A8, A9;
hence
G is
nilpotent
;
verum end;
hence
( G is nilpotent iff 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 & [.G1,((Omega). G).] is Subgroup of G2 ) ) ) )
by A1; verum