let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; 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; ( 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
; for z being Complex holds (z * M) + ((1r - z) * N) is convex
let z be Complex; (z * M) + ((1r - z) * N) is convex
let u, v be VECTOR of V; CONVEX4:def 23 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; ( 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)
; (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; verum