let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M1, M2 being Subset of V

for r1, r2 being Real st M1 is convex & M2 is convex holds

(r1 * M1) + (r2 * M2) is convex

let M1, M2 be Subset of V; :: thesis: for r1, r2 being Real st M1 is convex & M2 is convex holds

(r1 * M1) + (r2 * M2) is convex

let r1, r2 be Real; :: thesis: ( M1 is convex & M2 is convex implies (r1 * M1) + (r2 * M2) is convex )

assume that

A1: M1 is convex and

A2: M2 is convex ; :: thesis: (r1 * M1) + (r2 * M2) is convex

let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) holds

(r * u) + ((1 - r) * v) in (r1 * M1) + (r2 * M2)

let p be Real; :: thesis: ( 0 < p & p < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) implies (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) )

assume that

A3: ( 0 < p & p < 1 ) and

A4: u in (r1 * M1) + (r2 * M2) and

A5: v in (r1 * M1) + (r2 * M2) ; :: thesis: (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2)

v in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A5, RUSUB_4:def 9;

then consider v1, v2 being VECTOR of V such that

A6: v = v1 + v2 and

A7: v1 in r1 * M1 and

A8: v2 in r2 * M2 ;

u in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A4, RUSUB_4:def 9;

then consider u1, u2 being VECTOR of V such that

A9: u = u1 + u2 and

A10: u1 in r1 * M1 and

A11: u2 in r2 * M2 ;

consider y1 being VECTOR of V such that

A12: v1 = r1 * y1 and

A13: y1 in M1 by A7;

consider x1 being VECTOR of V such that

A14: u1 = r1 * x1 and

A15: x1 in M1 by A10;

A16: (p * u1) + ((1 - p) * v1) = ((r1 * p) * x1) + ((1 - p) * (r1 * y1)) by A14, A12, RLVECT_1:def 7

.= ((r1 * p) * x1) + ((r1 * (1 - p)) * y1) by RLVECT_1:def 7

.= (r1 * (p * x1)) + ((r1 * (1 - p)) * y1) by RLVECT_1:def 7

.= (r1 * (p * x1)) + (r1 * ((1 - p) * y1)) by RLVECT_1:def 7

.= r1 * ((p * x1) + ((1 - p) * y1)) by RLVECT_1:def 5 ;

consider y2 being VECTOR of V such that

A17: v2 = r2 * y2 and

A18: y2 in M2 by A8;

consider x2 being VECTOR of V such that

A19: u2 = r2 * x2 and

A20: x2 in M2 by A11;

A21: (p * u2) + ((1 - p) * v2) = ((r2 * p) * x2) + ((1 - p) * (r2 * y2)) by A19, A17, RLVECT_1:def 7

.= ((r2 * p) * x2) + ((r2 * (1 - p)) * y2) by RLVECT_1:def 7

.= (r2 * (p * x2)) + ((r2 * (1 - p)) * y2) by RLVECT_1:def 7

.= (r2 * (p * x2)) + (r2 * ((1 - p) * y2)) by RLVECT_1:def 7

.= r2 * ((p * x2) + ((1 - p) * y2)) by RLVECT_1:def 5 ;

(p * x2) + ((1 - p) * y2) in M2 by A2, A3, A20, A18;

then A22: (p * u2) + ((1 - p) * v2) in r2 * M2 by A21;

(p * x1) + ((1 - p) * y1) in M1 by A1, A3, A15, A13;

then A23: (p * u1) + ((1 - p) * v1) in { (r1 * x) where x is VECTOR of V : x in M1 } by A16;

(p * (u1 + u2)) + ((1 - p) * (v1 + v2)) = ((p * u1) + (p * u2)) + ((1 - p) * (v1 + v2)) by RLVECT_1:def 5

.= ((p * u1) + (p * u2)) + (((1 - p) * v1) + ((1 - p) * v2)) by RLVECT_1:def 5

.= (((p * u1) + (p * u2)) + ((1 - p) * v1)) + ((1 - p) * v2) by RLVECT_1:def 3

.= (((p * u1) + ((1 - p) * v1)) + (p * u2)) + ((1 - p) * v2) by RLVECT_1:def 3

.= ((p * u1) + ((1 - p) * v1)) + ((p * u2) + ((1 - p) * v2)) by RLVECT_1:def 3 ;

then (p * (u1 + u2)) + ((1 - p) * (v1 + v2)) in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A23, A22;

hence (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) by A9, A6, RUSUB_4:def 9; :: thesis: verum

