let V be RealLinearSpace; :: thesis: for M being convex Subset of V
for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let M be convex Subset of V; :: thesis: for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let N be Subset of V; :: thesis: for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let L be Linear_Combination of N; :: thesis: ( L is convex & N c= M implies Sum L in M )
assume that
A1: L is convex and
A2: N c= M ; :: thesis: Sum L in M
consider F being FinSequence of the carrier of V such that
A3: F is one-to-one and
A4: rng F = Carrier L and
A5: ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A1;
consider f being FinSequence of REAL such that
A6: len f = len F and
A7: Sum f = 1 and
A8: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A5;
not Carrier L, {} are_equipotent by A1, CARD_1:26, CONVEX1:21;
then A9: card (Carrier L) <> card {} by CARD_1:5;
then reconsider i = len F as non zero Element of NAT by A3, A4, FINSEQ_4:62;
A10: len (L (#) F) = len F by RLVECT_2:def 7;
defpred S1[ Nat] means (1 / (Sum (mid (f,1,$1)))) * (Sum (mid ((L (#) F),1,$1))) in M;
A11: len (L (#) F) = len F by RLVECT_2:def 7;
A12: for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A13: k >= 1 by NAT_1:14;
assume A14: (1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))) in M ; :: thesis: S1[k + 1]
now :: thesis: S1[k + 1]
per cases ( k >= len f or k < len f ) ;
suppose A15: k >= len f ; :: thesis: S1[k + 1]
A16: mid ((L (#) F),1,(k + 1)) = (L (#) F) | (k + 1) by FINSEQ_6:116, NAT_1:12
.= L (#) F by A6, A11, A15, FINSEQ_1:58, NAT_1:12 ;
A17: mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14
.= f by A15, FINSEQ_1:58 ;
A18: mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:12
.= f by A15, FINSEQ_1:58, NAT_1:12 ;
mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14
.= L (#) F by A6, A11, A15, FINSEQ_1:58 ;
hence S1[k + 1] by A14, A17, A18, A16; :: thesis: verum
end;
suppose A19: k < len f ; :: thesis: S1[k + 1]
mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14;
then A20: len (mid (f,1,k)) = k by A19, FINSEQ_1:59;
A21: ex i being Element of NAT st
( i in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . i )
proof
take 1 ; :: thesis: ( 1 in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . 1 )
1 <= len f by A19, NAT_1:14;
then A22: 1 in Seg (len f) ;
then 1 in dom f by FINSEQ_1:def 3;
then A23: ( f . 1 = L . (F . 1) & f . 1 >= 0 ) by A8;
1 in dom F by A6, A22, FINSEQ_1:def 3;
then F . 1 in Carrier L by A4, FUNCT_1:def 3;
then F . 1 in { v where v is Element of V : L . v <> 0 } by RLVECT_2:def 4;
then A24: ex v being Element of V st
( v = F . 1 & L . v <> 0 ) ;
1 in Seg (len (mid (f,1,k))) by A13, A20;
hence ( 1 in dom (mid (f,1,k)) & 0 < (mid (f,1,k)) . 1 ) by A13, A19, A23, A24, FINSEQ_1:def 3, FINSEQ_6:123; :: thesis: verum
end;
A25: for i being Nat st i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> holds
(mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i
proof
let i be Nat; :: thesis: ( i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> implies (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i )
assume i in dom <*((mid (f,1,(k + 1))) . (k + 1))*> ; :: thesis: (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i
then i in Seg 1 by FINSEQ_1:38;
then i = 1 by FINSEQ_1:2, TARSKI:def 1;
hence (mid (f,1,(k + 1))) . ((len (mid (f,1,k))) + i) = <*((mid (f,1,(k + 1))) . (k + 1))*> . i by A20; :: thesis: verum
end;
A26: mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:14;
set r1 = Sum (mid (f,1,k));
for i being Nat st i in dom (mid (f,1,k)) holds
0 <= (mid (f,1,k)) . i
proof
let i be Nat; :: thesis: ( i in dom (mid (f,1,k)) implies 0 <= (mid (f,1,k)) . i )
assume i in dom (mid (f,1,k)) ; :: thesis: 0 <= (mid (f,1,k)) . i
then A27: i in Seg k by A20, FINSEQ_1:def 3;
then A28: 1 <= i by FINSEQ_1:1;
A29: i <= k by A27, FINSEQ_1:1;
then i <= len f by A19, XXREAL_0:2;
then A30: i in dom f by A28, FINSEQ_3:25;
(mid (f,1,k)) . i = f . i by A19, A28, A29, FINSEQ_6:123;
hence 0 <= (mid (f,1,k)) . i by A8, A30; :: thesis: verum
end;
then A31: Sum (mid (f,1,k)) > 0 by A21, RVSUM_1:85;
A32: k + 1 <= len f by A19, NAT_1:13;
then A33: len (f | (k + 1)) = k + 1 by FINSEQ_1:59;
A34: for i being Nat st i in dom (mid (f,1,k)) holds
(mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i
proof
let i be Nat; :: thesis: ( i in dom (mid (f,1,k)) implies (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i )
A35: mid (f,1,k) = f | k by FINSEQ_6:116, NAT_1:14;
assume A36: i in dom (mid (f,1,k)) ; :: thesis: (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i
then A37: i in Seg (len (f | k)) by A35, FINSEQ_1:def 3;
len (f | k) = k by A19, FINSEQ_1:59;
then i <= k by A37, FINSEQ_1:1;
then A38: i <= k + 1 by NAT_1:12;
(f | k) . i = (f | k) /. i by A36, A35, PARTFUN1:def 6;
then A39: (mid (f,1,k)) . i = f /. i by A36, A35, FINSEQ_4:70;
( i in NAT & 1 <= i ) by A37, FINSEQ_1:1;
then i in Seg (k + 1) by A38;
then A40: i in dom (f | (k + 1)) by A33, FINSEQ_1:def 3;
then (f | (k + 1)) . i = (f | (k + 1)) /. i by PARTFUN1:def 6;
hence (mid (f,1,(k + 1))) . i = (mid (f,1,k)) . i by A26, A39, A40, FINSEQ_4:70; :: thesis: verum
end;
A41: k + 1 >= 1 by NAT_1:14;
then A42: k + 1 in Seg (len f) by A32;
then A43: k + 1 in dom f by FINSEQ_1:def 3;
A44: k + 1 in dom F by A6, A42, FINSEQ_1:def 3;
k + 1 in Seg (k + 1) by A41;
then A45: k + 1 in dom (f | (k + 1)) by A33, FINSEQ_1:def 3;
then (f | (k + 1)) /. (k + 1) = f /. (k + 1) by FINSEQ_4:70;
then (mid (f,1,(k + 1))) . (k + 1) = f /. (k + 1) by A26, A45, PARTFUN1:def 6;
then (mid (f,1,(k + 1))) . (k + 1) = f . (k + 1) by A43, PARTFUN1:def 6
.= L . (F . (k + 1)) by A8, A43 ;
then A46: (mid (f,1,(k + 1))) . (k + 1) = L . (F /. (k + 1)) by A44, PARTFUN1:def 6;
mid (f,1,(k + 1)) = f | (k + 1) by FINSEQ_6:116, NAT_1:14;
then ( len <*((mid (f,1,(k + 1))) . (k + 1))*> = 1 & len (mid (f,1,(k + 1))) = k + 1 ) by A32, FINSEQ_1:40, FINSEQ_1:59;
then dom (mid (f,1,(k + 1))) = Seg ((len (mid (f,1,k))) + (len <*((mid (f,1,(k + 1))) . (k + 1))*>)) by A20, FINSEQ_1:def 3;
then mid (f,1,(k + 1)) = (mid (f,1,k)) ^ <*((mid (f,1,(k + 1))) . (k + 1))*> by A34, A25, FINSEQ_1:def 7;
then A47: Sum (mid (f,1,(k + 1))) = (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) by A46, RVSUM_1:74;
A48: mid ((L (#) F),1,(k + 1)) = (L (#) F) | (k + 1) by FINSEQ_6:116, NAT_1:14;
set w2 = F /. (k + 1);
set w1 = Sum (mid ((L (#) F),1,k));
set r2 = L . (F /. (k + 1));
A49: (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) = (Sum (mid (f,1,k))) / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) by XCMPLX_1:99;
A50: ( F /. (k + 1) in M & L . (F /. (k + 1)) > 0 )
proof
k + 1 in Seg (len f) by A41, A32;
then k + 1 in dom f by FINSEQ_1:def 3;
then A51: ( f . (k + 1) = L . (F . (k + 1)) & f . (k + 1) >= 0 ) by A8;
k + 1 in Seg (len F) by A6, A41, A32;
then A52: k + 1 in dom F by FINSEQ_1:def 3;
then F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;
then A53: F /. (k + 1) in Carrier L by A4, A52, FUNCT_1:def 3;
Carrier L c= N by RLVECT_2:def 6;
hence F /. (k + 1) in M by A2, A53; :: thesis: L . (F /. (k + 1)) > 0
F /. (k + 1) in { v where v is Element of V : L . v <> 0 } by A53, RLVECT_2:def 4;
then ex v being Element of V st
( v = F /. (k + 1) & L . v <> 0 ) ;
hence L . (F /. (k + 1)) > 0 by A52, A51, PARTFUN1:def 6; :: thesis: verum
end;
then (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) > Sum (mid (f,1,k)) by XREAL_1:29;
then A54: (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) < 1 by A31, A49, XREAL_1:189;
A55: (Sum (mid (f,1,k))) + (L . (F /. (k + 1))) > 0 + 0 by A31, A50;
then 1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) > 0 by XREAL_1:139;
then A56: 0 < (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k))) by A31, XREAL_1:129;
k + 1 <= len (L (#) F) by A6, A32, RLVECT_2:def 7;
then A57: k + 1 in dom (L (#) F) by A41, FINSEQ_3:25;
A58: k < len (L (#) F) by A6, A19, RLVECT_2:def 7;
then A59: k + 1 <= len (L (#) F) by NAT_1:13;
then A60: len ((L (#) F) | (k + 1)) = k + 1 by FINSEQ_1:59;
A61: for i being Nat st i in dom (mid ((L (#) F),1,k)) holds
(mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i
proof
let i be Nat; :: thesis: ( i in dom (mid ((L (#) F),1,k)) implies (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i )
A62: mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14;
assume A63: i in dom (mid ((L (#) F),1,k)) ; :: thesis: (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i
then A64: i in Seg (len ((L (#) F) | k)) by A62, FINSEQ_1:def 3;
len ((L (#) F) | k) = k by A58, FINSEQ_1:59;
then i <= k by A64, FINSEQ_1:1;
then A65: i <= k + 1 by NAT_1:12;
((L (#) F) | k) . i = ((L (#) F) | k) /. i by A63, A62, PARTFUN1:def 6;
then A66: (mid ((L (#) F),1,k)) . i = (L (#) F) /. i by A63, A62, FINSEQ_4:70;
( i in NAT & 1 <= i ) by A64, FINSEQ_1:1;
then i in Seg (k + 1) by A65;
then A67: i in dom ((L (#) F) | (k + 1)) by A60, FINSEQ_1:def 3;
then ((L (#) F) | (k + 1)) . i = ((L (#) F) | (k + 1)) /. i by PARTFUN1:def 6;
hence (mid ((L (#) F),1,(k + 1))) . i = (mid ((L (#) F),1,k)) . i by A48, A66, A67, FINSEQ_4:70; :: thesis: verum
end;
k + 1 in Seg (k + 1) by A41;
then A68: k + 1 in dom ((L (#) F) | (k + 1)) by A60, FINSEQ_1:def 3;
then ((L (#) F) | (k + 1)) /. (k + 1) = (L (#) F) /. (k + 1) by FINSEQ_4:70;
then (mid ((L (#) F),1,(k + 1))) . (k + 1) = (L (#) F) /. (k + 1) by A48, A68, PARTFUN1:def 6;
then A69: (mid ((L (#) F),1,(k + 1))) . (k + 1) = (L (#) F) . (k + 1) by A57, PARTFUN1:def 6
.= (L . (F /. (k + 1))) * (F /. (k + 1)) by A57, RLVECT_2:def 7 ;
mid ((L (#) F),1,k) = (L (#) F) | k by FINSEQ_6:116, NAT_1:14;
then A70: len (mid ((L (#) F),1,k)) = k by A58, FINSEQ_1:59;
A71: for i being Nat st i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> holds
(mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i
proof
let i be Nat; :: thesis: ( i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> implies (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i )
assume i in dom <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> ; :: thesis: (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i
then i in Seg 1 by FINSEQ_1:38;
then i = 1 by FINSEQ_1:2, TARSKI:def 1;
hence (mid ((L (#) F),1,(k + 1))) . ((len (mid ((L (#) F),1,k))) + i) = <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> . i by A70; :: thesis: verum
end;
( len <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> = 1 & len (mid ((L (#) F),1,(k + 1))) = k + 1 ) by A59, A48, FINSEQ_1:40, FINSEQ_1:59;
then dom (mid ((L (#) F),1,(k + 1))) = Seg ((len (mid ((L (#) F),1,k))) + (len <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*>)) by A70, FINSEQ_1:def 3;
then mid ((L (#) F),1,(k + 1)) = (mid ((L (#) F),1,k)) ^ <*((mid ((L (#) F),1,(k + 1))) . (k + 1))*> by A61, A71, FINSEQ_1:def 7;
then A72: (1 / (Sum (mid (f,1,(k + 1))))) * (Sum (mid ((L (#) F),1,(k + 1)))) = (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((Sum (mid ((L (#) F),1,k))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A47, A69, FVSUM_1:71
.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((1 * (Sum (mid ((L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 8
.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((((Sum (mid (f,1,k))) * (1 / (Sum (mid (f,1,k))))) * (Sum (mid ((L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by A31, XCMPLX_1:106
.= (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (((Sum (mid (f,1,k))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 7
.= ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((Sum (mid (f,1,k))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k)))))) + ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 5
.= (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1)))) by RLVECT_1:def 7
.= (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) * ((1 / (Sum (mid (f,1,k)))) * (Sum (mid ((L (#) F),1,k))))) + (((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (L . (F /. (k + 1)))) * (F /. (k + 1))) by RLVECT_1:def 7 ;
1 - ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) = (((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) * (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))))) - ((1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) * (Sum (mid (f,1,k)))) by A55, XCMPLX_1:106
.= (((Sum (mid (f,1,k))) + (L . (F /. (k + 1)))) - (Sum (mid (f,1,k)))) * (1 / ((Sum (mid (f,1,k))) + (L . (F /. (k + 1))))) ;
hence S1[k + 1] by A14, A50, A56, A54, A72, CONVEX1:def 2; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
len F > 0 by A3, A4, A9, FINSEQ_4:62;
then A73: len F >= 0 + 1 by NAT_1:13;
A74: S1[1]
proof
mid (f,1,1) = f | 1 by FINSEQ_6:116;
then A75: len (mid (f,1,1)) = 1 by A6, A73, FINSEQ_1:59;
then 1 in dom (mid (f,1,1)) by FINSEQ_3:25;
then reconsider m = (mid (f,1,1)) . 1 as Element of REAL by PARTFUN1:4;
mid (f,1,1) = <*((mid (f,1,1)) . 1)*> by A75, FINSEQ_1:40;
then A76: Sum (mid (f,1,1)) = m by FINSOP_1:11;
Carrier L c= N by RLVECT_2:def 6;
then A77: Carrier L c= M by A2;
mid ((L (#) F),1,1) = (L (#) F) | 1 by FINSEQ_6:116;
then len (mid ((L (#) F),1,1)) = 1 by A73, A11, FINSEQ_1:59;
then A78: mid ((L (#) F),1,1) = <*((mid ((L (#) F),1,1)) . 1)*> by FINSEQ_1:40;
A79: 1 in Seg (len (L (#) F)) by A73, A11;
then A80: 1 in dom F by A11, FINSEQ_1:def 3;
then A81: F /. 1 = F . 1 by PARTFUN1:def 6;
A82: 1 in dom (L (#) F) by A79, FINSEQ_1:def 3;
A83: F . 1 in rng F by A80, FUNCT_1:def 3;
then F . 1 in { v where v is Element of V : L . v <> 0 } by A4, RLVECT_2:def 4;
then A84: ex v2 being Element of V st
( F . 1 = v2 & L . v2 <> 0 ) ;
1 in dom f by A6, A11, A79, FINSEQ_1:def 3;
then f . 1 = L . (F . 1) by A8
.= L . (F /. 1) by A80, PARTFUN1:def 6 ;
then A85: Sum (mid (f,1,1)) = L . (F /. 1) by A6, A73, A76, FINSEQ_6:123;
(mid ((L (#) F),1,1)) . 1 = (L (#) F) . 1 by A73, A11, FINSEQ_6:123
.= (L . (F /. 1)) * (F /. 1) by A82, RLVECT_2:def 7 ;
then (1 / (Sum (mid (f,1,1)))) * (Sum (mid ((L (#) F),1,1))) = (1 / (Sum (mid (f,1,1)))) * ((L . (F /. 1)) * (F /. 1)) by A78, RLVECT_1:44
.= ((1 / (Sum (mid (f,1,1)))) * (L . (F /. 1))) * (F /. 1) by RLVECT_1:def 7
.= 1 * (F /. 1) by A81, A85, A84, XCMPLX_1:106
.= F /. 1 by RLVECT_1:def 8 ;
hence S1[1] by A4, A81, A83, A77; :: thesis: verum
end;
for k being non zero Nat holds S1[k] from NAT_1:sch 10(A74, A12);
 then A86: (1 / (Sum (mid (f,1,i)))) * (Sum (mid ((L (#) F),1,i))) in M ;
Sum (mid (f,1,(len f))) = 1 by A6, A7, A73, FINSEQ_6:120;
then (1 / (Sum (mid (f,1,(len f))))) * (Sum (mid ((L (#) F),1,(len (L (#) F))))) = Sum (mid ((L (#) F),1,(len (L (#) F)))) by RLVECT_1:def 8
.= Sum (L (#) F) by A73, A10, FINSEQ_6:120 ;
hence Sum L in M by A3, A4, A6, A86, A10, RLVECT_2:def 8; :: thesis: verum