let V be ComplexLinearSpace; :: thesis: for v1, v2 being VECTOR of V
for L being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds
( ex r1, r2 being Real st
( r1 = L . v1 & r2 = L . v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0 ) & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
let v1, v2 be VECTOR of V; :: thesis: for L being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds
( ex r1, r2 being Real st
( r1 = L . v1 & r2 = L . v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0 ) & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
let L be C_Linear_Combination of V; :: thesis: ( L is convex & Carrier L = {v1,v2} & v1 <> v2 implies ( ex r1, r2 being Real st
( r1 = L . v1 & r2 = L . v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0 ) & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) )
assume that
A1: L is convex and
A2: Carrier L = {v1,v2} and
A3: v1 <> v2 ; :: thesis: ( ex r1, r2 being Real st
( r1 = L . v1 & r2 = L . v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0 ) & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
reconsider L = L as C_Linear_Combination of {v1,v2} by A2, Def4;
consider F being FinSequence of the carrier of V such that
A4: ( F is one-to-one & 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;
len F = card {v1,v2} by A2, A4, FINSEQ_4:62;
then A9: len f = 2 by A3, A6, CARD_2:57;
then A10: dom f = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
then A11: 2 in dom f by TARSKI:def 2;
then A12: f . 2 = L . (F . 2) by A8;
then f /. 2 = L . (F . 2) by A11, PARTFUN1:def 6;
then reconsider r2 = L . (F . 2) as Real ;
A13: f . 2 >= 0 by A8, A11;
A14: 1 in dom f by A10, TARSKI:def 2;
then A15: f . 1 = L . (F . 1) by A8;
then f /. 1 = L . (F . 1) by A14, PARTFUN1:def 6;
then reconsider r1 = L . (F . 1) as Real ;
A16: f = <*r1,r2*> by A9, A15, A12, FINSEQ_1:44;
ex c1, c2 being Real st
( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 )
proof
per cases ( F = <*v1,v2*> or F = <*v2,v1*> ) by A2, A3, A4, FINSEQ_3:99;
suppose F = <*v1,v2*> ; :: thesis: ex c1, c2 being Real st
( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 )
then A17: ( r1 = L . v1 & r2 = L . v2 ) by FINSEQ_1:44;
( r1 + r2 = 1 & r1 >= 0 ) by A7, A8, A14, A15, A16, RVSUM_1:77;
hence ex c1, c2 being Real st
( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 ) by A12, A13, A17; :: thesis: verum
end;
suppose F = <*v2,v1*> ; :: thesis: ex c1, c2 being Real st
( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 )
then A18: ( r1 = L . v2 & r2 = L . v1 ) by FINSEQ_1:44;
( r1 + r2 = 1 & r1 >= 0 ) by A7, A8, A14, A15, A16, RVSUM_1:77;
hence ex c1, c2 being Real st
( c1 = L . v1 & c2 = L . v2 & c1 + c2 = 1 & c1 >= 0 & c2 >= 0 ) by A12, A13, A18; :: thesis: verum
end;
end;
end;
hence ( ex r1, r2 being Real st
( r1 = L . v1 & r2 = L . v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0 ) & Sum L = ((L . v1) * v1) + ((L . v2) * v2) ) by A3, Th15; :: thesis: verum