let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M, N being Subset of V st M is convex & N is convex holds

for r being Real holds (r * M) + ((1 - r) * N) is convex

let M, N be Subset of V; :: thesis: ( M is convex & N is convex implies for r being Real holds (r * M) + ((1 - r) * N) is convex )

assume that

A1: M is convex and

A2: N is convex ; :: thesis: for r being Real holds (r * M) + ((1 - r) * N) is convex

let r be Real; :: thesis: (r * M) + ((1 - r) * N) 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 (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) holds

(r * u) + ((1 - r) * v) in (r * M) + ((1 - r) * N)

let p be Real; :: thesis: ( 0 < p & p < 1 & u in (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) implies (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) )

assume that

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

A4: u in (r * M) + ((1 - r) * N) and

A5: v in (r * M) + ((1 - r) * N) ; :: thesis: (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N)

A6: u in { (x1 + y1) where x1, y1 is VECTOR of V : ( x1 in r * M & y1 in (1 - r) * N ) } by A4, RUSUB_4:def 9;

v in { (x2 + y2) where x2, y2 is VECTOR of V : ( x2 in r * M & y2 in (1 - r) * N ) } by A5, RUSUB_4:def 9;

then consider x2, y2 being VECTOR of V such that

A7: v = x2 + y2 and

A8: x2 in r * M and

A9: y2 in (1 - r) * N ;

consider x1, y1 being VECTOR of V such that

A10: u = x1 + y1 and

A11: x1 in r * M and

A12: y1 in (1 - r) * N by A6;

consider mx2 being VECTOR of V such that

A13: x2 = r * mx2 and

A14: mx2 in M by A8;

consider mx1 being VECTOR of V such that

A15: x1 = r * mx1 and

A16: mx1 in M by A11;

A17: (p * x1) + ((1 - p) * x2) = ((p * r) * mx1) + ((1 - p) * (r * mx2)) by A15, A13, RLVECT_1:def 7

.= ((p * r) * mx1) + (((1 - p) * r) * mx2) by RLVECT_1:def 7

.= (r * (p * mx1)) + (((1 - p) * r) * mx2) by RLVECT_1:def 7

.= (r * (p * mx1)) + (r * ((1 - p) * mx2)) by RLVECT_1:def 7

.= r * ((p * mx1) + ((1 - p) * mx2)) by RLVECT_1:def 5 ;

consider ny2 being VECTOR of V such that

A18: y2 = (1 - r) * ny2 and

A19: ny2 in N by A9;

consider ny1 being VECTOR of V such that

A20: y1 = (1 - r) * ny1 and

A21: ny1 in N by A12;

A22: (p * y1) + ((1 - p) * y2) = ((p * (1 - r)) * ny1) + ((1 - p) * ((1 - r) * ny2)) by A20, A18, RLVECT_1:def 7

.= ((p * (1 - r)) * ny1) + (((1 - p) * (1 - r)) * ny2) by RLVECT_1:def 7

.= ((1 - r) * (p * ny1)) + (((1 - p) * (1 - r)) * ny2) by RLVECT_1:def 7

.= ((1 - r) * (p * ny1)) + ((1 - r) * ((1 - p) * ny2)) by RLVECT_1:def 7

.= (1 - r) * ((p * ny1) + ((1 - p) * ny2)) by RLVECT_1:def 5 ;

(p * ny1) + ((1 - p) * ny2) in N by A2, A3, A21, A19;

then A23: (p * y1) + ((1 - p) * y2) in (1 - r) * N by A22;

(p * mx1) + ((1 - p) * mx2) in M by A1, A3, A16, A14;

then A24: (p * x1) + ((1 - p) * x2) in { (r * w) where w is VECTOR of V : w in M } by A17;

(p * u) + ((1 - p) * v) = ((p * x1) + (p * y1)) + ((1 - p) * (x2 + y2)) by A10, A7, RLVECT_1:def 5

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

.= (((p * x1) + (p * y1)) + ((1 - p) * x2)) + ((1 - p) * y2) by RLVECT_1:def 3

.= (((p * x1) + ((1 - p) * x2)) + (p * y1)) + ((1 - p) * y2) by RLVECT_1:def 3

.= ((p * x1) + ((1 - p) * x2)) + ((p * y1) + ((1 - p) * y2)) by RLVECT_1:def 3 ;

then (p * u) + ((1 - p) * v) in { (w1 + w2) where w1, w2 is VECTOR of V : ( w1 in r * M & w2 in (1 - r) * N ) } by A24, A23;

hence (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) by RUSUB_4:def 9; :: thesis: verum

