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 holds
. 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 holds
. 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 holds
. 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 holds
. i is strict simple GroupWithOperators of O )

A2: now :: thesis: ( s1 is jordan_holder implies for i being Nat st i in dom holds
. i is strict simple GroupWithOperators of O )
assume A3: s1 is jordan_holder ; :: thesis: for i being Nat st i in dom holds
. i is strict simple GroupWithOperators of O

assume ex i being Nat st
( i in dom & . i is not strict simple GroupWithOperators of O ) ; :: thesis: contradiction
then consider i being Nat such that
A4: i in dom and
A5: (the_series_of_quotients_of s1) . i is not strict simple GroupWithOperators of O ;
A6: i in Seg () by ;
then A7: i <= len by FINSEQ_1:1;
len s1 = () + 1 by ;
then A8: i + 1 <= len s1 by ;
0 + 1 <= i + 1 by XREAL_1:6;
then i + 1 in Seg (len s1) by A8;
then A10: i + 1 in dom s1 by FINSEQ_1:def 3;
0 + () < 1 + () by XREAL_1:6;
then A11: len < len s1 by ;
then A12: i <= len s1 by ;
1 <= i by ;
then i in Seg (len s1) by A12;
then A13: i 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 ;
reconsider H1 = H1, N1 = N1 as strict StableSubgroup of G by Def11;
reconsider N1 = N1 as strict normal StableSubgroup of H1 by ;
A14: H1 ./. N1 is not strict simple GroupWithOperators of O by A1, A4, A5, Def33;
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 ;
suppose ex H being strict normal StableSubgroup of H1 ./. N1 st
( H <> (Omega). (H1 ./. N1) & H <> (1). (H1 ./. N1) ) ; :: thesis: contradiction
then consider H being strict normal StableSubgroup of H1 ./. N1 such that
A16: H <> (Omega). (H1 ./. N1) and
A17: 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 and
A19: ( H is normal implies ( N1 is normal StableSubgroup of N2 & N2 is normal ) ) by Th78;
A20: N2 is strict StableSubgroup of G by Th11;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A21: ( 1 <= i & not s1 is empty ) by ;
reconsider N2 = N2 as Element of the_stable_subgroups_of G by ;
set s2 = Ins (s1,i,N2);
A22: len (Ins (s1,i,N2)) = (len s1) + 1 by FINSEQ_5:69;
then A23: s1 <> Ins (s1,i,N2) ;
A24: now :: thesis: for j being Nat st j in dom (Ins (s1,i,N2)) & j + 1 in dom (Ins (s1,i,N2)) holds
for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds
H29 is normal StableSubgroup of H19
let j be Nat; :: thesis: ( j in dom (Ins (s1,i,N2)) & j + 1 in dom (Ins (s1,i,N2)) implies for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds
b5 is normal StableSubgroup of b4 )

assume j in dom (Ins (s1,i,N2)) ; :: thesis: ( j + 1 in dom (Ins (s1,i,N2)) implies for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds
b5 is normal StableSubgroup of b4 )

then A26: j in Seg (len (Ins (s1,i,N2))) by FINSEQ_1:def 3;
then A27: 1 <= j by FINSEQ_1:1;
A28: j <= len (Ins (s1,i,N2)) by ;
( 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 A29: ( (j + 1) - 1 <= i - 1 or j = i or j >= i + 1 ) by XREAL_1:9;
assume j + 1 in dom (Ins (s1,i,N2)) ; :: thesis: for H19, H29 being StableSubgroup of G st H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) holds
b5 is normal StableSubgroup of b4

