let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; :: thesis: for M, N being Subset of V st M is convex & N is convex holds
for z being Complex 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 holds (z * M) + ((1r - z) * N) is convex )
assume that
A1: M is convex and
A2: N is convex ; :: thesis: for z being Complex holds (z * M) + ((1r - z) * N) is convex
let z be Complex; :: 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) and
A5: v in (z * M) + ((1r - z) * N) ; :: thesis: (s * u) + ((1r - s) * v) in (z * M) + ((1r - z) * N)
consider x2, y2 being VECTOR of V such that
A6: v = x2 + y2 and
A7: x2 in z * M and
A8: y2 in (1r - z) * N by A5;
consider x1, y1 being VECTOR of V such that
A9: u = x1 + y1 and
A10: x1 in z * M and
A11: y1 in (1r - z) * N by A4;
consider mx2 being VECTOR of V such that
A12: x2 = z * mx2 and
A13: mx2 in M by A7;
consider mx1 being VECTOR of V such that
A14: x1 = z * mx1 and
A15: mx1 in M by A10;
A16: (s * x1) + ((1r - s) * x2) = ((s * z) * mx1) + ((1r - s) * (z * mx2)) by A14, A12, CLVECT_1:def 4
.= ((s * z) * mx1) + (((1r - s) * z) * mx2) by CLVECT_1:def 4
.= (z * (s * mx1)) + (((1r - s) * z) * mx2) by CLVECT_1:def 4
.= (z * (s * mx1)) + (z * ((1r - s) * mx2)) by CLVECT_1:def 4
.= z * ((s * mx1) + ((1r - s) * mx2)) by CLVECT_1:def 2 ;
consider ny2 being VECTOR of V such that
A17: y2 = (1r - z) * ny2 and
A18: ny2 in N by A8;
consider ny1 being VECTOR of V such that
A19: y1 = (1r - z) * ny1 and
A20: ny1 in N by A11;
A21: (s * y1) + ((1r - s) * y2) = ((s * (1r - z)) * ny1) + ((1r - s) * ((1r - z) * ny2)) by A19, A17, CLVECT_1:def 4
.= ((s * (1r - z)) * ny1) + (((1r - s) * (1r - z)) * ny2) by CLVECT_1:def 4
.= ((1r - z) * (s * ny1)) + (((1r - s) * (1r - z)) * ny2) by CLVECT_1:def 4
.= ((1r - z) * (s * ny1)) + ((1r - z) * ((1r - s) * ny2)) by CLVECT_1:def 4
.= (1r - z) * ((s * ny1) + ((1r - s) * ny2)) by CLVECT_1:def 2 ;
(s * ny1) + ((1r - s) * ny2) in N by A2, A3, A20, A18;
then A22: (s * y1) + ((1r - s) * y2) in (1r - z) * N by A21;
(s * mx1) + ((1r - s) * mx2) in M by A1, A3, A15, A13;
then A23: (s * x1) + ((1r - s) * x2) in z * M by A16;
(s * u) + ((1r - s) * v) = ((s * x1) + (s * y1)) + ((1r - s) * (x2 + y2)) by A9, A6, 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 3
.= (((s * x1) + ((1r - s) * x2)) + (s * y1)) + ((1r - s) * y2) by RLVECT_1:def 3
.= ((s * x1) + ((1r - s) * x2)) + ((s * y1) + ((1r - s) * y2)) by RLVECT_1:def 3 ;
hence (s * u) + ((1r - s) * v) in (z * M) + ((1r - z) * N) by A23, A22; :: thesis: verum