let O be set ; for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 holds
ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
let G be GroupWithOperators of O; for s1, s2 being CompositionSeries of G st len s1 > 1 & s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 holds
ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
let s1, s2 be CompositionSeries of G; ( len s1 > 1 & s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 implies ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j ) )
assume
len s1 > 1
; ( not s2 <> s1 or not s2 is strictly_decreasing or not s2 is_finer_than s1 or ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j ) )
then
len s1 >= 1 + 1
by NAT_1:13;
then
Seg 2 c= Seg (len s1)
by FINSEQ_1:5;
then A1:
Seg 2 c= dom s1
by FINSEQ_1:def 3;
assume A2:
s2 <> s1
; ( not s2 is strictly_decreasing or not s2 is_finer_than s1 or ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j ) )
assume A3:
s2 is strictly_decreasing
; ( not s2 is_finer_than s1 or ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j ) )
assume A4:
s2 is_finer_than s1
; ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
then consider n being Nat such that
A5:
len s2 = (len s1) + n
by Th95;
n <> 0
by A2, A4, A5, Th96;
then A6:
0 + (len s1) < n + (len s1)
by XREAL_1:6;
then
Seg (len s1) c= Seg (len s2)
by A5, FINSEQ_1:5;
then
Seg (len s1) c= dom s2
by FINSEQ_1:def 3;
then A7:
dom s1 c= dom s2
by FINSEQ_1:def 3;
now ex i being Element of NAT st
( i in dom s1 & s1 . i = s2 . i & i + 1 in dom s1 & s1 . (i + 1) <> s2 . (i + 1) )set fX =
{ k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } ;
A8:
1
in Seg 2
;
(
s1 . 1
= (Omega). G &
s2 . 1
= (Omega). G )
by Def28;
then A9:
1
in { k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) }
by A1, A8;
then
{ k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } c= dom s1
;
then reconsider fX =
{ k where k is Element of NAT : ( k in dom s1 & s1 . k = s2 . k ) } as non
empty finite real-membered set by A9;
set i =
max fX;
max fX in fX
by XXREAL_2:def 8;
then A10:
ex
k being
Element of
NAT st
(
max fX = k &
k in dom s1 &
s1 . k = s2 . k )
;
then reconsider i =
max fX as
Element of
NAT ;
take i =
i;
( i in dom s1 & s1 . i = s2 . i & i + 1 in dom s1 & s1 . (i + 1) <> s2 . (i + 1) )thus
(
i in dom s1 &
s1 . i = s2 . i )
by A10;
( i + 1 in dom s1 & s1 . (i + 1) <> s2 . (i + 1) )A11:
now i + 1 in dom s1assume
not
i + 1
in dom s1
;
contradictionthen A12:
not
i + 1
in Seg (len s1)
by FINSEQ_1:def 3;
per cases
( 1 > i + 1 or i + 1 > len s1 )
by A12;
suppose A13:
i + 1
> len s1
;
contradiction
i in Seg (len s1)
by A10, FINSEQ_1:def 3;
then A14:
i <= len s1
by FINSEQ_1:1;
i >= len s1
by A13, NAT_1:13;
then A15:
i = len s1
by A14, XXREAL_0:1;
then
(
0 + 1
<= i + 1 &
i + 1
<= len s2 )
by A5, A6, NAT_1:13;
then
i + 1
in Seg (len s2)
;
then A16:
i + 1
in dom s2
by FINSEQ_1:def 3;
then reconsider H1 =
s2 . i,
H2 =
s2 . (i + 1) as
Element of
the_stable_subgroups_of G by A10, FINSEQ_2:11;
reconsider H1 =
H1,
H2 =
H2 as
StableSubgroup of
G by Def11;
A17:
s2 . i = (1). G
by A10, A15, Def28;
then A18:
the
carrier of
H1 = {(1_ G)}
by Def8;
reconsider H2 =
H2 as
normal StableSubgroup of
H1 by A7, A10, A16, Def28;
1_ G in H2
by Lm17;
then
1_ G in the
carrier of
H2
by STRUCT_0:def 5;
then A19:
{(1_ G)} c= the
carrier of
H2
by ZFMISC_1:31;
H2 is
Subgroup of
(1). G
by A17, Def7;
then
the
carrier of
H2 c= the
carrier of
((1). G)
by GROUP_2:def 5;
then
the
carrier of
H2 c= {(1_ G)}
by Def8;
then
the
carrier of
H2 = {(1_ G)}
by A19, XBOOLE_0:def 10;
then
H1 ./. H2 is
trivial
by A18, Th77;
hence
contradiction
by A3, A7, A10, A16;
verum end; end; end; hence
i + 1
in dom s1
;
s1 . (i + 1) <> s2 . (i + 1)hence
s1 . (i + 1) <> s2 . (i + 1)
;
verum end;
then consider i being Nat such that
A23:
i in dom s1
and
A24:
i + 1 in dom s1
and
A25:
s1 . i = s2 . i
and
A26:
s1 . (i + 1) <> s2 . (i + 1)
;
now ex j being Element of NAT st
( j in dom s2 & s1 . (i + 1) = s2 . j & i + 1 < j )consider x being
set such that A27:
x c= dom s2
and A28:
s1 = s2 * (Sgm x)
by A4;
set j =
(Sgm x) . (i + 1);
A29:
x c= Seg (len s2)
by A27, FINSEQ_1:def 3;
A30:
i + 1
in dom (Sgm x)
by A24, A28, FUNCT_1:11;
then
(Sgm x) . (i + 1) in rng (Sgm x)
by FUNCT_1:3;
then
(Sgm x) . (i + 1) in x
by A29, FINSEQ_1:def 13;
then A31:
(Sgm x) . (i + 1) in Seg (len s2)
by A29;
then reconsider j =
(Sgm x) . (i + 1) as
Element of
NAT ;
A32:
i + 1
<= j
by A29, A30, FINSEQ_3:152;
take j =
j;
( j in dom s2 & s1 . (i + 1) = s2 . j & i + 1 < j )thus
j in dom s2
by A31, FINSEQ_1:def 3;
( s1 . (i + 1) = s2 . j & i + 1 < j )thus
s1 . (i + 1) = s2 . j
by A24, A28, FUNCT_1:12;
i + 1 < j
j <> i + 1
by A24, A26, A28, FUNCT_1:12;
hence
i + 1
< j
by A32, XXREAL_0:1;
verum end;
then consider j being Nat such that
A33:
( j in dom s2 & i + 1 < j )
and
A34:
s1 . (i + 1) = s2 . j
;
take
i
; ex j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
take
j
; ( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
thus
( i in dom s1 & i in dom s2 )
by A7, A23; ( i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
thus
( i + 1 in dom s1 & i + 1 in dom s2 )
by A7, A24; ( j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
thus
( j in dom s2 & i + 1 < j )
by A33; ( s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )
thus
( s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) )
by A25, A26; s1 . (i + 1) = s2 . j
thus
s1 . (i + 1) = s2 . j
by A34; verum