let V be RealLinearSpace; :: thesis: for M being Subset of V holds
( ( M is convex & M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) holds
Sum L in M )
let M be Subset of V; :: thesis: ( ( M is convex & M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) holds
Sum L in M )
A1: ( ( for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) holds
Sum L in M ) implies ( M is convex & M is cone ) )
proof
assume A2: for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) holds
Sum L in M ; :: thesis: ( M is convex & M is cone )
A3: for r being Real
for v being VECTOR of V st r > 0 & v in M holds
r * v in M
proof
let r be Real; :: thesis: for v being VECTOR of V st r > 0 & v in M holds
r * v in M
let v be VECTOR of V; :: thesis: ( r > 0 & v in M implies r * v in M )
assume that
A4: r > 0 and
A5: v in M ; :: thesis: r * v in M
reconsider r = r as Real ;
consider L being Linear_Combination of {v} such that
A6: L . v = r by RLVECT_4:37;
A7: for u being VECTOR of V st u in Carrier L holds
L . u > 0
proof
let u be VECTOR of V; :: thesis: ( u in Carrier L implies L . u > 0 )
A8: Carrier L c= {v} by RLVECT_2:def 6;
assume u in Carrier L ; :: thesis: L . u > 0
hence L . u > 0 by A4, A6, A8, TARSKI:def 1; :: thesis: verum
end;
A9: v in Carrier L by A4, A6, RLVECT_2:19;
{v} c= M by A5, ZFMISC_1:31;
then reconsider L = L as Linear_Combination of M by RLVECT_2:21;
Sum L in M by A2, A9, A7;
hence r * v in M by A6, RLVECT_2:32; :: thesis: verum
end;
A10: for u, v being VECTOR of V st u in M & v in M holds
u + v in M
proof
let u, v be VECTOR of V; :: thesis: ( u in M & v in M implies u + v in M )
assume that
A11: u in M and
A12: v in M ; :: thesis: u + v in M
per cases ( u <> v or u = v ) ;
suppose A13: u <> v ; :: thesis: u + v in M
consider L being Linear_Combination of {u,v} such that
A14: ( L . u = jj & L . v = jj ) by A13, RLVECT_4:38;
A15: Sum L = (1 * u) + (1 * v) by A13, A14, RLVECT_2:33
.= u + (1 * v) by RLVECT_1:def 8
.= u + v by RLVECT_1:def 8 ;
A16: Carrier L <> {} by A14, RLVECT_2:19;
A17: for v1 being VECTOR of V st v1 in Carrier L holds
L . v1 > 0
proof
let v1 be VECTOR of V; :: thesis: ( v1 in Carrier L implies L . v1 > 0 )
A18: Carrier L c= {u,v} by RLVECT_2:def 6;
assume A19: v1 in Carrier L ; :: thesis: L . v1 > 0
per cases ( v1 = u or v1 = v ) by A19, A18, TARSKI:def 2;
suppose v1 = u ; :: thesis: L . v1 > 0
hence L . v1 > 0 by A14; :: thesis: verum
end;
suppose v1 = v ; :: thesis: L . v1 > 0
hence L . v1 > 0 by A14; :: thesis: verum
end;
end;
end;
{u,v} c= M by A11, A12, ZFMISC_1:32;
then reconsider L = L as Linear_Combination of M by RLVECT_2:21;
Sum L in M by A2, A16, A17;
hence u + v in M by A15; :: thesis: verum
end;
suppose A20: u = v ; :: thesis: u + v in M
(jj + jj) * u in M by A3, A11;
then (1 * u) + (1 * u) in M by RLVECT_1:def 6;
then u + (1 * u) in M by RLVECT_1:def 8;
hence u + v in M by A20, RLVECT_1:def 8; :: thesis: verum
end;
end;
end;
M is cone by A3;
hence ( M is convex & M is cone ) by A10, Th7; :: thesis: verum
end;
( M is convex & M is cone implies for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) holds
Sum L in M )
proof
defpred S1[ Nat] means for LL being Linear_Combination of M st card (Carrier LL) = $1 & ( for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 ) & ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) holds
Sum LL in M;
assume that
A21: M is convex and
A22: M is cone ; :: thesis: for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) holds
Sum L in M
A23: S1[1]
proof
let LL be Linear_Combination of M; :: thesis: ( card (Carrier LL) = 1 & ( for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 ) & ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) implies Sum LL in M )
assume that
A24: card (Carrier LL) = 1 and
A25: for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 and
ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) ; :: thesis: Sum LL in M
consider x being object such that
A26: Carrier LL = {x} by A24, CARD_2:42;
{x} c= M by A26, RLVECT_2:def 6;
then A27: x in M by ZFMISC_1:31;
then reconsider x = x as VECTOR of V ;
x in Carrier LL by A26, TARSKI:def 1;
then A28: LL . x > 0 by A25;
Sum LL = (LL . x) * x by A26, RLVECT_2:35;
hence Sum LL in M by A22, A27, A28; :: thesis: verum
end;
A29: for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A30: S1[k] ; :: thesis: S1[k + 1]
let LL be Linear_Combination of M; :: thesis: ( card (Carrier LL) = k + 1 & ( for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 ) & ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) implies Sum LL in M )
assume that
A31: card (Carrier LL) = k + 1 and
A32: for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 and
A33: ex L1, L2 being Linear_Combination of M st
( Sum LL = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 & Carrier L1 c= Carrier LL & Carrier L2 c= Carrier LL & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v ) ) ; :: thesis: Sum LL in M
consider L1, L2 being Linear_Combination of M such that
A34: Sum LL = (Sum L1) + (Sum L2) and
A35: card (Carrier L1) = 1 and
A36: card (Carrier L2) = (card (Carrier LL)) - 1 and
A37: Carrier L1 c= Carrier LL and
A38: Carrier L2 c= Carrier LL and
A39: for v being VECTOR of V st v in Carrier L1 holds
L1 . v = LL . v and
A40: for v being VECTOR of V st v in Carrier L2 holds
L2 . v = LL . v by A33;
A41: for u being VECTOR of V st u in Carrier L1 holds
L1 . u > 0
proof
let u be VECTOR of V; :: thesis: ( u in Carrier L1 implies L1 . u > 0 )
assume A42: u in Carrier L1 ; :: thesis: L1 . u > 0
then L1 . u = LL . u by A39;
hence L1 . u > 0 by A32, A37, A42; :: thesis: verum
end;
A43: for u being VECTOR of V st u in Carrier L2 holds
L2 . u > 0
proof
let u be VECTOR of V; :: thesis: ( u in Carrier L2 implies L2 . u > 0 )
assume A44: u in Carrier L2 ; :: thesis: L2 . u > 0
then L2 . u = LL . u by A40;
hence L2 . u > 0 by A32, A38, A44; :: thesis: verum
end;
ex LL1, LL2 being Linear_Combination of M st
( Sum L1 = (Sum LL1) + (Sum LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L1)) - 1 & Carrier LL1 c= Carrier L1 & Carrier LL2 c= Carrier L1 & ( for v being VECTOR of V st v in Carrier LL1 holds
LL1 . v = L1 . v ) & ( for v being VECTOR of V st v in Carrier LL2 holds
LL2 . v = L1 . v ) ) by A35, Lm4;
then A45: Sum L1 in M by A23, A35, A41;
card (Carrier L2) >= 0 + 1 by A31, A36, NAT_1:13;
then ex LL1, LL2 being Linear_Combination of M st
( Sum L2 = (Sum LL1) + (Sum LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L2)) - 1 & Carrier LL1 c= Carrier L2 & Carrier LL2 c= Carrier L2 & ( for v being VECTOR of V st v in Carrier LL1 holds
LL1 . v = L2 . v ) & ( for v being VECTOR of V st v in Carrier LL2 holds
LL2 . v = L2 . v ) ) by Lm4;
then Sum L2 in M by A30, A31, A36, A43;
hence Sum LL in M by A21, A22, A34, A45, Th7; :: thesis: verum
end;
A46: for k being non zero Nat holds S1[k] from NAT_1:sch 10(A23, A29);
 let L be Linear_Combination of M; :: thesis: ( Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) implies Sum L in M )
assume that
A47: Carrier L <> {} and
A48: for v being VECTOR of V st v in Carrier L holds
L . v > 0 ; :: thesis: Sum L in M
card (Carrier L) >= 0 + 1 by A47, NAT_1:13;
then ex L1, L2 being Linear_Combination of M st
( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = L . v ) ) by Lm4;
hence Sum L in M by A47, A48, A46; :: thesis: verum
end;
hence ( ( M is convex & M is cone ) iff for L being Linear_Combination of M st Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) holds
Sum L in M ) by A1; :: thesis: verum