let x be set ; :: thesis: for V being RealLinearSpace
for L being Linear_Combination of V st L is convex & L . x = 1 holds
Carrier L = {x}
let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V st L is convex & L . x = 1 holds
Carrier L = {x}
let L be Linear_Combination of V; :: thesis: ( L is convex & L . x = 1 implies Carrier L = {x} )
assume that
A1: L is convex and
A2: L . x = 1 ; :: thesis: Carrier L = {x}
x in dom L by A2, FUNCT_1:def 2;
then reconsider v = x as Element of V by FUNCT_2:def 1;
consider K being Linear_Combination of {v} such that
A3: K . v = jj by RLVECT_4:37;
set LK = L - K;
A4: Carrier K c= {v} by RLVECT_2:def 6;
sum (L - K) = (sum L) - (sum K) by Th36
.= (sum L) - 1 by A3, A4, Th32
.= 1 - 1 by A1, Th62
.= 0 ;
then consider F being FinSequence of V such that
F is one-to-one and
A5: rng F = Carrier (L - K) and
A6: 0 = Sum ((L - K) * F) by Def3;
len ((L - K) * F) = len F by FINSEQ_2:33;
then A7: dom ((L - K) * F) = dom F by FINSEQ_3:29;
A8: for i being Nat st i in dom ((L - K) * F) holds
0 <= ((L - K) * F) . i
proof
let i be Nat; :: thesis: ( i in dom ((L - K) * F) implies 0 <= ((L - K) * F) . i )
assume A9: i in dom ((L - K) * F) ; :: thesis: 0 <= ((L - K) * F) . i
then A10: ((L - K) * F) . i = (L - K) . (F . i) by FUNCT_1:12;
A11: F . i in Carrier (L - K) by A5, A7, A9, FUNCT_1:def 3;
then A12: (L - K) . (F . i) = (L . (F . i)) - (K . (F . i)) by RLVECT_2:54;
per cases ( F . i = v or F . i <> v ) ;
suppose F . i = v ; :: thesis: 0 <= ((L - K) * F) . i
hence 0 <= ((L - K) * F) . i by A2, A3, A9, A12, FUNCT_1:12; :: thesis: verum
end;
suppose F . i <> v ; :: thesis: 0 <= ((L - K) * F) . i
then not F . i in Carrier K by A4, TARSKI:def 1;
then K . (F . i) = 0 by A11;
hence 0 <= ((L - K) * F) . i by A1, A10, A11, A12, Th62; :: thesis: verum
end;
end;
end;
Carrier (L - K) = {}
proof
assume Carrier (L - K) <> {} ; :: thesis: contradiction
then consider p being object such that
A13: p in Carrier (L - K) by XBOOLE_0:def 1;
reconsider p = p as Element of V by A13;
consider i being object such that
A14: i in dom F and
A15: F . i = p by A5, A13, FUNCT_1:def 3;
reconsider i = i as Nat by A14;
((L - K) * F) . i > 0
proof
A16: (L - K) . p = (L . p) - (K . p) by RLVECT_2:54;
per cases ( p = v or p <> v ) ;
suppose p = v ; :: thesis: ((L - K) * F) . i > 0
then (L - K) . p = 1 - 1 by A2, A3, RLVECT_2:54;
hence ((L - K) * F) . i > 0 by A13, RLVECT_2:19; :: thesis: verum
end;
end;
end;
hence contradiction by A6, A7, A8, A14, RVSUM_1:85; :: thesis: verum
end;
then ZeroLC V = L + (- K) by RLVECT_2:def 5;
then A18: - K = - L by RLVECT_2:50;
A19: v in Carrier L by A2;
- (- L) = L by RLVECT_2:53;
then K = L by A18, RLVECT_2:53;
hence Carrier L = {x} by A4, A19, ZFMISC_1:33; :: thesis: verum