for r being Real holds (r * M) + ((1 - r) * N) is convex

let M, N be Subset of V; :: thesis: ( M is convex & N is convex implies for r being Real holds (r * M) + ((1 - r) * N) is convex )

assume that

A1: M is convex and

A2: N is convex ; :: thesis: for r being Real holds (r * M) + ((1 - r) * N) is convex

let r be Real; :: thesis: (r * M) + ((1 - r) * N) 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 (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) holds

(r * u) + ((1 - r) * v) in (r * M) + ((1 - r) * N)

let p be Real; :: thesis: ( 0 < p & p < 1 & u in (r * M) + ((1 - r) * N) & v in (r * M) + ((1 - r) * N) implies (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) )

assume that

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

A4: u in (r * M) + ((1 - r) * N) and

A5: v in (r * M) + ((1 - r) * N) ; :: thesis: (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N)

A6: u in { (x1 + y1) where x1, y1 is VECTOR of V : ( x1 in r * M & y1 in (1 - r) * N ) } by A4, RUSUB_4:def 9;

v in { (x2 + y2) where x2, y2 is VECTOR of V : ( x2 in r * M & y2 in (1 - r) * N ) } by A5, RUSUB_4:def 9;

then consider x2, y2 being VECTOR of V such that

A7: v = x2 + y2 and

A8: x2 in r * M and

A9: y2 in (1 - r) * N ;

consider x1, y1 being VECTOR of V such that

A10: u = x1 + y1 and

A11: x1 in r * M and

A12: y1 in (1 - r) * N by A6;

consider mx2 being VECTOR of V such that

A13: x2 = r * mx2 and

A14: mx2 in M by A8;

consider mx1 being VECTOR of V such that

A15: x1 = r * mx1 and

A16: mx1 in M by A11;

A17: (p * x1) + ((1 - p) * x2) = ((p * r) * mx1) + ((1 - p) * (r * mx2)) by A15, A13, RLVECT_1:def 7

.= ((p * r) * mx1) + (((1 - p) * r) * mx2) by RLVECT_1:def 7

.= (r * (p * mx1)) + (((1 - p) * r) * mx2) by RLVECT_1:def 7

.= (r * (p * mx1)) + (r * ((1 - p) * mx2)) by RLVECT_1:def 7

.= r * ((p * mx1) + ((1 - p) * mx2)) by RLVECT_1:def 5 ;

consider ny2 being VECTOR of V such that

A18: y2 = (1 - r) * ny2 and

A19: ny2 in N by A9;

consider ny1 being VECTOR of V such that

A20: y1 = (1 - r) * ny1 and

A21: ny1 in N by A12;

A22: (p * y1) + ((1 - p) * y2) = ((p * (1 - r)) * ny1) + ((1 - p) * ((1 - r) * ny2)) by A20, A18, RLVECT_1:def 7

.= ((p * (1 - r)) * ny1) + (((1 - p) * (1 - r)) * ny2) by RLVECT_1:def 7

.= ((1 - r) * (p * ny1)) + (((1 - p) * (1 - r)) * ny2) by RLVECT_1:def 7

.= ((1 - r) * (p * ny1)) + ((1 - r) * ((1 - p) * ny2)) by RLVECT_1:def 7

.= (1 - r) * ((p * ny1) + ((1 - p) * ny2)) by RLVECT_1:def 5 ;

(p * ny1) + ((1 - p) * ny2) in N by A2, A3, A21, A19;

then A23: (p * y1) + ((1 - p) * y2) in (1 - r) * N by A22;

(p * mx1) + ((1 - p) * mx2) in M by A1, A3, A16, A14;

then A24: (p * x1) + ((1 - p) * x2) in { (r * w) where w is VECTOR of V : w in M } by A17;

(p * u) + ((1 - p) * v) = ((p * x1) + (p * y1)) + ((1 - p) * (x2 + y2)) by A10, A7, RLVECT_1:def 5

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

.= (((p * x1) + (p * y1)) + ((1 - p) * x2)) + ((1 - p) * y2) by RLVECT_1:def 3

.= (((p * x1) + ((1 - p) * x2)) + (p * y1)) + ((1 - p) * y2) by RLVECT_1:def 3

.= ((p * x1) + ((1 - p) * x2)) + ((p * y1) + ((1 - p) * y2)) by RLVECT_1:def 3 ;

then (p * u) + ((1 - p) * v) in { (w1 + w2) where w1, w2 is VECTOR of V : ( w1 in r * M & w2 in (1 - r) * N ) } by A24, A23;

hence (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) by RUSUB_4:def 9; :: thesis: verum