let O be set ; :: thesis: for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for fs being FinSequence of the_stable_subgroups_of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds
fs is composition_series
let G be GroupWithOperators of O; :: thesis: for s1 being CompositionSeries of G
for fs being FinSequence of the_stable_subgroups_of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds
fs is composition_series
let s1 be CompositionSeries of G; :: thesis: for fs being FinSequence of the_stable_subgroups_of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds
fs is composition_series
let fs be FinSequence of the_stable_subgroups_of G; :: thesis: for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds
fs is composition_series
let i be Nat; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) implies fs is composition_series )
assume A1: i in dom s1 ; :: thesis: ( not i + 1 in dom s1 or not s1 . i = s1 . (i + 1) or not fs = Del (s1,i) or fs is composition_series )
then consider k being Nat such that
A2: len s1 = k + 1 and
A3: len (Del (s1,i)) = k by FINSEQ_3:104;
assume i + 1 in dom s1 ; :: thesis: ( not s1 . i = s1 . (i + 1) or not fs = Del (s1,i) or fs is composition_series )
then i + 1 in Seg (len s1) by FINSEQ_1:def 3;
then A4: i + 1 <= len s1 by FINSEQ_1:1;
assume A5: s1 . i = s1 . (i + 1) ; :: thesis: ( not fs = Del (s1,i) or fs is composition_series )
assume A6: fs = Del (s1,i) ; :: thesis: fs is composition_series
A7: i in Seg (len s1) by A1, FINSEQ_1:def 3;
then A8: 1 <= i by FINSEQ_1:1;
then 1 + 1 <= i + 1 by XREAL_1:6;
then 1 + 1 <= (len fs) + 1 by A6, A4, A2, A3, XXREAL_0:2;
then A9: 1 <= len fs by XREAL_1:6;
per cases ( len fs = 1 or len fs > 1 ) by A9, XXREAL_0:1;
suppose A10: len fs = 1 ; :: thesis: fs is composition_series
A11: now :: thesis: for n being Nat st n in dom fs & n + 1 in dom fs holds
for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds
H2 is normal StableSubgroup of H1
let n be Nat; :: thesis: ( n in dom fs & n + 1 in dom fs implies for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds
H2 is normal StableSubgroup of H1 )
assume n in dom fs ; :: thesis: ( n + 1 in dom fs implies for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds
H2 is normal StableSubgroup of H1 )
then n in Seg 1 by A10, FINSEQ_1:def 3;
then A12: n = 1 by FINSEQ_1:2, TARSKI:def 1;
assume A13: n + 1 in dom fs ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds
H2 is normal StableSubgroup of H1
let H1, H2 be StableSubgroup of G; :: thesis: ( H1 = fs . n & H2 = fs . (n + 1) implies H2 is normal StableSubgroup of H1 )
assume that
H1 = fs . n and
H2 = fs . (n + 1) ; :: thesis: H2 is normal StableSubgroup of H1
2 in Seg 1 by A10, A12, A13, FINSEQ_1:def 3;
hence H2 is normal StableSubgroup of H1 by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum
end;
A14: s1 . 1 = (Omega). G by Def28;
A15: 1 <= i by A7, FINSEQ_1:1;
A16: i <= 1 by A6, A4, A2, A3, A10, XREAL_1:6;
then A17: i = 1 by A15, XXREAL_0:1;
dom s1 = Seg 2 by A6, A2, A3, A10, FINSEQ_1:def 3;
then 1 in dom s1 ;
then A18: i in dom s1 by A15, A16, XXREAL_0:1;
i <= 1 by A6, A4, A2, A3, A10, XREAL_1:6;
then A19: fs . (len fs) = s1 . (1 + 1) by A6, A2, A3, A10, A18, FINSEQ_3:111
.= (1). G by A6, A2, A3, A10, Def28 ;
s1 . 2 = (1). G by A6, A2, A3, A10, Def28;
hence fs is composition_series by A5, A10, A17, A14, A19, A11; :: thesis: verum
end;
suppose A20: len fs > 1 ; :: thesis: fs is composition_series
A21: fs . 1 = (Omega). G
proof
per cases ( i = 1 or i > 1 ) by A8, XXREAL_0:1;
suppose A22: i = 1 ; :: thesis: fs . 1 = (Omega). G
then fs . 1 = s1 . (1 + 1) by A1, A6, A2, A3, A20, FINSEQ_3:111;
hence fs . 1 = (Omega). G by A5, A22, Def28; :: thesis: verum
end;
suppose A23: i > 1 ; :: thesis: fs . 1 = (Omega). G
reconsider i = i as Element of NAT by INT_1:3;
fs . 1 = s1 . 1 by A23, A6, FINSEQ_3:110;
hence fs . 1 = (Omega). G by Def28; :: thesis: verum
end;
end;
end;
A24: now :: thesis: for n being Nat st n in dom fs & n + 1 in dom fs holds
for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds
H2 is normal StableSubgroup of H1
let n be Nat; :: thesis: ( n in dom fs & n + 1 in dom fs implies for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds
b5 is normal StableSubgroup of b4 )
assume that
A25: n in dom fs and
A26: n + 1 in dom fs ; :: thesis: for H1, H2 being StableSubgroup of G st H1 = fs . n & H2 = fs . (n + 1) holds
b5 is normal StableSubgroup of b4
A27: n in Seg (len fs) by A25, FINSEQ_1:def 3;
then A28: n <= k by A6, A3, FINSEQ_1:1;
reconsider n1 = n + 1 as Nat ;
A29: n + 1 in Seg (len fs) by A26, FINSEQ_1:def 3;
then A30: n1 <= k by A6, A3, FINSEQ_1:1;
A31: 0 + (len fs) < 1 + (len fs) by XREAL_1:6;
then A32: Seg (len fs) c= Seg (len s1) by A6, A2, A3, FINSEQ_1:5;
then n in Seg (len s1) by A27;
then A33: n in dom s1 by FINSEQ_1:def 3;
n1 in Seg (len s1) by A29, A32;
then A34: n1 in dom s1 by FINSEQ_1:def 3;
n1 <= len fs by A29, FINSEQ_1:1;
then n1 < len s1 by A6, A2, A3, A31, XXREAL_0:2;
then n1 + 1 <= k + 1 by A2, NAT_1:13;
then Seg (n1 + 1) c= Seg (len s1) by A2, FINSEQ_1:5;
then A35: Seg (n1 + 1) c= dom s1 by FINSEQ_1:def 3;
A36: n1 + 1 in Seg (n1 + 1) by FINSEQ_1:4;
let H1, H2 be StableSubgroup of G; :: thesis: ( H1 = fs . n & H2 = fs . (n + 1) implies b3 is normal StableSubgroup of b2 )
assume A37: H1 = fs . n ; :: thesis: ( H2 = fs . (n + 1) implies b3 is normal StableSubgroup of b2 )
assume A38: H2 = fs . (n + 1) ; :: thesis: b3 is normal StableSubgroup of b2
reconsider i = i, n = n as Nat ;
per cases ( n < i or n >= i ) ;
suppose A39: n < i ; :: thesis: b3 is normal StableSubgroup of b2
then A40: n1 <= i by NAT_1:13;
reconsider n9 = n, i = i as Element of NAT by INT_1:3;
A41: (Del (s1,i)) . n9 = s1 . n9 by A39, FINSEQ_3:110;
per cases ( n1 < i or n1 = i ) by A40, XXREAL_0:1;
suppose A42: n1 < i ; :: thesis: b3 is normal StableSubgroup of b2
reconsider n19 = n1, i = i as Element of NAT ;
(Del (s1,i)) . n19 = s1 . n19 by A42, FINSEQ_3:110;
hence H2 is normal StableSubgroup of H1 by A6, A37, A38, A33, A34, A41, Def28; :: thesis: verum
end;
suppose A43: n1 = i ; :: thesis: b3 is normal StableSubgroup of b2
then (Del (s1,i)) . n1 = s1 . (n1 + 1) by A1, A2, A30, FINSEQ_3:111;
hence H2 is normal StableSubgroup of H1 by A5, A6, A37, A38, A33, A34, A41, A43, Def28; :: thesis: verum
end;
end;
end;
suppose A44: n >= i ; :: thesis: b3 is normal StableSubgroup of b2
reconsider n9 = n, i = i as Element of NAT by INT_1:3;
A45: (Del (s1,i)) . n9 = s1 . (n9 + 1) by A1, A2, A28, A44, FINSEQ_3:111;
reconsider n19 = n1, i = i, k = k as Element of NAT by INT_1:3;
0 + n <= n + 1 by XREAL_1:6;
then A46: i <= n19 by A44, XXREAL_0:2;
n19 <= k by A6, A3, A29, FINSEQ_1:1;
then (Del (s1,i)) . n19 = s1 . (n19 + 1) by A1, A2, A46, FINSEQ_3:111;
hence H2 is normal StableSubgroup of H1 by A6, A37, A38, A34, A35, A36, A45, Def28; :: thesis: verum
end;
end;
end;
i <= len fs by A6, A4, A2, A3, XREAL_1:6;
then fs . (len fs) = s1 . (len s1) by A1, A6, A2, A3, FINSEQ_3:111;
then fs . (len fs) = (1). G by Def28;
hence fs is composition_series by A21, A24; :: thesis: verum
end;
end;