let V be RealLinearSpace; :: thesis: for L1, L2 being Convex_Combination of V
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of V
let L1, L2 be Convex_Combination of V; :: thesis: for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of V
let r be Real; :: thesis: ( 0 < r & r < 1 implies (r * L1) + ((1 - r) * L2) is Convex_Combination of V )
assume that
A1: 0 < r and
A2: r < 1 ; :: thesis: (r * L1) + ((1 - r) * L2) is Convex_Combination of V
A3: Carrier (r * L1) = Carrier L1 by A1, RLVECT_2:42;
set Mid = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2));
set L = (r * L1) + ((1 - r) * L2);
consider F2 being FinSequence of the carrier of V such that
A4: F2 is one-to-one and
A5: rng F2 = Carrier L2 and
A6: ex f being FinSequence of REAL st
( len f = len F2 & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L2 . (F2 . n) & f . n >= 0 ) ) ) by CONVEX1:def 3;
set Btm = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1));
set Top = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2));
consider F1 being FinSequence of the carrier of V such that
A7: F1 is one-to-one and
A8: rng F1 = Carrier L1 and
A9: ex f being FinSequence of REAL st
( len f = len F1 & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L1 . (F1 . n) & f . n >= 0 ) ) ) by CONVEX1:def 3;
consider Lt being Linear_Combination of V such that
A10: Carrier Lt = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:36;
A11: r - r < 1 - r by A2, XREAL_1:9;
then A12: Carrier ((1 - r) * L2) = Carrier L2 by RLVECT_2:42;
A13: r * (1 - r) > 0 by A1, A11, XREAL_1:129;
then A14: Carrier ((r * L1) + ((1 - r) * L2)) = (Carrier (r * L1)) \/ (Carrier ((1 - r) * L2)) by Lm5;
then consider Lm being Linear_Combination of V such that
A15: Carrier Lm = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:29;
consider Lb being Linear_Combination of V such that
A16: Carrier Lb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1)) by Lm7, XBOOLE_1:36;
consider Ft being FinSequence of the carrier of V such that
A17: Ft is one-to-one and
A18: rng Ft = Carrier Lt and
Sum Lt = Sum (Lt (#) Ft) by RLVECT_2:def 8;
consider Fb being FinSequence of the carrier of V such that
A19: Fb is one-to-one and
A20: rng Fb = Carrier Lb and
Sum Lb = Sum (Lb (#) Fb) by RLVECT_2:def 8;
consider Fm being FinSequence of the carrier of V such that
A21: Fm is one-to-one and
A22: rng Fm = Carrier Lm and
Sum Lm = Sum (Lm (#) Fm) by RLVECT_2:def 8;
A23: rng (Ft ^ Fm) = (rng Ft) \/ (rng Fm) by FINSEQ_1:31
.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L2)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, A10, A15, A18, A22, Lm5
.= (((Carrier L1) \ (Carrier L2)) \/ ((Carrier L2) \ (Carrier L2))) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:42
.= (((Carrier L1) \ (Carrier L2)) \/ {}) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:37
.= (Carrier L1) \ ((Carrier L2) \ (Carrier L2)) by XBOOLE_1:52
.= (Carrier L1) \ {} by XBOOLE_1:37
.= rng F1 by A8 ;
A24: rng Ft misses rng Fm by A10, A15, A18, A22, XBOOLE_1:17, XBOOLE_1:85;
then A25: Ft ^ Fm is one-to-one by A17, A21, FINSEQ_3:91;
set F = (Ft ^ Fm) ^ Fb;
consider f2 being FinSequence of REAL such that
A26: len f2 = len F2 and
A27: Sum f2 = 1 and
A28: for n being Nat st n in dom f2 holds
( f2 . n = L2 . (F2 . n) & f2 . n >= 0 ) by A6;
deffunc H1( set ) -> set = L1 . (Ft . $1);
consider ft being FinSequence such that
A29: ( len ft = len Ft & ( for j being Nat st j in dom ft holds
ft . j = H1(j) ) ) from FINSEQ_1:sch 2();
 rng ft c= REAL
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ft or y in REAL )
consider L1f being Function such that
A30: L1 = L1f and
A31: dom L1f = the carrier of V and
A32: rng L1f c= REAL by FUNCT_2:def 2;
assume y in rng ft ; :: thesis: y in REAL
then consider x being object such that
A33: x in dom ft and
A34: ft . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A33;
A35: ft . x = L1 . (Ft . x) by A29, A33;
x in Seg (len Ft) by A29, A33, FINSEQ_1:def 3;
then x in dom Ft by FINSEQ_1:def 3;
then A36: Ft . x in rng Ft by FUNCT_1:3;
rng Ft c= the carrier of V by FINSEQ_1:def 4;
then reconsider Ftx = Ft . x as Element of V by A36;
Ftx in dom L1f by A31;
then ft . x in rng L1f by A35, A30, FUNCT_1:3;
hence y in REAL by A34, A32; :: thesis: verum
end;
then reconsider ft = ft as FinSequence of REAL by FINSEQ_1:def 4;
deffunc H2( set ) -> set = L1 . (Fm . $1);
consider fm1 being FinSequence such that
A37: ( len fm1 = len Fm & ( for j being Nat st j in dom fm1 holds
fm1 . j = H2(j) ) ) from FINSEQ_1:sch 2();
 rng fm1 c= REAL
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng fm1 or y in REAL )
consider L1f being Function such that
A38: L1 = L1f and
A39: dom L1f = the carrier of V and
A40: rng L1f c= REAL by FUNCT_2:def 2;
assume y in rng fm1 ; :: thesis: y in REAL
then consider x being object such that
A41: x in dom fm1 and
A42: fm1 . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A41;
A43: fm1 . x = L1 . (Fm . x) by A37, A41;
x in Seg (len Fm) by A37, A41, FINSEQ_1:def 3;
then x in dom Fm by FINSEQ_1:def 3;
then A44: Fm . x in rng Fm by FUNCT_1:3;
rng Fm c= the carrier of V by FINSEQ_1:def 4;
then reconsider Fmx = Fm . x as Element of V by A44;
Fmx in dom L1f by A39;
then fm1 . x in rng L1f by A43, A38, FUNCT_1:3;
hence y in REAL by A42, A40; :: thesis: verum
end;
then reconsider fm1 = fm1 as FinSequence of REAL by FINSEQ_1:def 4;
deffunc H3( set ) -> set = L2 . (Fm . $1);
consider fm2 being FinSequence such that
A45: ( len fm2 = len Fm & ( for j being Nat st j in dom fm2 holds
fm2 . j = H3(j) ) ) from FINSEQ_1:sch 2();
 A46: for x being object st x in dom (ft ^ fm1) holds
(ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
proof
let x be object ; :: thesis: ( x in dom (ft ^ fm1) implies (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) )
assume A47: x in dom (ft ^ fm1) ; :: thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
then reconsider n = x as Element of NAT ;
now :: thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
per cases ( n in dom ft or ex m being Nat st
( m in dom fm1 & n = (len ft) + m ) ) by A47, FINSEQ_1:25;
suppose A48: n in dom ft ; :: thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
then n in Seg (len Ft) by A29, FINSEQ_1:def 3;
then A49: n in dom Ft by FINSEQ_1:def 3;
ft . n = L1 . (Ft . n) by A29, A48;
then (ft ^ fm1) . n = L1 . (Ft . n) by A48, FINSEQ_1:def 7;
hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A49, FINSEQ_1:def 7; :: thesis: verum
end;
suppose ex m being Nat st
( m in dom fm1 & n = (len ft) + m ) ; :: thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
then consider m being Element of NAT such that
A50: m in dom fm1 and
A51: n = (len ft) + m ;
m in Seg (len Fm) by A37, A50, FINSEQ_1:def 3;
then A52: m in dom Fm by FINSEQ_1:def 3;
(ft ^ fm1) . n = fm1 . m by A50, A51, FINSEQ_1:def 7
.= L1 . (Fm . m) by A37, A50 ;
hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A29, A51, A52, FINSEQ_1:def 7; :: thesis: verum
end;
end;
end;
hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) ; :: thesis: verum
end;
for x being object holds
( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) )
proof
let x be object ; :: thesis: ( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) )
A53: len (ft ^ fm1) = (len ft) + (len fm1) by FINSEQ_1:22
.= len (Ft ^ Fm) by A29, A37, FINSEQ_1:22 ;
A54: dom (ft ^ fm1) = Seg (len (ft ^ fm1)) by FINSEQ_1:def 3
.= dom (Ft ^ Fm) by A53, FINSEQ_1:def 3 ;
( x in dom (ft ^ fm1) implies (Ft ^ Fm) . x in dom L1 )
proof
assume x in dom (ft ^ fm1) ; :: thesis: (Ft ^ Fm) . x in dom L1
then (Ft ^ Fm) . x in rng (Ft ^ Fm) by A54, FUNCT_1:3;
then A55: (Ft ^ Fm) . x in (Carrier Lt) \/ (Carrier Lm) by A18, A22, FINSEQ_1:31;
dom L1 = the carrier of V by FUNCT_2:92;
hence (Ft ^ Fm) . x in dom L1 by A55; :: thesis: verum
end;
hence ( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) ) by A54; :: thesis: verum
end;
then A56: ft ^ fm1 = L1 * (Ft ^ Fm) by A46, FUNCT_1:10;
A57: dom L2 = the carrier of V by FUNCT_2:92;
A58: for x being object holds
( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) )
proof
let x be object ; :: thesis: ( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) )
A59: now :: thesis: ( x in dom f2 implies ( x in dom F2 & F2 . x in dom L2 ) )
assume x in dom f2 ; :: thesis: ( x in dom F2 & F2 . x in dom L2 )
then x in Seg (len F2) by A26, FINSEQ_1:def 3;
hence x in dom F2 by FINSEQ_1:def 3; :: thesis: F2 . x in dom L2
then F2 . x in rng F2 by FUNCT_1:3;
hence F2 . x in dom L2 by A5, A57; :: thesis: verum
end;
now :: thesis: ( x in dom F2 & F2 . x in dom L2 implies x in dom f2 )
assume that
A60: x in dom F2 and
F2 . x in dom L2 ; :: thesis: x in dom f2
x in Seg (len F2) by A60, FINSEQ_1:def 3;
hence x in dom f2 by A26, FINSEQ_1:def 3; :: thesis: verum
end;
hence ( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) ) by A59; :: thesis: verum
end;
deffunc H4( set ) -> set = L2 . (Fb . $1);
consider fb being FinSequence such that
A61: ( len fb = len Fb & ( for j being Nat st j in dom fb holds
fb . j = H4(j) ) ) from FINSEQ_1:sch 2();
 rng fm2 c= REAL
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng fm2 or y in REAL )
consider L2f being Function such that
A62: L2 = L2f and
A63: dom L2f = the carrier of V and
A64: rng L2f c= REAL by FUNCT_2:def 2;
assume y in rng fm2 ; :: thesis: y in REAL
then consider x being object such that
A65: x in dom fm2 and
A66: fm2 . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A65;
A67: fm2 . x = L2 . (Fm . x) by A45, A65;
x in Seg (len Fm) by A45, A65, FINSEQ_1:def 3;
then x in dom Fm by FINSEQ_1:def 3;
then A68: Fm . x in rng Fm by FUNCT_1:3;
rng Fm c= the carrier of V by FINSEQ_1:def 4;
then reconsider Fmx = Fm . x as Element of V by A68;
Fmx in dom L2f by A63;
then fm2 . x in rng L2f by A67, A62, FUNCT_1:3;
hence y in REAL by A66, A64; :: thesis: verum
end;
then reconsider fm2 = fm2 as FinSequence of REAL by FINSEQ_1:def 4;
A69: len (r * fm1) = len fm1 by RVSUM_1:117
.= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ;
rng fb c= REAL
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng fb or y in REAL )
consider L2f being Function such that
A70: L2 = L2f and
A71: dom L2f = the carrier of V and
A72: rng L2f c= REAL by FUNCT_2:def 2;
assume y in rng fb ; :: thesis: y in REAL
then consider x being object such that
A73: x in dom fb and
A74: fb . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A73;
A75: fb . x = L2 . (Fb . x) by A61, A73;
x in Seg (len Fb) by A61, A73, FINSEQ_1:def 3;
then x in dom Fb by FINSEQ_1:def 3;
then A76: Fb . x in rng Fb by FUNCT_1:3;
rng Fb c= the carrier of V by FINSEQ_1:def 4;
then reconsider Fbx = Fb . x as Element of V by A76;
Fbx in dom L2f by A71;
then fb . x in rng L2f by A75, A70, FUNCT_1:3;
hence y in REAL by A74, A72; :: thesis: verum
end;
then reconsider fb = fb as FinSequence of REAL by FINSEQ_1:def 4;
set f = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb);
consider f1 being FinSequence of REAL such that
A77: len f1 = len F1 and
A78: Sum f1 = 1 and
A79: for n being Nat st n in dom f1 holds
( f1 . n = L1 . (F1 . n) & f1 . n >= 0 ) by A9;
len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:22
.= ((len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:22
.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by RVSUM_1:117
.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len fb) by RVSUM_1:117
.= ((len ft) + (len (r * fm1))) + (len fb) by A69, INTEGRA5:2
.= ((len Ft) + (len Fm)) + (len Fb) by A29, A37, A61, RVSUM_1:117
.= (len (Ft ^ Fm)) + (len Fb) by FINSEQ_1:22 ;
then A80: len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = len ((Ft ^ Fm) ^ Fb) by FINSEQ_1:22;
A81: dom L1 = the carrier of V by FUNCT_2:92;
A82: for x being object holds
( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) )
proof
let x be object ; :: thesis: ( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) )
A83: now :: thesis: ( x in dom f1 implies ( x in dom F1 & F1 . x in dom L1 ) )
assume x in dom f1 ; :: thesis: ( x in dom F1 & F1 . x in dom L1 )
then x in Seg (len F1) by A77, FINSEQ_1:def 3;
hence x in dom F1 by FINSEQ_1:def 3; :: thesis: F1 . x in dom L1
then F1 . x in rng F1 by FUNCT_1:3;
hence F1 . x in dom L1 by A8, A81; :: thesis: verum
end;
now :: thesis: ( x in dom F1 & F1 . x in dom L1 implies x in dom f1 )
assume that
A84: x in dom F1 and
F1 . x in dom L1 ; :: thesis: x in dom f1
x in Seg (len F1) by A84, FINSEQ_1:def 3;
hence x in dom f1 by A77, FINSEQ_1:def 3; :: thesis: verum
end;
hence ( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) ) by A83; :: thesis: verum
end;
A85: rng (Ft ^ Fm) = (Carrier Lt) \/ (Carrier Lm) by A18, A22, FINSEQ_1:31;
for x being object st x in dom f1 holds
f1 . x = L1 . (F1 . x) by A79;
then A86: f1 = L1 * F1 by A82, FUNCT_1:10;
Ft ^ Fm is one-to-one by A17, A21, A24, FINSEQ_3:91;
then A87: F1,Ft ^ Fm are_fiberwise_equipotent by A7, A23, RFINSEQ:26;
then dom F1 = dom (Ft ^ Fm) by RFINSEQ:3;
then A88: Sum f1 = Sum (ft ^ fm1) by A8, A87, A81, A86, A85, A56, CLASSES1:83, RFINSEQ:9;
A89: rng (Fm ^ Fb) = (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31;
for x being object st x in dom f2 holds
f2 . x = L2 . (F2 . x) by A28;
then A90: f2 = L2 * F2 by A58, FUNCT_1:10;
A91: rng (Fm ^ Fb) = ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1))) \/ ((Carrier (r * L1)) /\ (Carrier ((1 - r) * L2))) by A15, A16, A22, A20, FINSEQ_1:31
.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L1)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, Lm5
.= (((Carrier L1) \ (Carrier L1)) \/ ((Carrier L2) \ (Carrier L1))) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:42
.= (((Carrier L2) \ (Carrier L1)) \/ {}) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:37
.= (Carrier L2) \ ((Carrier L1) \ (Carrier L1)) by XBOOLE_1:52
.= (Carrier L2) \ {} by XBOOLE_1:37
.= rng F2 by A5 ;
for n being Element of NAT st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds
( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
proof
let n be Element of NAT ; :: thesis: ( n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) implies ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) )
assume A92: n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) ; :: thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
now :: thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
per cases ( n in dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) or ex m being Nat st
( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ) by A92, FINSEQ_1:25;
suppose A93: n in dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ; :: thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
then A94: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) . n by FINSEQ_1:def 7;
now :: thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
per cases ( n in dom (r * ft) or ex k being Nat st
( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ) by A93, FINSEQ_1:25;
suppose A95: n in dom (r * ft) ; :: thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22
.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117
.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2
.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117
.= len (Ft ^ Fm) by FINSEQ_1:22 ;
then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def 3;
then n in dom (Ft ^ Fm) by FINSEQ_1:def 3;
then A96: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def 7;
A97: n in dom ft by A95, VALUED_1:def 5;
then n in Seg (len Ft) by A29, FINSEQ_1:def 3;
then A98: n in dom Ft by FINSEQ_1:def 3;
then A99: Ft . n in Carrier Lt by A18, FUNCT_1:3;
then reconsider Ftn = Ft . n as Element of V ;
A100: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = (r * ft) . n by A94, A95, FINSEQ_1:def 7
.= r * (ft . n) by RVSUM_1:44
.= r * (L1 . (Ft . n)) by A29, A97 ;
not Ft . n in Carrier L2 by A12, A10, A99, XBOOLE_0:def 5;
then L2 . Ftn = 0 by RLVECT_2:19;
then (1 - r) * (L2 . Ftn) = 0 ;
then ((1 - r) * L2) . Ftn = 0 by RLVECT_2:def 11;
then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Ftn) + (((1 - r) * L2) . Ftn) by A100, RLVECT_2:def 11
.= ((r * L1) + ((1 - r) * L2)) . (Ft . n) by RLVECT_2:def 10 ;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A98, A96, FINSEQ_1:def 7; :: thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0
A101: rng Ft c= rng (Ft ^ Fm) by FINSEQ_1:29;
Ft . n in rng Ft by A98, FUNCT_1:3;
then consider m9 being object such that
A102: m9 in dom F1 and
A103: F1 . m9 = Ft . n by A23, A101, FUNCT_1:def 3;
reconsider m9 = m9 as Element of NAT by A102;
m9 in Seg (len f1) by A77, A102, FINSEQ_1:def 3;
then m9 in dom f1 by FINSEQ_1:def 3;
then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A1, A100, A103; :: thesis: verum
end;
suppose ex k being Nat st
( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ; :: thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
then consider m being Element of NAT such that
A104: m in dom ((r * fm1) + ((1 - r) * fm2)) and
A105: n = (len (r * ft)) + m ;
len (r * fm1) = len fm1 by RVSUM_1:117
.= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ;
then A106: len ((r * fm1) + ((1 - r) * fm2)) = len (r * fm1) by INTEGRA5:2
.= len fm1 by RVSUM_1:117 ;
then A107: m in dom Fm by A37, A104, FINSEQ_3:29;
then A108: Fm . m in rng Fm by FUNCT_1:3;
then reconsider Fmm = Fm . m as Element of V by A22;
A109: m in dom fm1 by A104, A106, FINSEQ_3:29;
A110: m in dom fm2 by A37, A45, A104, A106, FINSEQ_3:29;
A111: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * fm1) + ((1 - r) * fm2)) . m by A94, A104, A105, FINSEQ_1:def 7
.= ((r * fm1) . m) + (((1 - r) * fm2) . m) by A104, VALUED_1:def 1
.= (r * (fm1 . m)) + (((1 - r) * fm2) . m) by RVSUM_1:44
.= (r * (fm1 . m)) + ((1 - r) * (fm2 . m)) by RVSUM_1:44
.= (r * (L1 . (Fm . m))) + ((1 - r) * (fm2 . m)) by A37, A109
.= (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) by A45, A110 ;
len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22
.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117
.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2
.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117
.= len (Ft ^ Fm) by FINSEQ_1:22 ;
then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def 3;
then n in dom (Ft ^ Fm) by FINSEQ_1:def 3;
then A112: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def 7;
A113: len (r * ft) = len Ft by A29, RVSUM_1:117;
( r * (L1 . Fmm) = (r * L1) . (Fm . m) & (1 - r) * (L2 . Fmm) = ((1 - r) * L2) . (Fm . m) ) by RLVECT_2:def 11;
then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (Fm . m) by A111, RLVECT_2:def 10;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A105, A107, A112, A113, FINSEQ_1:def 7; :: thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0
rng Fm c= rng (Ft ^ Fm) by FINSEQ_1:30;
then consider m9 being object such that
A114: m9 in dom F1 and
A115: F1 . m9 = Fm . m by A23, A108, FUNCT_1:def 3;
reconsider m9 = m9 as Element of NAT by A114;
m9 in Seg (len F1) by A114, FINSEQ_1:def 3;
then m9 in dom f1 by A77, FINSEQ_1:def 3;
then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79;
then A116: r * (L1 . (Fm . m)) >= 0 by A1, A115;
rng Fm c= rng (Fm ^ Fb) by FINSEQ_1:29;
then consider m9 being object such that
A117: m9 in dom F2 and
A118: F2 . m9 = Fm . m by A91, A108, FUNCT_1:def 3;
reconsider m9 = m9 as Element of NAT by A117;
m9 in Seg (len F2) by A117, FINSEQ_1:def 3;
then m9 in dom f2 by A26, FINSEQ_1:def 3;
then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28;
then (1 - r) * (L2 . (Fm . m)) >= 0 by A11, A118;
then (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) >= 0 + 0 by A116;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A111; :: thesis: verum
end;
end;
end;
hence ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ; :: thesis: verum
end;
suppose ex m being Nat st
( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ; :: thesis: ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )
then consider m being Element of NAT such that
A119: m in dom ((1 - r) * fb) and
A120: n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ;
A121: m in dom fb by A119, VALUED_1:def 5;
then m in Seg (len Fb) by A61, FINSEQ_1:def 3;
then A122: m in dom Fb by FINSEQ_1:def 3;
then A123: Fb . m in rng Fb by FUNCT_1:3;
then reconsider Fbm = Fb . m as Element of V by A20;
A124: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((1 - r) * fb) . m by A119, A120, FINSEQ_1:def 7
.= (1 - r) * (fb . m) by RVSUM_1:44
.= (1 - r) * (L2 . (Fb . m)) by A61, A121 ;
A125: len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22
.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117
.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2
.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117
.= len (Ft ^ Fm) by FINSEQ_1:22 ;
not Fb . m in Carrier L1 by A3, A16, A20, A123, XBOOLE_0:def 5;
then L1 . Fbm = 0 by RLVECT_2:19;
then r * (L1 . Fbm) = 0 ;
then (r * L1) . Fbm = 0 by RLVECT_2:def 11;
then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Fbm) + (((1 - r) * L2) . Fbm) by A124, RLVECT_2:def 11
.= ((r * L1) + ((1 - r) * L2)) . (Fb . m) by RLVECT_2:def 10 ;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A120, A122, A125, FINSEQ_1:def 7; :: thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0
rng Fb c= rng (Fm ^ Fb) by FINSEQ_1:30;
then consider m9 being object such that
A126: m9 in dom F2 and
A127: F2 . m9 = Fb . m by A91, A123, FUNCT_1:def 3;
reconsider m9 = m9 as Element of NAT by A126;
m9 in Seg (len F2) by A126, FINSEQ_1:def 3;
then m9 in dom f2 by A26, FINSEQ_1:def 3;
then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A11, A124, A127; :: thesis: verum
end;
end;
end;
hence ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ; :: thesis: verum
end;
then A128: for n being Nat st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds
( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ;
A129: rng Fb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1) by A1, A16, A20, RLVECT_2:42;
then rng (Ft ^ Fm) misses rng Fb by A8, A23, XBOOLE_1:79;
then A130: (Ft ^ Fm) ^ Fb is one-to-one by A19, A25, FINSEQ_3:91;
A131: for x being object st x in dom (fm2 ^ fb) holds
(fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
proof
let x be object ; :: thesis: ( x in dom (fm2 ^ fb) implies (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) )
assume A132: x in dom (fm2 ^ fb) ; :: thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
then reconsider n = x as Element of NAT ;
now :: thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
per cases ( n in dom fm2 or ex m being Nat st
( m in dom fb & n = (len fm2) + m ) ) by A132, FINSEQ_1:25;
suppose A133: n in dom fm2 ; :: thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
then n in Seg (len Fm) by A45, FINSEQ_1:def 3;
then A134: n in dom Fm by FINSEQ_1:def 3;
fm2 . n = L2 . (Fm . n) by A45, A133;
then (fm2 ^ fb) . n = L2 . (Fm . n) by A133, FINSEQ_1:def 7;
hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A134, FINSEQ_1:def 7; :: thesis: verum
end;
suppose ex m being Nat st
( m in dom fb & n = (len fm2) + m ) ; :: thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
then consider m being Element of NAT such that
A135: m in dom fb and
A136: n = (len fm2) + m ;
m in Seg (len Fb) by A61, A135, FINSEQ_1:def 3;
then A137: m in dom Fb by FINSEQ_1:def 3;
(fm2 ^ fb) . n = fb . m by A135, A136, FINSEQ_1:def 7
.= L2 . (Fb . m) by A61, A135 ;
hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A45, A136, A137, FINSEQ_1:def 7; :: thesis: verum
end;
end;
end;
hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) ; :: thesis: verum
end;
for x being object holds
( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) )
proof
let x be object ; :: thesis: ( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) )
A138: len (fm2 ^ fb) = (len fm2) + (len fb) by FINSEQ_1:22
.= len (Fm ^ Fb) by A45, A61, FINSEQ_1:22 ;
A139: dom (fm2 ^ fb) = Seg (len (fm2 ^ fb)) by FINSEQ_1:def 3
.= dom (Fm ^ Fb) by A138, FINSEQ_1:def 3 ;
( x in dom (fm2 ^ fb) implies (Fm ^ Fb) . x in dom L2 )
proof
assume x in dom (fm2 ^ fb) ; :: thesis: (Fm ^ Fb) . x in dom L2
then (Fm ^ Fb) . x in rng (Fm ^ Fb) by A139, FUNCT_1:3;
then A140: (Fm ^ Fb) . x in (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31;
dom L2 = the carrier of V by FUNCT_2:92;
hence (Fm ^ Fb) . x in dom L2 by A140; :: thesis: verum
end;
hence ( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) ) by A139; :: thesis: verum
end;
then A141: fm2 ^ fb = L2 * (Fm ^ Fb) by A131, FUNCT_1:10;
rng Fm misses rng Fb by A15, A16, A22, A20, XBOOLE_1:17, XBOOLE_1:85;
then Fm ^ Fb is one-to-one by A21, A19, FINSEQ_3:91;
then A142: F2,Fm ^ Fb are_fiberwise_equipotent by A4, A91, RFINSEQ:26;
then dom F2 = dom (Fm ^ Fb) by RFINSEQ:3;
then A143: Sum f2 = Sum (fm2 ^ fb) by A5, A142, A57, A90, A89, A141, CLASSES1:83, RFINSEQ:9;
A144: Sum (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = (Sum ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:75
.= ((Sum (r * ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:75
.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:87
.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87
.= ((r * (Sum ft)) + ((Sum (r * fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by A69, INTEGRA5:2
.= ((r * (Sum ft)) + ((r * (Sum fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87
.= ((r * (Sum ft)) + ((r * (Sum fm1)) + ((1 - r) * (Sum fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87
.= (r * ((Sum ft) + (Sum fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb)))
.= (r * (Sum (ft ^ fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb))) by RVSUM_1:75
.= (r * 1) + ((1 - r) * 1) by A78, A27, A88, A143, RVSUM_1:75
.= 0 + 1 ;
rng ((Ft ^ Fm) ^ Fb) = (Carrier L1) \/ ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1)) by A8, A23, A129, FINSEQ_1:31
.= (Carrier L1) \/ (Carrier ((r * L1) + ((1 - r) * L2))) by XBOOLE_1:39
.= Carrier ((r * L1) + ((1 - r) * L2)) by A3, A14, XBOOLE_1:7, XBOOLE_1:12 ;
hence (r * L1) + ((1 - r) * L2) is Convex_Combination of V by A130, A144, A80, A128, CONVEX1:def 3; :: thesis: verum