then A31: j + 1 in Seg (len (Ins (s1,i,N2))) by FINSEQ_1:def 3;
then A32: 1 <= j + 1 by FINSEQ_1:1;
A33: j + 1 <= len (Ins (s1,i,N2)) by ;
let H19, H29 be StableSubgroup of G; :: thesis: ( H19 = (Ins (s1,i,N2)) . j & H29 = (Ins (s1,i,N2)) . (j + 1) implies b3 is normal StableSubgroup of b2 )
assume A34: H19 = (Ins (s1,i,N2)) . j ; :: thesis: ( H29 = (Ins (s1,i,N2)) . (j + 1) implies b3 is normal StableSubgroup of b2 )
assume A35: H29 = (Ins (s1,i,N2)) . (j + 1) ; :: thesis: b3 is normal StableSubgroup of b2
per cases ( j <= i - 1 or j = i or j = i + 1 or i + 1 < j ) by ;
suppose A36: j <= i - 1 ; :: thesis: b3 is normal StableSubgroup of b2
A37: Seg (len (s1 | i)) = Seg i by ;
A38: dom (s1 | i) c= dom s1 by RELAT_1:60;
(- 1) + i < 0 + i by XREAL_1:6;
then j <= i by ;
then j in Seg (len (s1 | i)) by ;
then A39: j in dom (s1 | i) by FINSEQ_1:def 3;
j + 1 <= (i - 1) + 1 by ;
then j + 1 in Seg (len (s1 | i)) by ;
then A40: j + 1 in dom (s1 | i) by FINSEQ_1:def 3;
A41: (Ins (s1,i,N2)) . (j + 1) = s1 . (j + 1) by ;
(Ins (s1,i,N2)) . j = s1 . j by ;
hence H29 is normal StableSubgroup of H19 by A34, A35, A38, A39, A40, A41, Def28; :: thesis: verum
end;
suppose A42: j = i ; :: thesis: b3 is normal StableSubgroup of b2
then A43: j in Seg i by A27;
Seg (len (s1 | i)) = Seg i by ;
then A44: j in dom (s1 | i) by ;
A46: (Ins (s1,i,N2)) . j = s1 . j by ;
(Ins (s1,i,N2)) . (j + 1) = N2 by ;
hence H29 is normal StableSubgroup of H19 by A19, A34, A35, A42, A46; :: thesis: verum
end;
suppose A50: i + 1 < j ; :: thesis: b3 is normal StableSubgroup of b2
set j9 = j - 1;
0 + 1 <= i + 1 by XREAL_1:6;
then A51: 0 + 1 < j by ;
then A52: (0 + 1) - 1 < j - 1 by XREAL_1:9;
then reconsider j9 = j - 1 as Element of NAT by INT_1:3;
A53: j - 1 <= (len (Ins (s1,i,N2))) - 1 by ;
0 + 1 <= j9 by ;
then A54: j9 in dom s1 by ;
(i + 1) + 1 <= j by ;
then A55: ((i + 1) + 1) - 1 <= j - 1 by XREAL_1:9;
0 + j9 < 1 + j9 by XREAL_1:6;
then A56: i + 1 <= j9 + 1 by ;
A57: (j + 1) - 1 <= (len (Ins (s1,i,N2))) - 1 by ;
then A58: j9 + 1 in dom s1 by ;
A59: (Ins (s1,i,N2)) . (j + 1) = s1 . (j9 + 1) by ;
(Ins (s1,i,N2)) . j = (Ins (s1,i,N2)) . (j9 + 1)
.= s1 . j9 by ;
hence H29 is normal StableSubgroup of H19 by A34, A35, A54, A58, A59, Def28; :: thesis: verum
end;
end;
end;
A63: (Ins (s1,i,N2)) . (len (Ins (s1,i,N2))) = (Ins (s1,i,N2)) . ((len s1) + 1) by FINSEQ_5:69
.= s1 . (len s1) by
.= (1). G by Def28 ;
(Ins (s1,i,N2)) . 1 = s1 . 1 by
.= (Omega). G by Def28 ;
then reconsider s2 = Ins (s1,i,N2) as CompositionSeries of G by ;
now :: thesis: for j being Nat st j in dom s2 & j + 1 in dom s2 holds
for H19 being StableSubgroup of G
for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds
not H19 ./. N19 is trivial
let j be Nat; :: thesis: ( j in dom s2 & j + 1 in dom s2 implies for H19 being StableSubgroup of G
for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds
not b4 ./. b5 is trivial )

assume j in dom s2 ; :: thesis: ( j + 1 in dom s2 implies for H19 being StableSubgroup of G
for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds
not b4 ./. b5 is trivial )

