let V be non empty Abelian add-associative ComplexLinearSpace-like CLSStruct ; :: thesis: for M, N being Subset of V st M is convex & N is convex holds
for z being Complex st ex r being Real st z = r holds
(z * M) + ((1r - z) * N) is convex
let M, N be Subset of V; :: thesis: ( M is convex & N is convex implies for z being Complex st ex r being Real st z = r holds
(z * M) + ((1r - z) * N) is convex )
assume A1: ( M is convex & N is convex ) ; :: thesis: for z being Complex st ex r being Real st z = r holds
(z * M) + ((1r - z) * N) is convex
let z be Complex; :: thesis: ( ex r being Real st z = r implies (z * M) + ((1r - z) * N) is convex )
assume ex r being Real st z = r ; :: thesis: (z * M) + ((1r - z) * N) is convex
let u, v be VECTOR of V; :: according to CONVEX4:def 23 :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & u in (z * M) + ((1r - z) * N) & v in (z * M) + ((1r - z) * N) holds
(z * u) + ((1r - z) * v) in (z * M) + ((1r - z) * N)
let s be Complex; :: thesis: ( ex r being Real st
( s = r & 0 < r & r < 1 ) & u in (z * M) + ((1r - z) * N) & v in (z * M) + ((1r - z) * N) implies (s * u) + ((1r - s) * v) in (z * M) + ((1r - z) * N) )
assume that
A3: ex p being Real st
( s = p & 0 < p & p < 1 ) and
A4: ( u in (z * M) + ((1r - z) * N) & v in (z * M) + ((1r - z) * N) ) ; :: thesis: (s * u) + ((1r - s) * v) in (z * M) + ((1r - z) * N)
consider x1, y1 being VECTOR of V such that
A6: ( u = x1 + y1 & x1 in z * M & y1 in (1r - z) * N ) by A4;
consider x2, y2 being VECTOR of V such that
A7: ( v = x2 + y2 & x2 in z * M & y2 in (1r - z) * N ) by A4;
consider mx1 being VECTOR of V such that
A8: ( x1 = z * mx1 & mx1 in M ) by A6;
consider ny1 being VECTOR of V such that
A9: ( y1 = (1r - z) * ny1 & ny1 in N ) by A6;
consider mx2 being VECTOR of V such that
A10: ( x2 = z * mx2 & mx2 in M ) by A7;
consider ny2 being VECTOR of V such that
A11: ( y2 = (1r - z) * ny2 & ny2 in N ) by A7;
A12: ( (s * mx1) + ((1r - s) * mx2) in M & (s * ny1) + ((1r - s) * ny2) in N ) by A1, A3, A8, A9, A10, A11, Def202;
(s * x1) + ((1r - s) * x2) = ((s * z) * mx1) + ((1r - s) * (z * mx2)) by A8, A10, CLVECT_1:def 2
.= ((s * z) * mx1) + (((1r - s) * z) * mx2) by CLVECT_1:def 2
.= (z * (s * mx1)) + (((1r - s) * z) * mx2) by CLVECT_1:def 2
.= (z * (s * mx1)) + (z * ((1r - s) * mx2)) by CLVECT_1:def 2
.= z * ((s * mx1) + ((1r - s) * mx2)) by CLVECT_1:def 2 ;
then A14: (s * x1) + ((1r - s) * x2) in z * M by A12;
(s * y1) + ((1r - s) * y2) = ((s * (1r - z)) * ny1) + ((1r - s) * ((1r - z) * ny2)) by A9, A11, CLVECT_1:def 2
.= ((s * (1r - z)) * ny1) + (((1r - s) * (1r - z)) * ny2) by CLVECT_1:def 2
.= ((1r - z) * (s * ny1)) + (((1r - s) * (1r - z)) * ny2) by CLVECT_1:def 2
.= ((1r - z) * (s * ny1)) + ((1r - z) * ((1r - s) * ny2)) by CLVECT_1:def 2
.= (1r - z) * ((s * ny1) + ((1r - s) * ny2)) by CLVECT_1:def 2 ;
then A15: (s * y1) + ((1r - s) * y2) in (1r - z) * N by A12;
(s * u) + ((1r - s) * v) = ((s * x1) + (s * y1)) + ((1r - s) * (x2 + y2)) by A6, A7, CLVECT_1:def 2
.= ((s * x1) + (s * y1)) + (((1r - s) * x2) + ((1r - s) * y2)) by CLVECT_1:def 2
.= (((s * x1) + (s * y1)) + ((1r - s) * x2)) + ((1r - s) * y2) by RLVECT_1:def 6
.= (((s * x1) + ((1r - s) * x2)) + (s * y1)) + ((1r - s) * y2) by RLVECT_1:def 6
.= ((s * x1) + ((1r - s) * x2)) + ((s * y1) + ((1r - s) * y2)) by RLVECT_1:def 6 ;
hence (s * u) + ((1r - s) * v) in (z * M) + ((1r - z) * N) by A14, A15; :: thesis: verum