for r1, r2 being Real st M1 is convex & M2 is convex holds

(r1 * M1) + (r2 * M2) is convex

let M1, M2 be Subset of V; :: thesis: for r1, r2 being Real st M1 is convex & M2 is convex holds

(r1 * M1) + (r2 * M2) is convex

let r1, r2 be Real; :: thesis: ( M1 is convex & M2 is convex implies (r1 * M1) + (r2 * M2) is convex )

assume that

A1: M1 is convex and

A2: M2 is convex ; :: thesis: (r1 * M1) + (r2 * M2) is convex

let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) holds

(r * u) + ((1 - r) * v) in (r1 * M1) + (r2 * M2)

let p be Real; :: thesis: ( 0 < p & p < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) implies (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) )

assume that

A3: ( 0 < p & p < 1 ) and

A4: u in (r1 * M1) + (r2 * M2) and

A5: v in (r1 * M1) + (r2 * M2) ; :: thesis: (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2)

v in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A5, RUSUB_4:def 9;

then consider v1, v2 being VECTOR of V such that

A6: v = v1 + v2 and

A7: v1 in r1 * M1 and

A8: v2 in r2 * M2 ;

u in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A4, RUSUB_4:def 9;

then consider u1, u2 being VECTOR of V such that

A9: u = u1 + u2 and

A10: u1 in r1 * M1 and

A11: u2 in r2 * M2 ;

consider y1 being VECTOR of V such that

A12: v1 = r1 * y1 and

A13: y1 in M1 by A7;

consider x1 being VECTOR of V such that

A14: u1 = r1 * x1 and

A15: x1 in M1 by A10;

A16: (p * u1) + ((1 - p) * v1) = ((r1 * p) * x1) + ((1 - p) * (r1 * y1)) by A14, A12, RLVECT_1:def 7

.= ((r1 * p) * x1) + ((r1 * (1 - p)) * y1) by RLVECT_1:def 7

.= (r1 * (p * x1)) + ((r1 * (1 - p)) * y1) by RLVECT_1:def 7

.= (r1 * (p * x1)) + (r1 * ((1 - p) * y1)) by RLVECT_1:def 7

.= r1 * ((p * x1) + ((1 - p) * y1)) by RLVECT_1:def 5 ;

consider y2 being VECTOR of V such that

A17: v2 = r2 * y2 and

A18: y2 in M2 by A8;

consider x2 being VECTOR of V such that

A19: u2 = r2 * x2 and

A20: x2 in M2 by A11;

A21: (p * u2) + ((1 - p) * v2) = ((r2 * p) * x2) + ((1 - p) * (r2 * y2)) by A19, A17, RLVECT_1:def 7

.= ((r2 * p) * x2) + ((r2 * (1 - p)) * y2) by RLVECT_1:def 7

.= (r2 * (p * x2)) + ((r2 * (1 - p)) * y2) by RLVECT_1:def 7

.= (r2 * (p * x2)) + (r2 * ((1 - p) * y2)) by RLVECT_1:def 7

.= r2 * ((p * x2) + ((1 - p) * y2)) by RLVECT_1:def 5 ;

(p * x2) + ((1 - p) * y2) in M2 by A2, A3, A20, A18;

then A22: (p * u2) + ((1 - p) * v2) in r2 * M2 by A21;

(p * x1) + ((1 - p) * y1) in M1 by A1, A3, A15, A13;

then A23: (p * u1) + ((1 - p) * v1) in { (r1 * x) where x is VECTOR of V : x in M1 } by A16;

(p * (u1 + u2)) + ((1 - p) * (v1 + v2)) = ((p * u1) + (p * u2)) + ((1 - p) * (v1 + v2)) by RLVECT_1:def 5

.= ((p * u1) + (p * u2)) + (((1 - p) * v1) + ((1 - p) * v2)) by RLVECT_1:def 5

.= (((p * u1) + (p * u2)) + ((1 - p) * v1)) + ((1 - p) * v2) by RLVECT_1:def 3

.= (((p * u1) + ((1 - p) * v1)) + (p * u2)) + ((1 - p) * v2) by RLVECT_1:def 3

.= ((p * u1) + ((1 - p) * v1)) + ((p * u2) + ((1 - p) * v2)) by RLVECT_1:def 3 ;

then (p * (u1 + u2)) + ((1 - p) * (v1 + v2)) in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) } by A23, A22;

hence (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) by A9, A6, RUSUB_4:def 9; :: thesis: verum