let V be RealLinearSpace; :: thesis:
let v, u be VECTOR of V; :: thesis:
let A be Subset of V; :: thesis:
reconsider Z = 0 as Real ;
assume that
A1: v in conv A and
A2: u in conv A and
A3: v <> u ; :: thesis:
reconsider A1 = A as non empty Subset of V by A1;
A4: conv A1 = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;
then consider Lv being Convex_Combination of A1 such that
A5: v = Sum Lv and
A6: Lv in ConvexComb V by A1;
set Cv = Carrier Lv;
A7: Carrier Lv c= A by RLVECT_2:def 6;
consider Lu being Convex_Combination of A1 such that
A8: u = Sum Lu and
Lu in ConvexComb V by A2, A4;
set Cu = Carrier Lu;
A9: Carrier Lu c= A by RLVECT_2:def 6;
then A10: (Carrier Lv) \/ (Carrier Lu) c= A by A7, XBOOLE_1:8;

suppose not Carrier Lu c= Carrier Lv ; :: thesis:

then consider p being object such that
A11: p in Carrier Lu and
A12: not p in Carrier Lv ;
reconsider p = p as Element of V by A11;
( Carrier Lv <> {} & Carrier Lv c= A \ {p} ) by A7, A12, CONVEX1:21, ZFMISC_1:34;
then reconsider Ap = A \ {p} as non empty Subset of V ;
Carrier Lv c= Ap by A7, A12, ZFMISC_1:34;
then reconsider LV = Lv as Linear_Combination of Ap by RLVECT_2:def 6;
take p ; :: thesis:
take w = v; :: thesis:
take Z ; :: thesis:
A13: (Z * u) + ((1 - Z) * w) = (0. V) + (1 * w) by RLVECT_1:10
.= (0. V) + w by RLVECT_1:def 8
.= v ;
Sum LV in { (Sum K) where K is Convex_Combination of Ap : K in ConvexComb V } by A6;
hence ( p in A & w in conv (A \ {p}) & 0 <= Z & Z < 1 & (Z * u) + ((1 - Z) * w) = v ) by A5, A9, A11, A13, CONVEX3:5; :: thesis:

end;

suppose A14: Carrier Lu c= Carrier Lv ; :: thesis:

