let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for A being Subset of V
for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds
ex p being VECTOR of V st
( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )
let v be VECTOR of V; :: thesis: for A being Subset of V
for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds
ex p being VECTOR of V st
( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )
let A be Subset of V; :: thesis: for L being Linear_Combination of A st L is convex & v <> Sum L & L . v <> 0 holds
ex p being VECTOR of V st
( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )
let L be Linear_Combination of A; :: thesis: ( L is convex & v <> Sum L & L . v <> 0 implies ex p being VECTOR of V st
( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v ) )
assume that
A1: L is convex and
A2: v <> Sum L and
A3: L . v <> 0 ; :: thesis: ex p being VECTOR of V st
( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )
set Lv = L . v;
set 1Lv = 1 - (L . v);
A4: Carrier L c= A by RLVECT_2:def 6;
Carrier L <> {} by A1, CONVEX1:21;
then reconsider A1 = A as non empty Subset of V by A4;
consider K being Linear_Combination of {v} such that
A5: K . v = L . v by RLVECT_4:37;
A6: L . v <> 1
proof
assume A7: L . v = 1 ; :: thesis: contradiction
then Carrier L = {v} by A1, RLAFFIN1:64;
then Sum L = 1 * v by A7, RLVECT_2:35
.= v by RLVECT_1:def 8 ;
hence contradiction by A2; :: thesis: verum
end;
L . v <= 1 by A1, RLAFFIN1:63;
then L . v < 1 by A6, XXREAL_0:1;
then A8: 1 - (L . v) > 1 - 1 by XREAL_1:10;
v in Carrier L by A3;
then {v} c= A1 by A4, ZFMISC_1:31;
then K is Linear_Combination of A1 by RLVECT_2:21;
then reconsider LK = L - K as Linear_Combination of A1 by RLVECT_2:56;
(1 / (1 - (L . v))) * LK is Linear_Combination of A by RLVECT_2:44;
then A9: Carrier ((1 / (1 - (L . v))) * LK) c= A1 by RLVECT_2:def 6;
LK . v = (L . v) - (L . v) by A5, RLVECT_2:54;
then A10: ((1 / (1 - (L . v))) * LK) . v = (1 / (1 - (L . v))) * ((L . v) - (L . v)) by RLVECT_2:def 11;
then not v in Carrier ((1 / (1 - (L . v))) * LK) by RLVECT_2:19;
then A11: Carrier ((1 / (1 - (L . v))) * LK) c= A \ {v} by A9, ZFMISC_1:34;
A12: Carrier K c= {v} by RLVECT_2:def 6;
A13: for w being Element of V holds ((1 / (1 - (L . v))) * LK) . w >= 0
proof
let w be Element of V; :: thesis: ((1 / (1 - (L . v))) * LK) . w >= 0
A14: ((1 / (1 - (L . v))) * LK) . w = (1 / (1 - (L . v))) * (LK . w) by RLVECT_2:def 11
.= (1 / (1 - (L . v))) * ((L . w) - (K . w)) by RLVECT_2:54 ;
per cases ( w = v or w <> v ) ;
suppose w = v ; :: thesis: ((1 / (1 - (L . v))) * LK) . w >= 0
hence ((1 / (1 - (L . v))) * LK) . w >= 0 by A10; :: thesis: verum
end;
suppose w <> v ; :: thesis: ((1 / (1 - (L . v))) * LK) . w >= 0
then not w in Carrier K by A12, TARSKI:def 1;
then A15: K . w = 0 ;
L . w >= 0 by A1, RLAFFIN1:62;
hence ((1 / (1 - (L . v))) * LK) . w >= 0 by A8, A14, A15; :: thesis: verum
end;
end;
end;
sum LK = (sum L) - (sum K) by RLAFFIN1:36
.= (sum L) - (L . v) by A5, A12, RLAFFIN1:32
.= 1 - (L . v) by A1, RLAFFIN1:62 ;
then A16: sum ((1 / (1 - (L . v))) * LK) = (1 / (1 - (L . v))) * (1 - (L . v)) by RLAFFIN1:35
.= 1 by A8, XCMPLX_1:106 ;
then (1 / (1 - (L . v))) * LK is convex by A13, RLAFFIN1:62;
then Carrier ((1 / (1 - (L . v))) * LK) <> {} by CONVEX1:21;
then reconsider Av = A \ {v} as non empty Subset of V by A11;
reconsider 1LK = (1 / (1 - (L . v))) * LK as Convex_Combination of Av by A11, A13, A16, RLAFFIN1:62, RLVECT_2:def 6;
take p = Sum 1LK; :: thesis: ( p in conv (A \ {v}) & Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )
1LK in ConvexComb V by CONVEX3:def 1;
then p in { (Sum M) where M is Convex_Combination of Av : M in ConvexComb V } ;
hence p in conv (A \ {v}) by CONVEX3:5; :: thesis: ( Sum L = ((L . v) * v) + ((1 - (L . v)) * p) & ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v )
A17: Sum LK = (Sum L) - (Sum K) by RLVECT_3:4
.= (Sum L) - ((L . v) * v) by A5, RLVECT_2:32 ;
then (1 - (L . v)) * p = (1 - (L . v)) * ((1 / (1 - (L . v))) * ((Sum L) - ((L . v) * v))) by RLVECT_3:2
.= ((1 - (L . v)) * (1 / (1 - (L . v)))) * ((Sum L) - ((L . v) * v)) by RLVECT_1:def 7
.= 1 * ((Sum L) - ((L . v) * v)) by A8, XCMPLX_1:106
.= (Sum L) - ((L . v) * v) by RLVECT_1:def 8 ;
hence Sum L = ((L . v) * v) + ((1 - (L . v)) * p) by RLVECT_4:1; :: thesis: ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = v
1 - (1 / (L . v)) = ((L . v) / (L . v)) - (1 / (L . v)) by A3, XCMPLX_1:60
.= ((L . v) - 1) / (L . v) by XCMPLX_1:120
.= (- (1 - (L . v))) / (L . v)
.= - ((1 - (L . v)) / (L . v)) by XCMPLX_1:187 ;
then (1 - (1 / (L . v))) * (Sum 1LK) = (- ((1 - (L . v)) / (L . v))) * ((1 / (1 - (L . v))) * ((Sum L) - ((L . v) * v))) by A17, RLVECT_3:2
.= ((- ((1 - (L . v)) / (L . v))) * (1 / (1 - (L . v)))) * ((Sum L) - ((L . v) * v)) by RLVECT_1:def 7
.= (- (((1 - (L . v)) / (L . v)) * (1 / (1 - (L . v))))) * ((Sum L) - ((L . v) * v))
.= (- (((1 - (L . v)) / (1 - (L . v))) * (1 / (L . v)))) * ((Sum L) - ((L . v) * v)) by XCMPLX_1:85
.= (- (1 * (1 / (L . v)))) * ((Sum L) - ((L . v) * v)) by A8, XCMPLX_1:60
.= ((- (1 / (L . v))) * (Sum L)) - ((- (1 / (L . v))) * ((L . v) * v)) by RLVECT_1:34
.= ((- (1 / (L . v))) * (Sum L)) + (- ((- (1 / (L . v))) * ((L . v) * v))) by RLVECT_1:def 11
.= ((- (1 / (L . v))) * (Sum L)) + ((- (- (1 / (L . v)))) * ((L . v) * v)) by RLVECT_4:3
.= ((- (1 / (L . v))) * (Sum L)) + (((1 / (L . v)) * (L . v)) * v) by RLVECT_1:def 7
.= ((- (1 / (L . v))) * (Sum L)) + (1 * v) by A3, XCMPLX_1:106
.= ((- (1 / (L . v))) * (Sum L)) + v by RLVECT_1:def 8
.= (- ((1 / (L . v)) * (Sum L))) + v by RLVECT_4:3 ;
hence ((1 / (L . v)) * (Sum L)) + ((1 - (1 / (L . v))) * p) = (((1 / (L . v)) * (Sum L)) + (- ((1 / (L . v)) * (Sum L)))) + v by RLVECT_1:def 3
.= (((1 / (L . v)) * (Sum L)) - ((1 / (L . v)) * (Sum L))) + v by RLVECT_1:def 11
.= v by RLVECT_4:1 ;
:: thesis: verum