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 object 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 rr be Real; :: thesis: ( rr <= 0 or 1 <= rr or not u in M or not v in M or (rr * u) + ((1 - rr) * v) in M )
reconsider r = rr as Real ;
assume that
A2: 0 < rr and
A3: rr < 1 and
A4: ( u in M & v in M ) ; :: thesis: (rr * u) + ((1 - rr) * v) in M
set N = {u,v};
A5: {u,v} c= M by A4, ZFMISC_1:32;
reconsider N = {u,v} as Subset of V ;

now :: thesis: (rr * u) + ((1 - rr) * v) in M

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

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

consider L being Linear_Combination of {u,v} such that
A7: ( L . u = r & L . v = 1 - r ) by A6, RLVECT_4:38;
reconsider L = L as Linear_Combination of N ;
A8: L is convex

proof

A9: r - r < 1 - r by A3, XREAL_1:9;
then v in { w where w is Element of V : L . w <> 0 } by A7;
then A10: v in Carrier L by RLVECT_2:def 4;
A11: 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 A12: n in {1,2} by FINSEQ_1:2, FINSEQ_1:44;

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

u in { w where w is Element of V : L . w <> 0 } by A2, A7;
then u in Carrier L by RLVECT_2:def 4;
then A15: ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A10, RLVECT_2:def 6, ZFMISC_1:32;
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₂ ) ) ) ) )
A16: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:77
.= 1 ;
thus F is one-to-one by A6, FINSEQ_3:94; :: 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₂ ) ) ) ) )
thus rng F = (rng <*u*>) \/ (rng <*v*>) by FINSEQ_1:31
.= {u} \/ (rng <*v*>) by FINSEQ_1:38
.= {u} \/ {v} by FINSEQ_1:38
.= {u,v} by ENUMSET1:1
.= Carrier L by A15, 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₂ ) ) ) )
reconsider r = r as Element of REAL by XREAL_0:def 1;
reconsider jr = 1 - r as Element of REAL by XREAL_0:def 1;
take f = <*r,jr*>; :: 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₁ ) ) ) )
len <*r,(1 - r)*> = 2 by FINSEQ_1:44
.= len <*u,v*> by FINSEQ_1:44 ;
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 ) ) ) by A16, A11; :: thesis: verum

end;

Sum L = (r * u) + ((1 - r) * v) by A6, A7, RLVECT_2:33;
hence (rr * u) + ((1 - rr) * v) in M by A1, A5, A8; :: thesis: verum

end;

suppose A17: u = v ; :: thesis: (rr * u) + ((1 - rr) * v) in M

consider L being Linear_Combination of {u} such that
A18: L . u = jj by RLVECT_4:37;
reconsider L = L as Linear_Combination of N by A17, ENUMSET1:29;
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

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 ) ) ) )
A19: 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

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 ) ) )
A20: 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:2, FINSEQ_1:38;
then A21: n = 1 by TARSKI:def 1;
then <*rr*> . n = 1
.= L . (<*u*> . n) by A18, A21 ;
hence ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ; :: thesis: verum

end;

len <*1*> = 1 by FINSEQ_1:39
.= len <*u*> by FINSEQ_1:39 ;
hence ( 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 A20, FINSOP_1:11; :: thesis: verum

end;

u in { w where w is Element of V : L . w <> 0 } by A18;
then A22: u in Carrier L by RLVECT_2:def 4;
v in { w where w is Element of V : L . w <> 0 } by A17, A18;
then v in Carrier L by RLVECT_2:def 4;
then ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by A22, RLVECT_2:def 6, ZFMISC_1:32;
then Carrier L = {u,v} by XBOOLE_0:def 10;
then Carrier L = {u} by A17, ENUMSET1:29;
hence ( <*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 A19, FINSEQ_1:38, FINSEQ_3:93; :: thesis: verum

end;

then L is convex ;
then A23: Sum L in M by A1, A5;
(r * u) + ((1 - r) * v) = (r + (1 - r)) * u by A17, RLVECT_1:def 6
.= (0 + 1) * u ;
hence (rr * u) + ((1 - rr) * v) in M by A18, A23, RLVECT_2:32; :: thesis: verum

end;

end;

end;

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