defpred S₁[ set , set ] means for r being Real
for p being Element of V st r = $2 & p = $1 holds
( r < 0 & Lv . p <> Lu . p & ((r * Lu) + ((1 - r) * Lv)) . p = 0 );
set P = { r where r is Element of REAL : ex p being Element of V st
( S₁[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } ;

A15: now :: thesis:

let x be object ; :: thesis:
assume x in { r where r is Element of REAL : ex p being Element of V st
( S₁[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } ; :: thesis:
then ex r being Element of REAL st
( r = x & ex p being Element of V st
( S₁[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) ) ;
hence x is real ; :: thesis:

end;

A16: for p being Element of V
for r, s being Element of REAL st S₁[p,r] & S₁[p,s] holds
r = s

proof

let p be Element of V; :: thesis:
let r, s be Element of REAL ; :: thesis:
assume A17: S₁[p,r] ; :: thesis:
then A18: ((r * Lu) + ((1 - r) * Lv)) . p = 0 ;
A19: Lv . p <> Lu . p by A17;
assume S₁[p,s] ; :: thesis:
then ((s * Lu) + ((1 - s) * Lv)) . p = 0 ;
then s = ((Lv . p) - 0) / ((Lv . p) - (Lu . p)) by A19, Lm3
.= r by A18, A19, Lm3 ;
hence r = s ; :: thesis:

end;

( sum Lu = 1 & sum Lv = 1 ) by RLAFFIN1:62;
then consider p being Element of V such that
A20: Lu . p > Lv . p by A3, A5, A8, Th24;
A21: Lv . p <> 0

proof

assume A22: Lv . p = 0 ; :: thesis:
then not p in Carrier Lu by A14, RLVECT_2:19;
hence contradiction by A20, A22; :: thesis:

end;

then p in Carrier Lv ;
then A23: p in (Carrier Lv) \/ (Carrier Lu) by XBOOLE_0:def 3;
set r = (Lv . p) / ((Lv . p) - (Lu . p));
A24: ( (Lv . p) / ((Lv . p) - (Lu . p)) = ((Lv . p) - Z) / ((Lv . p) - (Lu . p)) & (Lv . p) - (Lu . p) < (Lu . p) - (Lu . p) ) by A20, XREAL_1:9;
Lv . p > 0 by A21, RLAFFIN1:62;
then S₁[p,(Lv . p) / ((Lv . p) - (Lu . p))] by A24, Lm3;
then A25: (Lv . p) / ((Lv . p) - (Lu . p)) in { r where r is Element of REAL : ex p being Element of V st
( S₁[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } by A23;
A26: (Carrier Lv) \/ (Carrier Lu) is finite ;
{ r where r is Element of REAL : ex p being Element of V st
( S₁[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } is finite from FRAENKEL:sch 28(A26, A16);
then reconsider P = { r where r is Element of REAL : ex p being Element of V st
( S₁[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) } as non empty finite real-membered set by A15, A25, MEMBERED:def 3;
set M = max P;
max P in P by XXREAL_2:def 8;
then consider r being Element of REAL such that
A27: max P = r and
A28: ex p being Element of V st
( S₁[p,r] & p in (Carrier Lv) \/ (Carrier Lu) ) ;
set Lw = (r * Lu) + ((1 - r) * Lv);
consider p being Element of V such that
A29: S₁[p,r] and
A30: p in (Carrier Lv) \/ (Carrier Lu) by A28;
set w = (r * u) + ((1 - r) * v);
set R = (- r) / (1 - r);
A31: Sum ((r * Lu) + ((1 - r) * Lv)) = (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:1
.= (r * u) + (Sum ((1 - r) * Lv)) by A8, RLVECT_3:2
.= (r * u) + ((1 - r) * v) by A5, RLVECT_3:2 ;
A32: for z being Element of V holds 0 <= ((r * Lu) + ((1 - r) * Lv)) . z

proof

let z be Element of V; :: thesis:
A33: ((Z * Lu) + ((1 - Z) * Lv)) . z = ((Z * Lu) . z) + (((1 - Z) * Lv) . z) by RLVECT_2:def 10
.= (Z * (Lu . z)) + (((1 - Z) * Lv) . z) by RLVECT_2:def 11
.= (Z * (Lu . z)) + ((1 - 0) * (Lv . z)) by RLVECT_2:def 11
.= Lv . z ;
assume A34: 0 > ((r * Lu) + ((1 - r) * Lv)) . z ; :: thesis:
A35: ((r * Lu) + ((1 - r) * Lv)) . z = ((r * Lu) . z) + (((1 - r) * Lv) . z) by RLVECT_2:def 10
.= (r * (Lu . z)) + (((1 - r) * Lv) . z) by RLVECT_2:def 11
.= (r * (Lu . z)) + ((1 - r) * (Lv . z)) by RLVECT_2:def 11 ;
A36: Lv . z <> 0

proof

assume A37: Lv . z = 0 ; :: thesis:
then not z in Carrier Lu by A14, RLVECT_2:19;
then Lu . z = 0 ;
hence contradiction by A34, A35, A37; :: thesis:

end;

then z in Carrier Lv ;
then A38: z in (Carrier Lv) \/ (Carrier Lu) by XBOOLE_0:def 3;
Lv . z >= 0 by RLAFFIN1:62;
then consider rs being Real such that
A39: ((rs * Lu) + ((1 - rs) * Lv)) . z = 0 and
A40: ( r <= 0 implies ( r <= rs & rs <= 0 ) ) and
( 0 <= r implies ( 0 <= rs & rs <= r ) ) by A33, A34, Th25;
reconsider rs = rs as Element of REAL by XREAL_0:def 1;
rs <> 0 by A33, A36, A39;
then S₁[z,rs] by A29, A34, A35, A39, A40, RLAFFIN1:62;
then rs in P by A38;
then rs <= r by A27, XXREAL_2:def 8;
then rs = r by A28, A40, XXREAL_0:1;
hence contradiction by A34, A39; :: thesis:

end;

( r * Lu is Linear_Combination of A & (1 - r) * Lv is Linear_Combination of A ) by RLVECT_2:44;
then (r * Lu) + ((1 - r) * Lv) is Linear_Combination of A by RLVECT_2:38;
then A41: Carrier ((r * Lu) + ((1 - r) * Lv)) c= A by RLVECT_2:def 6;
((r * Lu) + ((1 - r) * Lv)) . p = 0 by A29;
then not p in Carrier ((r * Lu) + ((1 - r) * Lv)) by RLVECT_2:19;
then A42: Carrier ((r * Lu) + ((1 - r) * Lv)) c= A \ {p} by A41, ZFMISC_1:34;
A43: sum ((r * Lu) + ((1 - r) * Lv)) = (sum (r * Lu)) + (sum ((1 - r) * Lv)) by RLAFFIN1:34
.= (r * (sum Lu)) + (sum ((1 - r) * Lv)) by RLAFFIN1:35
.= (r * 1) + (sum ((1 - r) * Lv)) by RLAFFIN1:62
.= (r * 1) + ((1 - r) * (sum Lv)) by RLAFFIN1:35
.= (r * 1) + ((1 - r) * 1) by RLAFFIN1:62
.= 1 ;
then (r * Lu) + ((1 - r) * Lv) is convex by A32, RLAFFIN1:62;
then Carrier ((r * Lu) + ((1 - r) * Lv)) <> {} by CONVEX1:21;
then reconsider Ap = A \ {p} as non empty Subset of V by A42;
reconsider LW = (r * Lu) + ((1 - r) * Lv) as Linear_Combination of Ap by A42, RLVECT_2:def 6;
A44: LW is convex by A32, A43, RLAFFIN1:62;
then LW in ConvexComb V by CONVEX3:def 1;
then A45: Sum LW in { (Sum K) where K is Convex_Combination of Ap : K in ConvexComb V } by A44;
take p ; :: thesis:
take (r * u) + ((1 - r) * v) ; :: thesis:
take (- r) / (1 - r) ; :: thesis:
A46: 0 > r by A29;
then A47: ( 1 + (- r) > 0 + (- r) & (1 + (- r)) / (1 + (- r)) = 1 ) by XCMPLX_1:60, XREAL_1:6;
(((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = (((- r) / (1 - r)) * u) + ((((1 - r) / (1 - r)) - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) by A46, XCMPLX_1:60
.= (((- r) / (1 - r)) * u) + ((((1 - r) - (- r)) / (1 - r)) * ((r * u) + ((1 - r) * v))) by XCMPLX_1:120
.= (((- r) / (1 - r)) * u) + (((1 / (1 - r)) * (r * u)) + ((1 / (1 - r)) * ((1 - r) * v))) by RLVECT_1:def 5
.= (((- r) / (1 - r)) * u) + ((((1 / (1 - r)) * r) * u) + ((1 / (1 - r)) * ((1 - r) * v))) by RLVECT_1:def 7
.= (((- r) / (1 - r)) * u) + ((((1 / (1 - r)) * r) * u) + (((1 / (1 - r)) * (1 - r)) * v)) by RLVECT_1:def 7
.= (((- r) / (1 - r)) * u) + ((((r / (1 - r)) * 1) * u) + (((1 / (1 - r)) * (1 - r)) * v)) by XCMPLX_1:75
.= (((- r) / (1 - r)) * u) + (((r / (1 - r)) * u) + (1 * v)) by A46, XCMPLX_1:87
.= ((((- r) / (1 - r)) * u) + ((r / (1 - r)) * u)) + (1 * v) by RLVECT_1:def 3
.= ((((- r) / (1 - r)) + (r / (1 - r))) * u) + (1 * v) by RLVECT_1:def 6
.= ((((- r) + r) / (1 - r)) * u) + (1 * v) by XCMPLX_1:62
.= ((0 / (1 - r)) * u) + v by RLVECT_1:def 8
.= (0. V) + v by RLVECT_1:10
.= v ;
hence ( p in A & (r * u) + ((1 - r) * v) in conv (A \ {p}) & 0 <= (- r) / (1 - r) & (- r) / (1 - r) < 1 & (((- r) / (1 - r)) * u) + ((1 - ((- r) / (1 - r))) * ((r * u) + ((1 - r) * v))) = v ) by A10, A30, A31, A45, A46, A47, CONVEX3:5, XREAL_1:74; :: thesis:

end;