let O be set ; :: thesis: for G being GroupWithOperators of O
for s1 being CompositionSeries of G st len s1 > 1 holds
( s1 is jordan_holder iff for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O )
let G be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G st len s1 > 1 holds
( s1 is jordan_holder iff for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O )
let s1 be CompositionSeries of G; :: thesis: ( len s1 > 1 implies ( s1 is jordan_holder iff for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O ) )
assume A1:
len s1 > 1
; :: thesis: ( s1 is jordan_holder iff for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O )
A2:
now assume A3:
s1 is
jordan_holder
;
:: thesis: for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of Oassume
ex
i being
Nat st
(
i in dom (the_series_of_quotients_of s1) &
(the_series_of_quotients_of s1) . i is not
strict simple GroupWithOperators of
O )
;
:: thesis: contradictionthen consider i being
Nat such that A4:
i in dom (the_series_of_quotients_of s1)
and A5:
(the_series_of_quotients_of s1) . i is not
strict simple GroupWithOperators of
O
;
A6:
len s1 = (len (the_series_of_quotients_of s1)) + 1
by A1, Def36;
0 + (len (the_series_of_quotients_of s1)) < 1
+ (len (the_series_of_quotients_of s1))
by XREAL_1:8;
then A7:
len (the_series_of_quotients_of s1) < len s1
by A1, Def36;
A8:
i in Seg (len (the_series_of_quotients_of s1))
by A4, FINSEQ_1:def 3;
then A9:
( 1
<= i &
i <= len (the_series_of_quotients_of s1) )
by FINSEQ_1:3;
then A10:
i <= len s1
by A7, XXREAL_0:2;
then
i in Seg (len s1)
by A9, FINSEQ_1:3;
then A11:
i in dom s1
by FINSEQ_1:def 3;
A12:
0 + 1
<= i + 1
by XREAL_1:8;
A13:
i + 1
<= len s1
by A6, A9, XREAL_1:8;
then
i + 1
in Seg (len s1)
by A12;
then A14:
i + 1
in dom s1
by FINSEQ_1:def 3;
then reconsider H1 =
s1 . i,
N1 =
s1 . (i + 1) as
Element of
the_stable_subgroups_of G by A11, FINSEQ_2:13;
reconsider H1 =
H1,
N1 =
N1 as
strict StableSubgroup of
G by Def11;
reconsider N1 =
N1 as
strict normal StableSubgroup of
H1 by A11, A14, Def31;
A15:
H1 ./. N1 is not
strict simple GroupWithOperators of
O
by A1, A4, A5, Def36;
per cases
( H1 ./. N1 is trivial or ex H being strict normal StableSubgroup of H1 ./. N1 st
( H <> (Omega). (H1 ./. N1) & H <> (1). (H1 ./. N1) ) )
by A15, Def13;
suppose
ex
H being
strict normal StableSubgroup of
H1 ./. N1 st
(
H <> (Omega). (H1 ./. N1) &
H <> (1). (H1 ./. N1) )
;
:: thesis: contradictionthen consider H being
strict normal StableSubgroup of
H1 ./. N1 such that A17:
(
H <> (Omega). (H1 ./. N1) &
H <> (1). (H1 ./. N1) )
;
N1 = Ker (nat_hom N1)
by Th48;
then consider N2 being
strict StableSubgroup of
H1 such that A18:
( the
carrier of
N2 = (nat_hom N1) " the
carrier of
H & (
H is
normal implies (
N1 is
normal StableSubgroup of
N2 &
N2 is
normal ) ) )
by Th78;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
N2 is
strict StableSubgroup of
G
by Th11;
then reconsider N2 =
N2 as
Element of
the_stable_subgroups_of G by Def11;
set s2 =
Ins s1,
i,
N2;
A19:
( 1
<= i & not
s1 is
empty )
by A1, A8, FINSEQ_1:3;
1
<= (len s1) + 1
by A1, NAT_1:13;
then A20:
1
<= len (Ins s1,i,N2)
by FINSEQ_5:72;
then
1
in Seg (len (Ins s1,i,N2))
;
then A21:
1
in dom (Ins s1,i,N2)
by FINSEQ_1:def 3;
1
in Seg (len s1)
by A1;
then A22:
1
in dom s1
by FINSEQ_1:def 3;
len (Ins s1,i,N2) in Seg (len (Ins s1,i,N2))
by A20;
then A23:
len (Ins s1,i,N2) in dom (Ins s1,i,N2)
by FINSEQ_1:def 3;
len s1 in Seg (len s1)
by A1;
then A24:
len s1 in dom s1
by FINSEQ_1:def 3;
A25:
(Ins s1,i,N2) . 1 =
(Ins s1,i,N2) /. 1
by A21, PARTFUN1:def 8
.=
s1 /. 1
by A19, FINSEQ_5:78
.=
s1 . 1
by A22, PARTFUN1:def 8
.=
(Omega). G
by Def31
;
A26:
(Ins s1,i,N2) . (len (Ins s1,i,N2)) =
(Ins s1,i,N2) /. (len (Ins s1,i,N2))
by A23, PARTFUN1:def 8
.=
(Ins s1,i,N2) /. ((len s1) + 1)
by FINSEQ_5:72
.=
s1 /. (len s1)
by A13, FINSEQ_5:77
.=
s1 . (len s1)
by A24, PARTFUN1:def 8
.=
(1). G
by Def31
;
A27:
len (Ins s1,i,N2) = (len s1) + 1
by FINSEQ_5:72;
then A28:
s1 <> Ins s1,
i,
N2
;
now let j be
Nat;
:: thesis: ( j in dom (Ins s1,i,N2) & j + 1 in dom (Ins s1,i,N2) implies for H1', H2' being StableSubgroup of G st H1' = (Ins s1,i,N2) . j & H2' = (Ins s1,i,N2) . (j + 1) holds
b5 is normal StableSubgroup of b4 )assume A29:
j in dom (Ins s1,i,N2)
;
:: thesis: ( j + 1 in dom (Ins s1,i,N2) implies for H1', H2' being StableSubgroup of G st H1' = (Ins s1,i,N2) . j & H2' = (Ins s1,i,N2) . (j + 1) holds
b5 is normal StableSubgroup of b4 )then
j in Seg (len (Ins s1,i,N2))
by FINSEQ_1:def 3;
then A30:
( 1
<= j &
j <= len (Ins s1,i,N2) )
by FINSEQ_1:3;
assume A31:
j + 1
in dom (Ins s1,i,N2)
;
:: thesis: for H1', H2' being StableSubgroup of G st H1' = (Ins s1,i,N2) . j & H2' = (Ins s1,i,N2) . (j + 1) holds
b5 is normal StableSubgroup of b4then
j + 1
in Seg (len (Ins s1,i,N2))
by FINSEQ_1:def 3;
then A32:
( 1
<= j + 1 &
j + 1
<= len (Ins s1,i,N2) )
by FINSEQ_1:3;
let H1',
H2' be
StableSubgroup of
G;
:: thesis: ( H1' = (Ins s1,i,N2) . j & H2' = (Ins s1,i,N2) . (j + 1) implies b3 is normal StableSubgroup of b2 )assume A33:
H1' = (Ins s1,i,N2) . j
;
:: thesis: ( H2' = (Ins s1,i,N2) . (j + 1) implies b3 is normal StableSubgroup of b2 )assume A34:
H2' = (Ins s1,i,N2) . (j + 1)
;
:: thesis: b3 is normal StableSubgroup of b2
(
j < i or
j = i or
j > i )
by XXREAL_0:1;
then
(
j + 1
<= i or
j = i or
j >= i + 1 )
by NAT_1:13;
then A35:
(
(j + 1) - 1
<= i - 1 or
j = i or
j >= i + 1 )
by XREAL_1:11;
per cases
( j <= i - 1 or j = i or j = i + 1 or i + 1 < j )
by A35, XXREAL_0:1;
suppose A36:
j <= i - 1
;
:: thesis: b3 is normal StableSubgroup of b2A37:
Seg (len (s1 | i)) = Seg i
by A7, A9, FINSEQ_1:80, XXREAL_0:2;
A38:
dom (s1 | i) c= dom s1
by RELAT_1:89;
(- 1) + i < 0 + i
by XREAL_1:8;
then
j <= i
by A36, XXREAL_0:2;
then
j in Seg (len (s1 | i))
by A30, A37, FINSEQ_1:3;
then A39:
j in dom (s1 | i)
by FINSEQ_1:def 3;
j + 1
<= (i - 1) + 1
by A36, XREAL_1:8;
then
j + 1
in Seg (len (s1 | i))
by A32, A37;
then A40:
j + 1
in dom (s1 | i)
by FINSEQ_1:def 3;
A41:
(Ins s1,i,N2) . j =
(Ins s1,i,N2) /. j
by A29, PARTFUN1:def 8
.=
s1 /. j
by A39, FINSEQ_5:75
.=
s1 . j
by A38, A39, PARTFUN1:def 8
;
(Ins s1,i,N2) . (j + 1) =
(Ins s1,i,N2) /. (j + 1)
by A31, PARTFUN1:def 8
.=
s1 /. (j + 1)
by A40, FINSEQ_5:75
.=
s1 . (j + 1)
by A38, A40, PARTFUN1:def 8
;
hence
H2' is
normal StableSubgroup of
H1'
by A33, A34, A38, A39, A40, A41, Def31;
:: thesis: verum end; suppose A42:
j = i
;
:: thesis: b3 is normal StableSubgroup of b2then A43:
(Ins s1,i,N2) . (j + 1) =
(Ins s1,i,N2) /. (i + 1)
by A31, PARTFUN1:def 8
.=
N2
by A7, A9, FINSEQ_5:76, XXREAL_0:2
;
A44:
Seg (len (s1 | i)) = Seg i
by A7, A9, FINSEQ_1:80, XXREAL_0:2;
A45:
dom (s1 | i) c= dom s1
by RELAT_1:89;
j in Seg i
by A30, A42;
then A46:
j in dom (s1 | i)
by A44, FINSEQ_1:def 3;
(Ins s1,i,N2) . j =
(Ins s1,i,N2) /. j
by A29, PARTFUN1:def 8
.=
s1 /. j
by A46, FINSEQ_5:75
.=
s1 . j
by A45, A46, PARTFUN1:def 8
;
hence
H2' is
normal StableSubgroup of
H1'
by A18, A33, A34, A42, A43;
:: thesis: verum end; suppose A47:
j = i + 1
;
:: thesis: b3 is normal StableSubgroup of b2
i + 1
<= (len s1) + 1
by A10, XREAL_1:8;
then
( 1
<= i + 1 &
i + 1
<= len (Ins s1,i,N2) )
by A12, FINSEQ_5:72;
then
i + 1
in Seg (len (Ins s1,i,N2))
;
then
i + 1
in dom (Ins s1,i,N2)
by FINSEQ_1:def 3;
then A48:
H1' =
(Ins s1,i,N2) /. (i + 1)
by A33, A47, PARTFUN1:def 8
.=
N2
by A7, A9, FINSEQ_5:76, XXREAL_0:2
;
(i + 1) + 1
<= (len s1) + 1
by A13, XREAL_1:8;
then
( 1
<= (i + 1) + 1 &
(i + 1) + 1
<= len (Ins s1,i,N2) )
by A12, FINSEQ_5:72, XREAL_1:8;
then
(i + 1) + 1
in Seg (len (Ins s1,i,N2))
;
then
(i + 1) + 1
in dom (Ins s1,i,N2)
by FINSEQ_1:def 3;
then H2' =
(Ins s1,i,N2) /. ((i + 1) + 1)
by A34, A47, PARTFUN1:def 8
.=
s1 /. (i + 1)
by A13, FINSEQ_5:77
.=
N1
by A14, PARTFUN1:def 8
;
hence
H2' is
normal StableSubgroup of
H1'
by A18, A48;
:: thesis: verum end; suppose A49:
i + 1
< j
;
:: thesis: b3 is normal StableSubgroup of b2then
(i + 1) + 1
<= j
by NAT_1:13;
then A50:
((i + 1) + 1) - 1
<= j - 1
by XREAL_1:11;
set j' =
j - 1;
0 + 1
<= i + 1
by XREAL_1:8;
then A51:
0 + 1
< j
by A49, XXREAL_0:2;
then A52:
(0 + 1) - 1
< j - 1
by XREAL_1:11;
then reconsider j' =
j - 1 as
Element of
NAT by INT_1:16;
A53:
j - 1
<= (len (Ins s1,i,N2)) - 1
by A30, XREAL_1:11;
0 + j' < 1
+ j'
by XREAL_1:8;
then A54:
i + 1
<= j' + 1
by A50, XXREAL_0:2;
A55:
(j + 1) - 1
<= (len (Ins s1,i,N2)) - 1
by A32, XREAL_1:11;
0 + 1
<= j'
by A52, NAT_1:13;
then
j' in Seg (len s1)
by A27, A53;
then A56:
j' in dom s1
by FINSEQ_1:def 3;
j' + 1
in Seg (len s1)
by A27, A51, A55;
then A57:
j' + 1
in dom s1
by FINSEQ_1:def 3;
A58:
(Ins s1,i,N2) . j =
(Ins s1,i,N2) /. (j' + 1)
by A29, PARTFUN1:def 8
.=
s1 /. j'
by A27, A50, A53, FINSEQ_5:77
.=
s1 . j'
by A56, PARTFUN1:def 8
;
(Ins s1,i,N2) . (j + 1) =
(Ins s1,i,N2) /. ((j' + 1) + 1)
by A31, PARTFUN1:def 8
.=
s1 /. (j' + 1)
by A27, A54, A55, FINSEQ_5:77
.=
s1 . (j' + 1)
by A57, PARTFUN1:def 8
;
hence
H2' is
normal StableSubgroup of
H1'
by A33, A34, A56, A57, A58, Def31;
:: thesis: verum end; end; then reconsider s2 =
Ins s1,
i,
N2 as
CompositionSeries of
G by A25, A26, Def31;
now let j be
Nat;
:: thesis: ( j in dom s2 & j + 1 in dom s2 implies for H1' being StableSubgroup of G
for N1' being normal StableSubgroup of H1' st H1' = s2 . j & N1' = s2 . (j + 1) holds
not b4 ./. b5 is trivial )assume A59:
j in dom s2
;
:: thesis: ( j + 1 in dom s2 implies for H1' being StableSubgroup of G
for N1' being normal StableSubgroup of H1' st H1' = s2 . j & N1' = s2 . (j + 1) holds
not b4 ./. b5 is trivial )then
j in Seg (len s2)
by FINSEQ_1:def 3;
then A60:
( 1
<= j &
j <= len s2 )
by FINSEQ_1:3;
assume A61:
j + 1
in dom s2
;
:: thesis: for H1' being StableSubgroup of G
for N1' being normal StableSubgroup of H1' st H1' = s2 . j & N1' = s2 . (j + 1) holds
not b4 ./. b5 is trivial then
j + 1
in Seg (len s2)
by FINSEQ_1:def 3;
then A62:
( 1
<= j + 1 &
j + 1
<= len s2 )
by FINSEQ_1:3;
let H1' be
StableSubgroup of
G;
:: thesis: for N1' being normal StableSubgroup of H1' st H1' = s2 . j & N1' = s2 . (j + 1) holds
not b3 ./. b4 is trivial let N1' be
normal StableSubgroup of
H1';
:: thesis: ( H1' = s2 . j & N1' = s2 . (j + 1) implies not b2 ./. b3 is trivial )assume A63:
H1' = s2 . j
;
:: thesis: ( N1' = s2 . (j + 1) implies not b2 ./. b3 is trivial )assume A64:
N1' = s2 . (j + 1)
;
:: thesis: not b2 ./. b3 is trivial
(
j < i or
j = i or
j > i )
by XXREAL_0:1;
then
(
j + 1
<= i or
j = i or
j >= i + 1 )
by NAT_1:13;
then A65:
(
(j + 1) - 1
<= i - 1 or
j = i or
j >= i + 1 )
by XREAL_1:11;
A66:
s1 is
strictly_decreasing
by A3, Def34;
per cases
( j <= i - 1 or j = i or j = i + 1 or i + 1 < j )
by A65, XXREAL_0:1;
suppose A67:
j <= i - 1
;
:: thesis: not b2 ./. b3 is trivial A68:
Seg (len (s1 | i)) = Seg i
by A7, A9, FINSEQ_1:80, XXREAL_0:2;
A69:
dom (s1 | i) c= dom s1
by RELAT_1:89;
(- 1) + i < 0 + i
by XREAL_1:8;
then
j <= i
by A67, XXREAL_0:2;
then
j in Seg (len (s1 | i))
by A60, A68, FINSEQ_1:3;
then A70:
j in dom (s1 | i)
by FINSEQ_1:def 3;
j + 1
<= (i - 1) + 1
by A67, XREAL_1:8;
then
j + 1
in Seg (len (s1 | i))
by A62, A68;
then A71:
j + 1
in dom (s1 | i)
by FINSEQ_1:def 3;
A72:
s2 . j =
s2 /. j
by A59, PARTFUN1:def 8
.=
s1 /. j
by A70, FINSEQ_5:75
.=
s1 . j
by A69, A70, PARTFUN1:def 8
;
s2 . (j + 1) =
s2 /. (j + 1)
by A61, PARTFUN1:def 8
.=
s1 /. (j + 1)
by A71, FINSEQ_5:75
.=
s1 . (j + 1)
by A69, A71, PARTFUN1:def 8
;
hence
not
H1' ./. N1' is
trivial
by A63, A64, A66, A69, A70, A71, A72, Def33;
:: thesis: verum end; suppose A73:
j = i
;
:: thesis: not b2 ./. b3 is trivial then A74:
s2 . (j + 1) =
s2 /. (i + 1)
by A61, PARTFUN1:def 8
.=
N2
by A7, A9, FINSEQ_5:76, XXREAL_0:2
;
reconsider N2 =
N2 as
normal StableSubgroup of
H1 by A18;
A75:
Seg (len (s1 | i)) = Seg i
by A7, A9, FINSEQ_1:80, XXREAL_0:2;
A76:
dom (s1 | i) c= dom s1
by RELAT_1:89;
j in Seg i
by A60, A73;
then A77:
j in dom (s1 | i)
by A75, FINSEQ_1:def 3;
A78:
s2 . j =
s2 /. j
by A59, PARTFUN1:def 8
.=
s1 /. j
by A77, FINSEQ_5:75
.=
s1 . j
by A76, A77, PARTFUN1:def 8
;
hence
not
H1' ./. N1' is
trivial
;
:: thesis: verum end; suppose A79:
j = i + 1
;
:: thesis: not b2 ./. b3 is trivial
i + 1
<= (len s1) + 1
by A10, XREAL_1:8;
then
( 1
<= i + 1 &
i + 1
<= len s2 )
by A12, FINSEQ_5:72;
then
i + 1
in Seg (len s2)
;
then
i + 1
in dom s2
by FINSEQ_1:def 3;
then A80:
H1' =
s2 /. (i + 1)
by A63, A79, PARTFUN1:def 8
.=
N2
by A7, A9, FINSEQ_5:76, XXREAL_0:2
;
(i + 1) + 1
<= (len s1) + 1
by A13, XREAL_1:8;
then
( 1
<= (i + 1) + 1 &
(i + 1) + 1
<= len s2 )
by A12, FINSEQ_5:72, XREAL_1:8;
then
(i + 1) + 1
in Seg (len s2)
;
then
(i + 1) + 1
in dom s2
by FINSEQ_1:def 3;
then A81:
N1' =
s2 /. ((i + 1) + 1)
by A64, A79, PARTFUN1:def 8
.=
s1 /. (i + 1)
by A13, FINSEQ_5:77
.=
N1
by A14, PARTFUN1:def 8
;
hence
not
H1' ./. N1' is
trivial
;
:: thesis: verum end; suppose A82:
i + 1
< j
;
:: thesis: not b2 ./. b3 is trivial then
(i + 1) + 1
<= j
by NAT_1:13;
then A83:
((i + 1) + 1) - 1
<= j - 1
by XREAL_1:11;
set j' =
j - 1;
A84:
0 + 1
<= i + 1
by XREAL_1:8;
then
0 + 1
< j
by A82, XXREAL_0:2;
then A85:
(0 + 1) - 1
< j - 1
by XREAL_1:11;
then reconsider j' =
j - 1 as
Element of
NAT by INT_1:16;
A86:
j - 1
<= (len s2) - 1
by A60, XREAL_1:11;
0 + j' < 1
+ j'
by XREAL_1:8;
then A87:
i + 1
<= j' + 1
by A83, XXREAL_0:2;
A88:
(j + 1) - 1
<= (len s2) - 1
by A62, XREAL_1:11;
0 + 1
<= j'
by A85, NAT_1:13;
then
j' in Seg (len s1)
by A27, A86;
then A89:
j' in dom s1
by FINSEQ_1:def 3;
1
<= j' + 1
by A82, A84, XXREAL_0:2;
then
j' + 1
in Seg (len s1)
by A27, A88;
then A90:
j' + 1
in dom s1
by FINSEQ_1:def 3;
A91:
s2 . j =
s2 /. (j' + 1)
by A59, PARTFUN1:def 8
.=
s1 /. j'
by A27, A83, A86, FINSEQ_5:77
.=
s1 . j'
by A89, PARTFUN1:def 8
;
s2 . (j + 1) =
s2 /. ((j' + 1) + 1)
by A61, PARTFUN1:def 8
.=
s1 /. (j' + 1)
by A27, A87, A88, FINSEQ_5:77
.=
s1 . (j' + 1)
by A90, PARTFUN1:def 8
;
hence
not
H1' ./. N1' is
trivial
by A63, A64, A66, A89, A90, A91, Def33;
:: thesis: verum end; end; then A92:
s2 is
strictly_decreasing
by Def33;
A93:
(dom s2) \ {(i + 1)} c= dom s2
by XBOOLE_1:36;
s1 = Del s2,
(i + 1)
by A11, Lm44;
then
s2 is_finer_than s1
by A93, Def32;
hence
contradiction
by A3, A28, A92, Def34;
:: thesis: verum end; end;
now assume A94:
for
i being
Nat st
i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is
strict simple GroupWithOperators of
O
;
:: thesis: s1 is jordan_holder assume A95:
not
s1 is
jordan_holder
;
:: thesis: contradictionper cases
( not s1 is strictly_decreasing or ex s2 being CompositionSeries of G st
( s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 ) )
by A95, Def34;
suppose
not
s1 is
strictly_decreasing
;
:: thesis: contradictionthen
ex
i being
Nat st
(
i in dom s1 &
i + 1
in dom s1 & ex
H1 being
StableSubgroup of
G ex
N1 being
normal StableSubgroup of
H1 st
(
H1 = s1 . i &
N1 = s1 . (i + 1) &
H1 ./. N1 is
trivial ) )
by Def33;
then consider i being
Nat,
H1 being
StableSubgroup of
G,
N1 being
normal StableSubgroup of
H1 such that A96:
(
i in dom s1 &
i + 1
in dom s1 )
and A97:
(
H1 = s1 . i &
N1 = s1 . (i + 1) )
and A98:
H1 ./. N1 is
trivial
;
(
i in Seg (len s1) &
i + 1
in Seg (len s1) )
by A96, FINSEQ_1:def 3;
then A99:
( 1
<= i &
i + 1
<= len s1 )
by FINSEQ_1:3;
then
1
+ 1
<= i + 1
by XREAL_1:8;
then
1
+ 1
<= len s1
by A99, XXREAL_0:2;
then A100:
len s1 > 1
by NAT_1:13;
then
(len (the_series_of_quotients_of s1)) + 1
= len s1
by Def36;
then
len (the_series_of_quotients_of s1) = (len s1) - 1
;
then
(i + 1) - 1
<= len (the_series_of_quotients_of s1)
by A99, XREAL_1:11;
then
i in Seg (len (the_series_of_quotients_of s1))
by A99, FINSEQ_1:3;
then A101:
i in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
then
(
H1 ./. N1 is
trivial &
(the_series_of_quotients_of s1) . i = H1 ./. N1 )
by A97, A98, A100, Def36;
then
H1 ./. N1 is
strict simple GroupWithOperators of
O
by A94, A101;
hence
contradiction
by A98, Def13;
:: thesis: verum end; suppose
ex
s2 being
CompositionSeries of
G st
(
s2 <> s1 &
s2 is
strictly_decreasing &
s2 is_finer_than s1 )
;
:: thesis: contradictionthen consider s2 being
CompositionSeries of
G such that A102:
(
s2 <> s1 &
s2 is
strictly_decreasing &
s2 is_finer_than s1 )
;
consider i,
j being
Nat such that A103:
(
i in dom s1 &
i in dom s2 &
i + 1
in dom s1 &
i + 1
in dom s2 &
j in dom s2 )
and A104:
(
i + 1
< j &
s1 . i = s2 . i &
s1 . (i + 1) <> s2 . (i + 1) &
s1 . (i + 1) = s2 . j )
by A1, A102, Th100;
reconsider H1 =
s1 . i,
H2 =
s1 . (i + 1),
H =
s2 . (i + 1) as
Element of
the_stable_subgroups_of G by A103, FINSEQ_2:13;
reconsider H1 =
H1,
H2 =
H2,
H =
H as
strict StableSubgroup of
G by Def11;
reconsider H =
H as
strict normal StableSubgroup of
H1 by A103, A104, Def31;
reconsider H2 =
H2 as
strict normal StableSubgroup of
H1 by A103, Def31;
reconsider H3 =
HGrWOpStr(# the
carrier of
H2,the
multF of
H2,the
action of
H2 #) as
strict normal StableSubgroup of
H by A103, A104, Th40, Th101;
reconsider H2' =
H2 as
normal StableSubgroup of
H by A103, A104, Th40, Th101;
reconsider J =
H ./. H2' as
strict normal StableSubgroup of
H1 ./. H2 by Th44;
then A108:
H1 ./. H2 is not
simple GroupWithOperators of
O
by A105, Def13;
(
i in Seg (len s1) &
i + 1
in Seg (len s1) )
by A103, FINSEQ_1:def 3;
then A109:
( 1
<= i &
i + 1
<= len s1 )
by FINSEQ_1:3;
then
1
+ 1
<= i + 1
by XREAL_1:8;
then
1
+ 1
<= len s1
by A109, XXREAL_0:2;
then A110:
len s1 > 1
by NAT_1:13;
then
(len (the_series_of_quotients_of s1)) + 1
= len s1
by Def36;
then
len (the_series_of_quotients_of s1) = (len s1) - 1
;
then
(i + 1) - 1
<= len (the_series_of_quotients_of s1)
by A109, XREAL_1:11;
then
i in Seg (len (the_series_of_quotients_of s1))
by A109, FINSEQ_1:3;
then A111:
i in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
then
(the_series_of_quotients_of s1) . i = H1 ./. H2
by A110, Def36;
hence
contradiction
by A94, A108, A111;
:: thesis: verum end; end;
hence
( s1 is jordan_holder iff for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O )
by A2; :: thesis: verum