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

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

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

Carrier (L - K) = {}
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;

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

proof

then
ZeroLC V = L + (- K)
by RLVECT_2:def 5;
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

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

hence
contradiction
by A6, A7, A8, A14, RVSUM_1:85; :: thesis: verum
A16:
(L - K) . p = (L . p) - (K . p)
by RLVECT_2:54;

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