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

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

.= (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

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

L . v <= 1
by A1, RLAFFIN1:63;
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;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

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

sum LK =
(sum L) - (sum K)
by RLAFFIN1:36
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 ;

end;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 ;

.= (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