let V be RealLinearSpace; :: thesis: for M being Subset of V st ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) holds
M is convex
let M be Subset of V; :: thesis: ( ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) implies M is convex )
assume A1: for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ; :: thesis: M is convex
let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or 1 <= b₁ or not u in M or not v in M or (b₁ * u) + ((1 - b₁) * v) in M )
let r be Real; :: thesis: ( r <= 0 or 1 <= r or not u in M or not v in M or (r * u) + ((1 - r) * v) in M )
assume that
A2: 0 < r and
A3: r < 1 and
A4: u in M and
A5: v in M ; :: thesis: (r * u) + ((1 - r) * v) in M
set N = {u,v};
A6: {u,v} c= M by A4, A5, ZFMISC_1:38;
reconsider N = {u,v} as Subset of V ;

now

per cases ( u <> v or u = v ) ;

suppose A7: u <> v ; :: thesis: (r * u) + ((1 - r) * v) in M

consider L being Linear_Combination of {u,v} such that
A8: ( L . u = r & L . v = 1 - r ) from RLVECT_4:sch 3(A7);
reconsider L = L as Linear_Combination of N ;
A9: Sum L = (r * u) + ((1 - r) * v) by A7, A8, RLVECT_2:51;
L is convex

proof

take F = <*u,v*>; :: according to CONVEX1:def 3 :: thesis: ( F is one-to-one & rng F = Carrier L & ex b₁ being FinSequence of REAL st
( len b₁ = len F & Sum b₁ = 1 & ( for b₂ being set holds
( not b₂ in dom b₁ or ( b₁ . b₂ = L . (F . b₂) & 0 <= b₁ . b₂ ) ) ) ) )
thus F is one-to-one by A7, FINSEQ_3:103; :: thesis: ( rng F = Carrier L & ex b₁ being FinSequence of REAL st
( len b₁ = len F & Sum b₁ = 1 & ( for b₂ being set holds
( not b₂ in dom b₁ or ( b₁ . b₂ = L . (F . b₂) & 0 <= b₁ . b₂ ) ) ) ) )
A10: Carrier L c= {u,v} by RLVECT_2:def 8;
u in { w where w is Element of V : L . w <> 0 } by A2, A8;
then A11: u in Carrier L by RLVECT_2:def 6;
A12: r - r < 1 - r by A3, XREAL_1:11;
then v in { w where w is Element of V : L . w <> 0 } by A8;
then v in Carrier L by RLVECT_2:def 6;
then A13: {u,v} c= Carrier L by A11, ZFMISC_1:38;
thus rng F = (rng <*u*>) \/ (rng <*v*>) by FINSEQ_1:44
.= {u} \/ (rng <*v*>) by FINSEQ_1:55
.= {u} \/ {v} by FINSEQ_1:55
.= {u,v} by ENUMSET1:41
.= Carrier L by A10, A13, XBOOLE_0:def 10 ; :: thesis: ex b₁ being FinSequence of REAL st
( len b₁ = len F & Sum b₁ = 1 & ( for b₂ being set holds
( not b₂ in dom b₁ or ( b₁ . b₂ = L . (F . b₂) & 0 <= b₁ . b₂ ) ) ) )
take f = <*r,(1 - r)*>; :: thesis: ( len f = len F & Sum f = 1 & ( for b₁ being set holds
( not b₁ in dom f or ( f . b₁ = L . (F . b₁) & 0 <= f . b₁ ) ) ) )
thus ( 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 ) ) ) :: thesis: verum

proof

( len f = len <*u,v*> & Sum f = 1 & ( for n being Element of NAT st n in dom f holds
( f . n = L . (<*u,v*> . n) & f . n >= 0 ) ) )

proof

A14: len <*r,(1 - r)*> = 2 by FINSEQ_1:61
.= len <*u,v*> by FINSEQ_1:61 ;
A15: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:107
.= 1 ;
for n being Element of NAT st n in dom <*r,(1 - r)*> holds
( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )

proof

let n be Element of NAT ; :: thesis: ( n in dom <*r,(1 - r)*> implies ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) )
assume n in dom <*r,(1 - r)*> ; :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
then n in Seg (len <*r,(1 - r)*>) by FINSEQ_1:def 3;
then A16: n in {1,2} by FINSEQ_1:4, FINSEQ_1:61;

now

per cases ( n = 1 or n = 2 ) by A16, TARSKI:def 2;

suppose A17: n = 1 ; :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )

then L . (<*u,v*> . n) = r by A8, FINSEQ_1:61;
hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) by A2, A17, FINSEQ_1:61; :: thesis: verum

end;

suppose A18: n = 2 ; :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )

then L . (<*u,v*> . n) = 1 - r by A8, FINSEQ_1:61;
hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) by A12, A18, FINSEQ_1:61; :: thesis: verum

end;

end;

end;

hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) ; :: thesis: verum

end;

hence ( len f = len <*u,v*> & Sum f = 1 & ( for n being Element of NAT st n in dom f holds
( f . n = L . (<*u,v*> . n) & f . n >= 0 ) ) ) by A14, A15; :: thesis: verum

end;

hence ( 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 ) ) ) ; :: thesis: verum

end;

end;

hence (r * u) + ((1 - r) * v) in M by A1, A6, A9; :: thesis: verum

end;

suppose A19: u = v ; :: thesis: (r * u) + ((1 - r) * v) in M

consider L being Linear_Combination of {u} such that
A20: L . u = 1 from RLVECT_4:sch 2();
reconsider L = L as Linear_Combination of N by A19, ENUMSET1:69;
L is convex

proof

ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & 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 ) ) ) )

proof

A21: Carrier L c= {u,v} by RLVECT_2:def 8;
u in { w where w is Element of V : L . w <> 0 } by A20;
then A22: u in Carrier L by RLVECT_2:def 6;
v in { w where w is Element of V : L . w <> 0 } by A19, A20;
then v in Carrier L by RLVECT_2:def 6;
then {u,v} c= Carrier L by A22, ZFMISC_1:38;
then Carrier L = {u,v} by A21, XBOOLE_0:def 10;
then A23: Carrier L = {u} by A19, ENUMSET1:69;
A24: ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) )

proof

A25: len <*1*> = 1 by FINSEQ_1:56
.= len <*u*> by FINSEQ_1:56 ;
A26: for n being Element of NAT st n in dom <*rr*> holds
( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )

proof

let n be Element of NAT ; :: thesis: ( n in dom <*rr*> implies ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) )
assume n in dom <*rr*> ; :: thesis: ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )
then n in {1} by FINSEQ_1:4, FINSEQ_1:55;
then A27: n = 1 by TARSKI:def 1;
then <*rr*> . n = 1 by FINSEQ_1:57
.= L . (<*u*> . n) by A20, A27, FINSEQ_1:57 ;
hence ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) by A27, FINSEQ_1:57; :: thesis: verum

end;

take <*rr*> ; :: thesis: ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds
( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) )
thus ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds
( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) ) by A25, A26, FINSOP_1:12; :: thesis: verum

end;

take <*u*> ; :: thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) )
thus ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) by A23, A24, FINSEQ_1:55, FINSEQ_3:102; :: thesis: verum

end;

hence L is convex by CONVEX1:def 3; :: thesis: verum

end;

then A28: Sum L in M by A1, A6;
(r * u) + ((1 - r) * v) = (r + (1 - r)) * u by A19, RLVECT_1:def 9
.= (0 + 1) * u ;
hence (r * u) + ((1 - r) * v) in M by A20, A28, RLVECT_2:50; :: thesis: verum

end;

end;

end;

hence (r * u) + ((1 - r) * v) in M ; :: thesis: verum