let V be non empty Abelian add-associative RealLinearSpace-like 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)
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 10;
then consider x1, y1 being VECTOR of V such that
A6: ( u = x1 + y1 & x1 in r * M & y1 in (1 - r) * N ) ;
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 10;
then consider x2, y2 being VECTOR of V such that
A7: ( v = x2 + y2 & x2 in r * M & y2 in (1 - r) * N ) ;
consider mx1 being VECTOR of V such that
A8: ( x1 = r * mx1 & mx1 in M ) by A6;
consider ny1 being VECTOR of V such that
A9: ( y1 = (1 - r) * ny1 & ny1 in N ) by A6;
consider mx2 being VECTOR of V such that
A10: ( x2 = r * mx2 & mx2 in M ) by A7;
consider ny2 being VECTOR of V such that
A11: ( y2 = (1 - r) * ny2 & ny2 in N ) by A7;
A12: (p * mx1) + ((1 - p) * mx2) in M by A1, A3, A8, A10, Def2;
A13: (p * ny1) + ((1 - p) * ny2) in N by A2, A3, A9, A11, Def2;
(p * x1) + ((1 - p) * x2) = ((p * r) * mx1) + ((1 - p) * (r * mx2)) by A8, A10, RLVECT_1:def 9
.= ((p * r) * mx1) + (((1 - p) * r) * mx2) by RLVECT_1:def 9
.= (r * (p * mx1)) + (((1 - p) * r) * mx2) by RLVECT_1:def 9
.= (r * (p * mx1)) + (r * ((1 - p) * mx2)) by RLVECT_1:def 9
.= r * ((p * mx1) + ((1 - p) * mx2)) by RLVECT_1:def 9 ;
then A14: (p * x1) + ((1 - p) * x2) in { (r * w) where w is VECTOR of V : w in M } by A12;
(p * y1) + ((1 - p) * y2) = ((p * (1 - r)) * ny1) + ((1 - p) * ((1 - r) * ny2)) by A9, A11, RLVECT_1:def 9
.= ((p * (1 - r)) * ny1) + (((1 - p) * (1 - r)) * ny2) by RLVECT_1:def 9
.= ((1 - r) * (p * ny1)) + (((1 - p) * (1 - r)) * ny2) by RLVECT_1:def 9
.= ((1 - r) * (p * ny1)) + ((1 - r) * ((1 - p) * ny2)) by RLVECT_1:def 9
.= (1 - r) * ((p * ny1) + ((1 - p) * ny2)) by RLVECT_1:def 9 ;
then A15: (p * y1) + ((1 - p) * y2) in (1 - r) * N by A13;
(p * u) + ((1 - p) * v) = ((p * x1) + (p * y1)) + ((1 - p) * (x2 + y2)) by A6, A7, RLVECT_1:def 9
.= ((p * x1) + (p * y1)) + (((1 - p) * x2) + ((1 - p) * y2)) by RLVECT_1:def 9
.= (((p * x1) + (p * y1)) + ((1 - p) * x2)) + ((1 - p) * y2) by RLVECT_1:def 6
.= (((p * x1) + ((1 - p) * x2)) + (p * y1)) + ((1 - p) * y2) by RLVECT_1:def 6
.= ((p * x1) + ((1 - p) * x2)) + ((p * y1) + ((1 - p) * y2)) by RLVECT_1:def 6 ;
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 A14, A15;
hence (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N) by RUSUB_4:def 10; :: thesis: verum