then A65: j in Seg (len s2) by FINSEQ_1:def 3;
then A66: 1 <= j by FINSEQ_1:1;
( 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 A67: ( (j + 1) - 1 <= i - 1 or j = i or j >= i + 1 ) by XREAL_1:9;
assume j + 1 in dom s2 ; :: thesis: for H19 being StableSubgroup of G
for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds
not b4 ./. b5 is trivial

then A69: j + 1 in Seg (len s2) by FINSEQ_1:def 3;
then A70: 1 <= j + 1 by FINSEQ_1:1;
A71: j + 1 <= len s2 by ;
let H19 be StableSubgroup of G; :: thesis: for N19 being normal StableSubgroup of H19 st H19 = s2 . j & N19 = s2 . (j + 1) holds
not b3 ./. b4 is trivial

let N19 be normal StableSubgroup of H19; :: thesis: ( H19 = s2 . j & N19 = s2 . (j + 1) implies not b2 ./. b3 is trivial )
assume A72: H19 = s2 . j ; :: thesis: ( N19 = s2 . (j + 1) implies not b2 ./. b3 is trivial )
A73: j <= len s2 by ;
A74: s1 is strictly_decreasing by A3;
assume A75: N19 = s2 . (j + 1) ; :: thesis: not b2 ./. b3 is trivial
per cases ( j <= i - 1 or j = i or j = i + 1 or i + 1 < j ) by ;
suppose A76: j <= i - 1 ; :: thesis: not b2 ./. b3 is trivial
Seg (len (s1 | i)) = Seg i by ;
then S: dom (s1 | i) = Seg i by FINSEQ_1:def 3;
A78: dom (s1 | i) c= dom s1 by RELAT_1:60;
(- 1) + i < 0 + i by XREAL_1:6;
then j <= i by ;
then A79: j in dom (s1 | i) by A66, S;
j + 1 <= (i - 1) + 1 by ;
then A80: j + 1 in dom (s1 | i) by A70, S;
then A81: s2 . (j + 1) = s1 . (j + 1) by FINSEQ_5:72;
s2 . j = s1 . j by ;
hence not H19 ./. N19 is trivial by A72, A75, A74, A78, A79, A80, A81; :: thesis: verum
end;
suppose A82: j = i ; :: thesis: not b2 ./. b3 is trivial
then A83: j in Seg i by A66;
Seg (len (s1 | i)) = Seg i by ;
then A84: j in dom (s1 | i) by ;
A85: s2 . (j + 1) = N2 by ;
reconsider N2 = N2 as normal StableSubgroup of H1 by A19;
A87: s2 . j = s1 . j by ;
now :: thesis: not H19 ./. N19 is trivial
assume H19 ./. N19 is trivial ; :: thesis: contradiction
then H1 = N2 by A72, A75, A82, A85, A87, Th76;
hence contradiction by A16, A18, Th80; :: thesis: verum
end;
hence not H19 ./. N19 is trivial ; :: thesis: verum
end;
suppose A88: j = i + 1 ; :: thesis: not b2 ./. b3 is trivial
then A89: H19 = N2 by ;
A91: N19 = s1 . (i + 1) by ;
now :: thesis: not H19 ./. N19 is trivial
assume H19 ./. N19 is trivial ; :: thesis: contradiction
then the carrier of N1 = (nat_hom N1) " the carrier of H by ;
hence contradiction by A17, Th81; :: thesis: verum
end;
hence not H19 ./. N19 is trivial ; :: thesis: verum
end;
suppose A92: i + 1 < j ; :: thesis: not b2 ./. b3 is trivial
set j9 = j - 1;
A93: 0 + 1 <= i + 1 by XREAL_1:6;
then 0 + 1 < j by ;
then A94: (0 + 1) - 1 < j - 1 by XREAL_1:9;
then reconsider j9 = j - 1 as Element of NAT by INT_1:3;
A95: (j + 1) - 1 <= (len s2) - 1 by ;
(i + 1) + 1 <= j by ;
then A96: ((i + 1) + 1) - 1 <= j - 1 by XREAL_1:9;
1 <= j9 + 1 by ;
then A97: j9 + 1 in dom s1 by ;
0 + j9 < 1 + j9 by XREAL_1:6;
then A98: i + 1 <= j9 + 1 by ;
A99: s2 . (j + 1) = s1 . (j9 + 1) by ;
A100: j - 1 <= (len s2) - 1 by ;
0 + 1 <= j9 by ;
then A101: j9 in dom s1 by ;
s2 . j = s2 . (j9 + 1)
.= s1 . j9 by ;
hence not H19 ./. N19 is trivial by A72, A75, A74, A101, A97, A99; :: thesis: verum
end;
end;
end;
then A102: s2 is strictly_decreasing ;
( (dom s2) \ {(i + 1)} c= dom s2 & s1 = Del (s2,(i + 1)) ) by ;
then s2 is_finer_than s1 ;
hence contradiction by A3, A23, A102; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( for i being Nat st i in dom holds
. i is strict simple GroupWithOperators of O ) implies s1 is jordan_holder )
assume A103: for i being Nat st i in dom holds
. i is strict simple GroupWithOperators of O ; :: thesis: s1 is jordan_holder
assume A104: not s1 is jordan_holder ; :: thesis: contradiction
per 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 A104;
suppose not s1 is strictly_decreasing ; :: thesis: contradiction
then 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 ) ) ;
then consider i being Nat, H1 being StableSubgroup of G, N1 being normal StableSubgroup of H1 such that
A105: i in dom s1 and
A106: i + 1 in dom s1 and
A107: ( H1 = s1 . i & N1 = s1 . (i + 1) ) and
A108: H1 ./. N1 is trivial ;
A109: i + 1 <= len s1 by ;
A110: 1 <= i by ;
then 1 + 1 <= i + 1 by XREAL_1:6;
then 1 + 1 <= len s1 by ;
then A111: len s1 > 1 by NAT_1:13;
then (len ) + 1 = len s1 by Def33;
then len = (len s1) - 1 ;
then (i + 1) - 1 <= len by ;
then i in Seg () by A110;
then A112: i in dom by FINSEQ_1:def 3;
then (the_series_of_quotients_of s1) . i = H1 ./. N1 by ;
then H1 ./. N1 is strict simple GroupWithOperators of O by ;
hence contradiction by A108, Def13; :: thesis: verum
end;
suppose ex s2 being CompositionSeries of G st
( s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 ) ; :: thesis: contradiction
then consider s2 being CompositionSeries of G such that
A113: s2 <> s1 and
A114: s2 is strictly_decreasing and
A115: s2 is_finer_than s1 ;
consider i, j being Nat such that
A116: i in dom s1 and
A117: i in dom s2 and
A118: i + 1 in dom s1 and
A119: i + 1 in dom s2 and
A120: ( j in dom s2 & i + 1 < j ) and
A121: s1 . i = s2 . i and
A122: s1 . (i + 1) <> s2 . (i + 1) and
A123: s1 . (i + 1) = s2 . j by ;
reconsider H1 = s1 . i, H2 = s1 . (i + 1), H = s2 . (i + 1) as Element of the_stable_subgroups_of G by ;
reconsider H1 = H1, H2 = H2, H = H as strict StableSubgroup of G by Def11;
reconsider H2 = H2 as strict normal StableSubgroup of H1 by ;
reconsider H = H as strict normal StableSubgroup of H1 by ;
reconsider H29 = H2 as normal StableSubgroup of H by ;
reconsider J = H ./. H29 as strict normal StableSubgroup of H1 ./. H2 by Th44;
A124: now :: thesis: not J = (Omega). (H1 ./. H2)
assume J = (Omega). (H1 ./. H2) ; :: thesis: contradiction
then A125: the carrier of H = union (Cosets H2) by Th22;
then A126: H = H1 by ;
then reconsider H1 = H1 as strict normal StableSubgroup of H ;
H1 = (Omega). H by ;
then H ./. H1 is trivial by Th57;
hence contradiction by A114, A117, A119, A121, A126; :: thesis: verum
end;
reconsider H3 = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #) as strict normal StableSubgroup of H by ;
now :: thesis: not J = (1). (H1 ./. H2)
assume J = (1). (H1 ./. H2) ; :: thesis: contradiction
then union (Cosets H3) = union {(1_ (H1 ./. H2))} by Def8;
then the carrier of H = union {(1_ (H1 ./. H2))} by Th22;
then the carrier of H = 1_ (H1 ./. H2) by ZFMISC_1:25;
then the carrier of H = carr H2 by Th43;
hence contradiction by A122, Lm4; :: thesis: verum
end;
then A127: H1 ./. H2 is not simple GroupWithOperators of O by ;
i + 1 in Seg (len s1) by ;
then A128: i + 1 <= len s1 by FINSEQ_1:1;
i in Seg (len s1) by ;
then A129: 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then 1 + 1 <= len s1 by ;
then A130: len s1 > 1 by NAT_1:13;
then (len ) + 1 = len s1 by Def33;
then len = (len s1) - 1 ;
then (i + 1) - 1 <= len by ;
then i in Seg () by A129;
then A131: i in dom by FINSEQ_1:def 3;
then (the_series_of_quotients_of s1) . i = H1 ./. H2 by ;
hence contradiction by A103, A127, A131; :: thesis: verum
end;
end;
end;
hence ( s1 is jordan_holder iff for i being Nat st i in dom holds
. i is strict simple GroupWithOperators of O ) by A2; :: thesis: verum