let V be ComplexLinearSpace; for v1, v2, v3 being VECTOR of V
for L being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds
( ex r1, r2, r3 being Real st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
let v1, v2, v3 be VECTOR of V; for L being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds
( ex r1, r2, r3 being Real st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
let L be C_Linear_Combination of V; ( L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 implies ( ex r1, r2, r3 being Real st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ) )
assume that
A1:
L is convex
and
A2:
Carrier L = {v1,v2,v3}
and
A3:
( v1 <> v2 & v2 <> v3 & v3 <> v1 )
; ( ex r1, r2, r3 being Real st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
reconsider L = L as C_Linear_Combination of {v1,v2,v3} 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,v3}
by A2, A4, FINSEQ_4:62;
then A9:
len f = 3
by A3, A6, CARD_2:58;
then A10:
dom f = {1,2,3}
by FINSEQ_1:def 3, FINSEQ_3:1;
then A11:
2 in dom f
by ENUMSET1:def 1;
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 Element of REAL ;
A13:
f . 2 >= 0
by A8, A11;
A14:
3 in dom f
by A10, ENUMSET1:def 1;
then A15:
f . 3 = L . (F . 3)
by A8;
then
f /. 3 = L . (F . 3)
by A14, PARTFUN1:def 6;
then reconsider r3 = L . (F . 3) as Element of REAL ;
A16:
f . 3 >= 0
by A8, A14;
A17:
1 in dom f
by A10, ENUMSET1:def 1;
then A18:
f . 1 = L . (F . 1)
by A8;
then
f /. 1 = L . (F . 1)
by A17, PARTFUN1:def 6;
then reconsider r1 = L . (F . 1) as Element of REAL ;
A19:
f = <*r1,r2,r3*>
by A9, A18, A12, A15, FINSEQ_1:45;
then A20:
(r1 + r2) + r3 = 1
by A7, RVSUM_1:78;
A21:
f . 1 >= 0
by A8, A17;
ex a, b, c being Real st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )
proof
per cases
( F = <*v1,v2,v3*> or F = <*v1,v3,v2*> or F = <*v2,v1,v3*> or F = <*v2,v3,v1*> or F = <*v3,v1,v2*> or F = <*v3,v2,v1*> )
by A2, A3, A4, CONVEX1:31;
suppose A22:
F = <*v1,v2,v3*>
;
ex a, b, c being Real st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )then A23:
(
r1 = L . v1 &
r2 = L . v2 )
by FINSEQ_1:45;
A24:
r2 >= 0
by A8, A11, A12;
A25:
r3 = L . v3
by A22, FINSEQ_1:45;
(
(r1 + r2) + r3 = 1 &
r1 >= 0 )
by A7, A8, A17, A18, A19, RVSUM_1:78;
hence
ex
a,
b,
c being
Real st
(
a = L . v1 &
b = L . v2 &
c = L . v3 &
(a + b) + c = 1 &
a >= 0 &
b >= 0 &
c >= 0 )
by A15, A16, A23, A25, A24;
verum end; suppose A26:
F = <*v1,v3,v2*>
;
ex a, b, c being Real st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )then A27:
(
r1 = L . v1 &
r3 = L . v2 )
by FINSEQ_1:45;
A28:
r3 >= 0
by A8, A14, A15;
A29:
r2 = L . v3
by A26, FINSEQ_1:45;
(
(r1 + r3) + r2 = 1 &
r1 >= 0 )
by A8, A17, A18, A20;
hence
ex
a,
b,
c being
Real st
(
a = L . v1 &
b = L . v2 &
c = L . v3 &
(a + b) + c = 1 &
a >= 0 &
b >= 0 &
c >= 0 )
by A12, A13, A27, A29, A28;
verum end; suppose A30:
F = <*v2,v1,v3*>
;
ex a, b, c being Real st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )then A31:
(
r2 = L . v1 &
r1 = L . v2 )
by FINSEQ_1:45;
A32:
r1 >= 0
by A8, A17, A18;
A33:
r3 = L . v3
by A30, FINSEQ_1:45;
(
(r2 + r1) + r3 = 1 &
r2 >= 0 )
by A7, A8, A11, A12, A19, RVSUM_1:78;
hence
ex
a,
b,
c being
Real st
(
a = L . v1 &
b = L . v2 &
c = L . v3 &
(a + b) + c = 1 &
a >= 0 &
b >= 0 &
c >= 0 )
by A15, A16, A31, A33, A32;
verum end; suppose A34:
F = <*v2,v3,v1*>
;
ex a, b, c being Real st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )then A35:
(
r3 = L . v1 &
r1 = L . v2 )
by FINSEQ_1:45;
A36:
r1 >= 0
by A8, A17, A18;
A37:
r2 = L . v3
by A34, FINSEQ_1:45;
(
(r3 + r1) + r2 = 1 &
r3 >= 0 )
by A8, A14, A15, A20;
hence
ex
a,
b,
c being
Real st
(
a = L . v1 &
b = L . v2 &
c = L . v3 &
(a + b) + c = 1 &
a >= 0 &
b >= 0 &
c >= 0 )
by A12, A13, A35, A37, A36;
verum end; suppose A38:
F = <*v3,v1,v2*>
;
ex a, b, c being Real st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )then A39:
(
r2 = L . v1 &
r3 = L . v2 )
by FINSEQ_1:45;
A40:
r3 >= 0
by A8, A14, A15;
A41:
r1 = L . v3
by A38, FINSEQ_1:45;
(
(r2 + r3) + r1 = 1 &
r2 >= 0 )
by A8, A11, A12, A20;
hence
ex
a,
b,
c being
Real st
(
a = L . v1 &
b = L . v2 &
c = L . v3 &
(a + b) + c = 1 &
a >= 0 &
b >= 0 &
c >= 0 )
by A18, A21, A39, A41, A40;
verum end; suppose A42:
F = <*v3,v2,v1*>
;
ex a, b, c being Real st
( a = L . v1 & b = L . v2 & c = L . v3 & (a + b) + c = 1 & a >= 0 & b >= 0 & c >= 0 )then A43:
(
r3 = L . v1 &
r2 = L . v2 )
by FINSEQ_1:45;
A44:
r2 >= 0
by A8, A11, A12;
A45:
r1 = L . v3
by A42, FINSEQ_1:45;
(
(r3 + r2) + r1 = 1 &
r3 >= 0 )
by A8, A14, A15, A20;
hence
ex
a,
b,
c being
Real st
(
a = L . v1 &
b = L . v2 &
c = L . v3 &
(a + b) + c = 1 &
a >= 0 &
b >= 0 &
c >= 0 )
by A18, A21, A43, A45, A44;
verum end;
end;
hence
( ex r1, r2, r3 being Real st
( r1 = L . v1 & r2 = L . v2 & r3 = L . v3 & (r1 + r2) + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
by A3, Lm3; verum