let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del s1,i holds
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del s1,i holds
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
let s1, s2 be CompositionSeries of G; :: thesis: for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del s1,i holds
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
let i be Nat; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del s1,i implies the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i )
assume A1:
i in dom s1
; :: thesis: ( not i + 1 in dom s1 or not s1 . i = s1 . (i + 1) or not s2 = Del s1,i or the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i )
assume A2:
i + 1 in dom s1
; :: thesis: ( not s1 . i = s1 . (i + 1) or not s2 = Del s1,i or the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i )
assume A3:
s1 . i = s1 . (i + 1)
; :: thesis: ( not s2 = Del s1,i or the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i )
assume A4:
s2 = Del s1,i
; :: thesis: the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
set f1 = the_series_of_quotients_of s1;
A5:
i in Seg (len s1)
by A1, FINSEQ_1:def 3;
then
( 1 <= i & i <= len s1 )
by FINSEQ_1:3;
then A6:
1 + 1 <= i + 1
by XREAL_1:8;
i + 1 in Seg (len s1)
by A2, FINSEQ_1:def 3;
then A7:
( 1 <= i + 1 & i + 1 <= len s1 )
by FINSEQ_1:3;
then A8:
2 <= len s1
by A6, XXREAL_0:2;
consider k being Nat such that
A9:
( len s1 = k + 1 & len (Del s1,i) = k )
by A1, FINSEQ_3:113;
A10:
1 < len s1
by A8, XXREAL_0:2;
then A11:
len s1 = (len (the_series_of_quotients_of s1)) + 1
by Def36;
1 + 1 <= (len s2) + 1
by A4, A6, A7, A9, XXREAL_0:2;
then A12:
1 <= len s2
by XREAL_1:8;
per cases
( len s2 = 1 or len s2 > 1 )
by A12, XXREAL_0:1;
suppose A13:
len s2 = 1
;
:: thesis: the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),ithen A14:
the_series_of_quotients_of s2 = {}
by Def36;
1
in Seg (len (the_series_of_quotients_of s1))
by A4, A9, A11, A13;
then
1
in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
then consider k1 being
Nat such that A15:
(
len (the_series_of_quotients_of s1) = k1 + 1 &
len (Del (the_series_of_quotients_of s1),1) = k1 )
by FINSEQ_3:113;
( 1
<= i &
i <= 1 )
by A4, A5, A7, A9, A13, FINSEQ_1:3, XREAL_1:8;
then
len (Del (the_series_of_quotients_of s1),i) = 0
by A4, A9, A11, A13, A15, XXREAL_0:1;
hence
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),
i
by A14;
:: thesis: verum end; suppose A16:
len s2 > 1
;
:: thesis: the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),i
(i + 1) - 1
<= (len s1) - 1
by A7, XREAL_1:11;
then
( 1
<= i &
i <= len (the_series_of_quotients_of s1) )
by A5, A11, FINSEQ_1:3;
then
i in Seg (len (the_series_of_quotients_of s1))
by FINSEQ_1:3;
then A17:
i in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
then consider k1 being
Nat such that A18:
(
len (the_series_of_quotients_of s1) = k1 + 1 &
len (Del (the_series_of_quotients_of s1),i) = k1 )
by FINSEQ_3:113;
now let n be
Nat;
:: thesis: ( n in dom (Del (the_series_of_quotients_of s1),i) implies for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del (the_series_of_quotients_of s1),i) . b3 = b4 ./. b5 )assume A19:
n in dom (Del (the_series_of_quotients_of s1),i)
;
:: thesis: for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del (the_series_of_quotients_of s1),i) . b3 = b4 ./. b5then A20:
n in Seg (len (Del (the_series_of_quotients_of s1),i))
by FINSEQ_1:def 3;
let H1 be
StableSubgroup of
G;
:: thesis: for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del (the_series_of_quotients_of s1),i) . b2 = b3 ./. b4let N1 be
normal StableSubgroup of
H1;
:: thesis: ( H1 = s2 . n & N1 = s2 . (n + 1) implies (Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3 )assume A21:
H1 = s2 . n
;
:: thesis: ( N1 = s2 . (n + 1) implies (Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3 )assume A22:
N1 = s2 . (n + 1)
;
:: thesis: (Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3
((len (the_series_of_quotients_of s1)) - (len (Del (the_series_of_quotients_of s1),i))) + (len (Del (the_series_of_quotients_of s1),i)) > 0 + (len (Del (the_series_of_quotients_of s1),i))
by A18, XREAL_1:8;
then
Seg (len (Del (the_series_of_quotients_of s1),i)) c= Seg (len (the_series_of_quotients_of s1))
by FINSEQ_1:7;
then
n in Seg (len (the_series_of_quotients_of s1))
by A20;
then A23:
n in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
A24:
( 1
<= n &
n <= len (Del (the_series_of_quotients_of s1),i) )
by A20, FINSEQ_1:3;
A25:
n <= k1
by A18, A20, FINSEQ_1:3;
set n1 =
n + 1;
A26:
n + 1
<= k
by A9, A11, A18, A25, XREAL_1:8;
0 + n < 1
+ n
by XREAL_1:8;
then A27:
n <= k
by A26, XXREAL_0:2;
1
+ 1
<= n + 1
by A24, XREAL_1:8;
then
1
<= n + 1
by XXREAL_0:2;
then
n + 1
in Seg (len (the_series_of_quotients_of s1))
by A9, A11, A26;
then A28:
n + 1
in dom (the_series_of_quotients_of s1)
by FINSEQ_1:def 3;
reconsider n1 =
n + 1 as
Nat ;
per cases
( n < i or n >= i )
;
suppose A29:
n < i
;
:: thesis: (Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3then A30:
n1 <= i
by NAT_1:13;
per cases
( n1 < i or n1 = i )
by A30, XXREAL_0:1;
suppose A31:
n1 < i
;
:: thesis: (Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3reconsider n' =
n as
Element of
NAT by INT_1:16;
(
s1 . n' = H1 &
s1 . (n' + 1) = N1 )
by A1, A4, A9, A21, A22, A29, A31, FINSEQ_3:119;
then
(the_series_of_quotients_of s1) . n = H1 ./. N1
by A10, A23, Def36;
hence
(Del (the_series_of_quotients_of s1),i) . n = H1 ./. N1
by A1, A18, A19, A29, FINSEQ_3:119;
:: thesis: verum end; suppose
n1 = i
;
:: thesis: (Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3then
(
s1 . n = H1 &
s1 . (n + 1) = N1 )
by A1, A3, A4, A9, A19, A21, A22, A26, A29, FINSEQ_3:119, FINSEQ_3:120;
then
(the_series_of_quotients_of s1) . n = H1 ./. N1
by A10, A23, Def36;
hence
(Del (the_series_of_quotients_of s1),i) . n = H1 ./. N1
by A1, A18, A19, A29, FINSEQ_3:119;
:: thesis: verum end; end; suppose A32:
n >= i
;
:: thesis: (Del (the_series_of_quotients_of s1),i) . b1 = b2 ./. b3A33:
0 + i < 1
+ i
by XREAL_1:8;
n + 1
>= i + 1
by A32, XREAL_1:8;
then A34:
n1 >= i
by A33, XXREAL_0:2;
reconsider n1' =
n1 as
Element of
NAT ;
(
s1 . n1' = H1 &
s1 . (n1' + 1) = N1 )
by A1, A4, A9, A19, A21, A22, A26, A27, A32, A34, FINSEQ_3:120;
then
(the_series_of_quotients_of s1) . n1 = H1 ./. N1
by A10, A28, Def36;
hence
(Del (the_series_of_quotients_of s1),i) . n = H1 ./. N1
by A17, A18, A19, A25, A32, FINSEQ_3:120;
:: thesis: verum end; end; hence
the_series_of_quotients_of s2 = Del (the_series_of_quotients_of s1),
i
by A4, A9, A11, A16, A18, Def36;
:: thesis: verum end;