let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
the_schreier_series_of (s1,s2) is_finer_than s1

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
the_schreier_series_of (s1,s2) is_finer_than s1

let s1, s2 be CompositionSeries of G; :: thesis: ( len s1 > 1 & len s2 > 1 implies the_schreier_series_of (s1,s2) is_finer_than s1 )
assume that
A1: len s1 > 1 and
A2: len s2 > 1 ; :: thesis: the_schreier_series_of (s1,s2) is_finer_than s1
now :: thesis: ex fX being Element of bool REAL st
( fX c= dom (the_schreier_series_of (s1,s2)) & s1 = (the_schreier_series_of (s1,s2)) * (Sgm fX) )
set rR = rng s1;
set R = s1;
set l = (((len s1) - 1) * ((len s2) - 1)) + 1;
set X = Seg (len s1);
set g = { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } ;
now :: thesis: for x being object st x in { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } holds
ex y, z being object st x = [y,z]
let x be object ; :: thesis: ( x in { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } implies ex y, z being object st x = [y,z] )
assume x in { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } ; :: thesis: ex y, z being object st x = [y,z]
then consider k being Element of NAT such that
A3: [k,(((k - 1) * ((len s2) - 1)) + 1)] = x and
1 <= k and
k <= len s1 ;
set z = ((k - 1) * ((len s2) - 1)) + 1;
set y = k;
reconsider y = k, z = ((k - 1) * ((len s2) - 1)) + 1 as object ;
take y = y; :: thesis: ex z being object st x = [y,z]
take z = z; :: thesis: x = [y,z]
thus x = [y,z] by A3; :: thesis: verum
end;
then reconsider g = { [k,(((k - 1) * ((len s2) - 1)) + 1)] where k is Element of NAT : ( 1 <= k & k <= len s1 ) } as Relation by RELAT_1:def 1;
A4: now :: thesis: for y being object st y in rng g holds
y in REAL
let y be object ; :: thesis: ( y in rng g implies y in REAL )
assume y in rng g ; :: thesis:
then consider x being object such that
A5: [x,y] in g by XTUPLE_0:def 13;
consider k being Element of NAT such that
A6: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] and
1 <= k and
k <= len s1 by A5;
((k - 1) * ((len s2) - 1)) + 1 = y by ;
hence y in REAL by XREAL_0:def 1; :: thesis: verum
end;
A7: now :: thesis: for x, y1, y2 being object st [x,y1] in g & [x,y2] in g holds
y1 = y2
let x, y1, y2 be object ; :: thesis: ( [x,y1] in g & [x,y2] in g implies y1 = y2 )
assume [x,y1] in g ; :: thesis: ( [x,y2] in g implies y1 = y2 )
then consider k being Element of NAT such that
A8: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y1] and
1 <= k and
k <= len s1 ;
A9: k = x by ;
assume [x,y2] in g ; :: thesis: y1 = y2
then consider k9 being Element of NAT such that
A10: [k9,(((k9 - 1) * ((len s2) - 1)) + 1)] = [x,y2] and
1 <= k9 and
k9 <= len s1 ;
k9 = x by ;
hence y1 = y2 by ; :: thesis: verum
end;
now :: thesis: for x being object st x in dom g holds
x in NAT
let x be object ; :: thesis: ( x in dom g implies x in NAT )
assume x in dom g ; :: thesis:
then consider y being object such that
A11: [x,y] in g by XTUPLE_0:def 12;
consider k being Element of NAT such that
A12: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] and
1 <= k and
k <= len s1 by A11;
k = x by ;
hence x in NAT ; :: thesis: verum
end;
then A13: dom g c= NAT ;
reconsider g = g as Function by ;
A14: rng g c= REAL by A4;
reconsider f = g as PartFunc of (dom g),(rng g) by RELSET_1:4;
dom g c= REAL by ;
then reconsider f = f as PartFunc of REAL,REAL by ;
set dR = dom s1;
set t = the_schreier_series_of (s1,s2);
set fX = f .: (Seg (len s1));
take fX = f .: (Seg (len s1)); :: thesis: ( fX c= dom (the_schreier_series_of (s1,s2)) & s1 = (the_schreier_series_of (s1,s2)) * (Sgm fX) )
reconsider R = s1 as Relation of (dom s1),(rng s1) by FUNCT_2:1;
A15: (id (dom s1)) * R = R by FUNCT_2:17;
(len s2) + 1 > 1 + 1 by ;
then len s2 >= 2 by NAT_1:13;
then A16: (len s2) - 1 >= 2 - 1 by XREAL_1:9;
(len s1) + 1 > 1 + 1 by ;
then len s1 >= 2 by NAT_1:13;
then (len s1) - 1 >= 2 - 1 by XREAL_1:9;
then reconsider l = (((len s1) - 1) * ((len s2) - 1)) + 1 as Element of NAT by ;
A17: len (the_schreier_series_of (s1,s2)) = l by ;
then A18: dom (the_schreier_series_of (s1,s2)) = Seg l by FINSEQ_1:def 3;
(len s2) + 1 > 1 + 1 by ;
then len s2 >= 2 by NAT_1:13;
then A19: (len s2) - 1 >= 2 - 1 by XREAL_1:9;
now :: thesis: for y being object st y in fX holds
y in Seg l
let y be object ; :: thesis: ( y in fX implies y in Seg l )
assume y in fX ; :: thesis: y in Seg l
then consider x being object such that
A20: [x,y] in g and
x in Seg (len s1) by RELAT_1:def 13;
consider k being Element of NAT such that
A21: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] and
A22: 1 <= k and
A23: k <= len s1 by A20;
reconsider y9 = y as Integer by ;
A24: k - 1 >= 1 - 1 by ;
then A25: y9 > 0 by ;
k - 1 <= (len s1) - 1 by ;
then A26: (k - 1) * ((len s2) - 1) <= ((len s1) - 1) * ((len s2) - 1) by ;
((k - 1) * ((len s2) - 1)) + 1 >= 0 + 1 by ;
then A27: y9 >= 1 by ;
reconsider y9 = y9 as Element of NAT by ;
((k - 1) * ((len s2) - 1)) + 1 = y by ;
then y9 <= l by ;
hence y in Seg l by A27; :: thesis: verum
end;
then A28: fX c= Seg l ;
hence fX c= dom (the_schreier_series_of (s1,s2)) by ; :: thesis: s1 = (the_schreier_series_of (s1,s2)) * (Sgm fX)
now :: thesis: for x being object st x in Seg (len s1) holds
x in dom f
let x be object ; :: thesis: ( x in Seg (len s1) implies x in dom f )
assume A29: x in Seg (len s1) ; :: thesis: x in dom f
then reconsider k = x as Element of NAT ;
set y = ((k - 1) * ((len s2) - 1)) + 1;
( 1 <= k & k <= len s1 ) by ;
then [x,(((k - 1) * ((len s2) - 1)) + 1)] in f ;
hence x in dom f by XTUPLE_0:def 12; :: thesis: verum
end;
then A30: Seg (len s1) c= dom f ;
then A31: dom s1 c= dom f by FINSEQ_1:def 3;
now :: thesis: for x being object st x in dom f holds
x in dom s1
let x be object ; :: thesis: ( x in dom f implies x in dom s1 )
assume x in dom f ; :: thesis: x in dom s1
then consider y being object such that
A32: [x,y] in f by XTUPLE_0:def 12;
consider k being Element of NAT such that
A33: ( [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] & 1 <= k & k <= len s1 ) by A32;
( k in Seg (len s1) & k = x ) by ;
hence x in dom s1 by FINSEQ_1:def 3; :: thesis: verum
end;
then dom f c= dom s1 ;
then A34: dom s1 = dom f by ;
then Seg (len s1) = dom f by FINSEQ_1:def 3;
then A35: rng f c= Seg l by ;
then A36: dom s1 = dom ((the_schreier_series_of (s1,s2)) * f) by ;
A37: now :: thesis: for x being object st x in dom s1 holds
s1 . x = ((the_schreier_series_of (s1,s2)) * f) . x
let x be object ; :: thesis: ( x in dom s1 implies s1 . b1 = ((the_schreier_series_of (s1,s2)) * f) . b1 )
assume A38: x in dom s1 ; :: thesis: s1 . b1 = ((the_schreier_series_of (s1,s2)) * f) . b1
then [x,(f . x)] in f by ;
then consider i being Element of NAT such that
A39: [i,(((i - 1) * ((len s2) - 1)) + 1)] = [x,(f . x)] and
A40: 1 <= i and
A41: i <= len s1 ;
set k = ((i - 1) * ((len s2) - 1)) + 1;
((i - 1) * ((len s2) - 1)) + 1 = f . x by ;
then ((i - 1) * ((len s2) - 1)) + 1 in rng f by ;
then ((i - 1) * ((len s2) - 1)) + 1 in Seg l by A35;
then reconsider k = ((i - 1) * ((len s2) - 1)) + 1 as Element of NAT ;
A42: x in dom ((the_schreier_series_of (s1,s2)) * f) by ;
per cases ( i = len s1 or i <> len s1 ) ;
suppose A43: i = len s1 ; :: thesis: s1 . b1 = ((the_schreier_series_of (s1,s2)) * f) . b1
((the_schreier_series_of (s1,s2)) * f) . x = (the_schreier_series_of (s1,s2)) . (f . x) by
.= (the_schreier_series_of (s1,s2)) . k by
.= (1). G by A1, A2, A43, Def35
.= s1 . (len s1) by Def28 ;
hence s1 . x = ((the_schreier_series_of (s1,s2)) * f) . x by ; :: thesis: verum
end;
suppose i <> len s1 ; :: thesis: s1 . b1 = ((the_schreier_series_of (s1,s2)) * f) . b1
then i < len s1 by ;
then A44: i + 1 <= len s1 by NAT_1:13;
then A45: (i + 1) - 1 <= (len s1) - 1 by XREAL_1:9;
A46: s2 . 1 = (Omega). G by Def28;
then reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . 1 as strict StableSubgroup of G by ;
now :: thesis: for x being object st x in the carrier of H2 holds
x in the carrier of ()
let x be object ; :: thesis: ( x in the carrier of H2 implies x in the carrier of () )
H2 is Subgroup of G by Def7;
then A47: the carrier of H2 c= the carrier of G by GROUP_2:def 5;
assume x in the carrier of H2 ; :: thesis: x in the carrier of ()
hence x in the carrier of () by A47; :: thesis: verum
end;
then the carrier of H2 c= the carrier of () ;
then A48: the carrier of H2 = the carrier of H2 /\ the carrier of H3 by ;
(len s2) - 1 > 1 - 1 by ;
then A49: (len s2) - 1 >= 0 + 1 by INT_1:7;
0 + i <= 1 + i by XREAL_1:6;
then 1 <= i + 1 by ;
then i + 1 in Seg (len s1) by A44;
then A50: i + 1 in dom s1 by FINSEQ_1:def 3;
i in Seg (len s1) by ;
then i in dom s1 by FINSEQ_1:def 3;
then A51: H1 is normal StableSubgroup of H2 by ;
((the_schreier_series_of (s1,s2)) * f) . x = (the_schreier_series_of (s1,s2)) . (f . x) by
.= (the_schreier_series_of (s1,s2)) . k by
.= H1 "\/" (H2 /\ H3) by A1, A2, A40, A45, A49, Def35
.= H1 "\/" H2 by
.= H2 by ;
hence s1 . x = ((the_schreier_series_of (s1,s2)) * f) . x by ; :: thesis: verum
end;
end;
end;
now :: thesis: for r1, r2 being Real st r1 in (Seg (len s1)) /\ (dom f) & r2 in (Seg (len s1)) /\ (dom f) & r1 < r2 holds
f . r1 < f . r2
let r1, r2 be Real; :: thesis: ( r1 in (Seg (len s1)) /\ (dom f) & r2 in (Seg (len s1)) /\ (dom f) & r1 < r2 implies f . r1 < f . r2 )
assume r1 in (Seg (len s1)) /\ (dom f) ; :: thesis: ( r2 in (Seg (len s1)) /\ (dom f) & r1 < r2 implies f . r1 < f . r2 )
then r1 in dom f by XBOOLE_0:def 4;
then [r1,(f . r1)] in f by FUNCT_1:1;
then consider k9 being Element of NAT such that
A52: [k9,(((k9 - 1) * ((len s2) - 1)) + 1)] = [r1,(f . r1)] and
1 <= k9 and
k9 <= len s1 ;
assume r2 in (Seg (len s1)) /\ (dom f) ; :: thesis: ( r1 < r2 implies f . r1 < f . r2 )
then r2 in dom f by XBOOLE_0:def 4;
then [r2,(f . r2)] in f by FUNCT_1:1;
then consider k99 being Element of NAT such that
A53: [k99,(((k99 - 1) * ((len s2) - 1)) + 1)] = [r2,(f . r2)] and
1 <= k99 and
k99 <= len s1 ;
A54: k99 = r2 by ;
assume A55: r1 < r2 ; :: thesis: f . r1 < f . r2
k9 = r1 by ;
then k9 - 1 < k99 - 1 by ;
then A56: (k9 - 1) * ((len s2) - 1) < (k99 - 1) * ((len s2) - 1) by ;
A57: ((k99 - 1) * ((len s2) - 1)) + 1 = f . r2 by ;
((k9 - 1) * ((len s2) - 1)) + 1 = f . r1 by ;
hence f . r1 < f . r2 by ; :: thesis: verum
end;
then A58: f | (Seg (len s1)) is increasing by RFUNCT_2:20;
now :: thesis: for y being object st y in f .: (Seg (len s1)) holds
y in NAT \
let y be object ; :: thesis: ( y in f .: (Seg (len s1)) implies y in NAT \ )
assume y in f .: (Seg (len s1)) ; :: thesis:
then consider x being object such that
A59: [x,y] in g and
x in Seg (len s1) by RELAT_1:def 13;
consider k being Element of NAT such that
A60: [k,(((k - 1) * ((len s2) - 1)) + 1)] = [x,y] and
A61: 1 <= k and
k <= len s1 by A59;
reconsider y9 = y as Integer by ;
( ((k - 1) * ((len s2) - 1)) + 1 = y & k - 1 >= 1 - 1 ) by ;
then ( y9 in NAT & not y in ) by ;
hence y in NAT \ by XBOOLE_0:def 5; :: thesis: verum
end;
then f .: (Seg (len s1)) c= NAT \ ;
then (the_schreier_series_of (s1,s2)) * (Sgm fX) = (the_schreier_series_of (s1,s2)) * (f * (Sgm (Seg (len s1)))) by
.= ((the_schreier_series_of (s1,s2)) * f) * (Sgm (Seg (len s1))) by RELAT_1:36
.= s1 * (Sgm (Seg (len s1))) by
.= s1 * (idseq (len s1)) by FINSEQ_3:48
.= s1 * (id (Seg (len s1))) by FINSEQ_2:def 1
.= s1 * (id (dom s1)) by FINSEQ_1:def 3 ;
hence s1 = (the_schreier_series_of (s1,s2)) * (Sgm fX) by A15; :: thesis: verum
end;
hence the_schreier_series_of (s1,s2) is_finer_than s1 ; :: thesis: verum