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: ( 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
assume A2: ( M is convex & 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
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 A3: ( Carrier L <> {} & ( for v being VECTOR of V st v in Carrier L holds
L . v > 0 ) ) ; :: thesis: Sum L in M
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;
A4: 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
A5: card (Carrier LL) = 1 and
A6: 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 set such that
A7: Carrier LL = {x} by A5, CARD_2:60;
{x} c= M by A7, RLVECT_2:def 8;
then A8: x in M by ZFMISC_1:37;
then reconsider x = x as VECTOR of V ;
A9: Sum LL = (LL . x) * x by A7, RLVECT_2:53;
x in Carrier LL by A7, TARSKI:def 1;
then LL . x > 0 by A6;
hence Sum LL in M by A2, A8, A9, Def3; :: thesis: verum
end;
A10: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A11: 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
A12: card (Carrier LL) = k + 1 and
A13: for u being VECTOR of V st u in Carrier LL holds
LL . u > 0 and
A14: 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
A15: ( 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 ) ) by A14;
card (Carrier L2) >= 0 + 1 by A12, A15, NAT_1:13;
then A16: 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;
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 u in Carrier L2 ; :: thesis: L2 . u > 0
then ( u in Carrier LL & L2 . u = LL . u ) by A15;
hence L2 . u > 0 by A13; :: thesis: verum
end;
then A17: Sum L2 in M by A11, A12, A15, A16;
A18: 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 A15, Lm4;
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 u in Carrier L1 ; :: thesis: L1 . u > 0
then ( u in Carrier LL & L1 . u = LL . u ) by A15;
hence L1 . u > 0 by A13; :: thesis: verum
end;
then Sum L1 in M by A4, A15, A18;
hence Sum LL in M by A2, A15, A17, Th7; :: thesis: verum
end;
A19: for k being non empty Nat holds S1[k] from NAT_1:sch 10(A4, A10);
 card (Carrier L) <> 0 by A3;
then card (Carrier L) > 0 ;
then card (Carrier L) >= 0 + 1 by NAT_1:13;
then A21: 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;
consider k being non empty Element of NAT ;
thus Sum L in M by A3, A19, A21; :: thesis: verum
end;
( ( 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 A23: 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 )
A24: 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 A25: ( r > 0 & v in M ) ; :: thesis: r * v in M
consider L being Linear_Combination of {v} such that
A26: L . v = r from RLVECT_4:sch 2();
 A27: v in Carrier L by A25, A26, RLVECT_2:28;
A28: 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 )
assume A29: u in Carrier L ; :: thesis: L . u > 0
Carrier L c= {v} by RLVECT_2:def 8;
hence L . u > 0 by A25, A26, A29, TARSKI:def 1; :: thesis: verum
end;
{v} c= M by A25, ZFMISC_1:37;
then reconsider L = L as Linear_Combination of M by RLVECT_2:33;
Sum L in M by A23, A27, A28;
hence r * v in M by A26, RLVECT_2:50; :: thesis: verum
end;
then A30: M is cone by Def3;
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 A31: ( u in M & v in M ) ; :: thesis: u + v in M
per cases ( u <> v or u = v ) ;
suppose A32: u <> v ; :: thesis: u + v in M
consider L being Linear_Combination of {u,v} such that
A33: ( L . u = 1 & L . v = 1 ) from RLVECT_4:sch 3(A32);
A34: Carrier L <> {} by A33, RLVECT_2:28;
A35: 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 )
assume A36: v1 in Carrier L ; :: thesis: L . v1 > 0
A37: Carrier L c= {u,v} by RLVECT_2:def 8;
per cases ( v1 = u or v1 = v ) by A36, A37, TARSKI:def 2;
suppose v1 = u ; :: thesis: L . v1 > 0
hence L . v1 > 0 by A33; :: thesis: verum
end;
suppose v1 = v ; :: thesis: L . v1 > 0
hence L . v1 > 0 by A33; :: thesis: verum
end;
end;
end;
A38: Sum L = (1 * u) + (1 * v) by A32, A33, RLVECT_2:51
.= u + (1 * v) by RLVECT_1:def 9
.= u + v by RLVECT_1:def 9 ;
{u,v} c= M by A31, ZFMISC_1:38;
then reconsider L = L as Linear_Combination of M by RLVECT_2:33;
Sum L in M by A23, A34, A35;
hence u + v in M by A38; :: thesis: verum
end;
suppose A39: u = v ; :: thesis: u + v in M
(1 + 1) * u in M by A24, A31;
then (1 * u) + (1 * u) in M by RLVECT_1:def 9;
then u + (1 * u) in M by RLVECT_1:def 9;
hence u + v in M by A39, RLVECT_1:def 9; :: thesis: verum
end;
end;
end;
hence ( M is convex & M is cone ) by A30, Th7; :: 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