let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; for M1, M2 being Subset of V
for r1, r2 being Real st M1 is convex & M2 is convex holds
(r1 * M1) + (r2 * M2) is convex
let M1, M2 be Subset of V; for r1, r2 being Real st M1 is convex & M2 is convex holds
(r1 * M1) + (r2 * M2) is convex
let r1, r2 be Real; ( M1 is convex & M2 is convex implies (r1 * M1) + (r2 * M2) is convex )
assume that
A1:
M1 is convex
and
A2:
M2 is convex
; (r1 * M1) + (r2 * M2) is convex
let u, v be VECTOR of V; CONVEX1:def 2 for r being Real st 0 < r & r < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) holds
(r * u) + ((1 - r) * v) in (r1 * M1) + (r2 * M2)
let p be Real; ( 0 < p & p < 1 & u in (r1 * M1) + (r2 * M2) & v in (r1 * M1) + (r2 * M2) implies (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2) )
assume that
A3:
( 0 < p & p < 1 )
and
A4:
u in (r1 * M1) + (r2 * M2)
and
A5:
v in (r1 * M1) + (r2 * M2)
; (p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2)
v in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) }
by A5, RUSUB_4:def 9;
then consider v1, v2 being VECTOR of V such that
A6:
v = v1 + v2
and
A7:
v1 in r1 * M1
and
A8:
v2 in r2 * M2
;
u in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) }
by A4, RUSUB_4:def 9;
then consider u1, u2 being VECTOR of V such that
A9:
u = u1 + u2
and
A10:
u1 in r1 * M1
and
A11:
u2 in r2 * M2
;
consider y1 being VECTOR of V such that
A12:
v1 = r1 * y1
and
A13:
y1 in M1
by A7;
consider x1 being VECTOR of V such that
A14:
u1 = r1 * x1
and
A15:
x1 in M1
by A10;
A16: (p * u1) + ((1 - p) * v1) =
((r1 * p) * x1) + ((1 - p) * (r1 * y1))
by A14, A12, RLVECT_1:def 7
.=
((r1 * p) * x1) + ((r1 * (1 - p)) * y1)
by RLVECT_1:def 7
.=
(r1 * (p * x1)) + ((r1 * (1 - p)) * y1)
by RLVECT_1:def 7
.=
(r1 * (p * x1)) + (r1 * ((1 - p) * y1))
by RLVECT_1:def 7
.=
r1 * ((p * x1) + ((1 - p) * y1))
by RLVECT_1:def 5
;
consider y2 being VECTOR of V such that
A17:
v2 = r2 * y2
and
A18:
y2 in M2
by A8;
consider x2 being VECTOR of V such that
A19:
u2 = r2 * x2
and
A20:
x2 in M2
by A11;
A21: (p * u2) + ((1 - p) * v2) =
((r2 * p) * x2) + ((1 - p) * (r2 * y2))
by A19, A17, RLVECT_1:def 7
.=
((r2 * p) * x2) + ((r2 * (1 - p)) * y2)
by RLVECT_1:def 7
.=
(r2 * (p * x2)) + ((r2 * (1 - p)) * y2)
by RLVECT_1:def 7
.=
(r2 * (p * x2)) + (r2 * ((1 - p) * y2))
by RLVECT_1:def 7
.=
r2 * ((p * x2) + ((1 - p) * y2))
by RLVECT_1:def 5
;
(p * x2) + ((1 - p) * y2) in M2
by A2, A3, A20, A18;
then A22:
(p * u2) + ((1 - p) * v2) in r2 * M2
by A21;
(p * x1) + ((1 - p) * y1) in M1
by A1, A3, A15, A13;
then A23:
(p * u1) + ((1 - p) * v1) in { (r1 * x) where x is VECTOR of V : x in M1 }
by A16;
(p * (u1 + u2)) + ((1 - p) * (v1 + v2)) =
((p * u1) + (p * u2)) + ((1 - p) * (v1 + v2))
by RLVECT_1:def 5
.=
((p * u1) + (p * u2)) + (((1 - p) * v1) + ((1 - p) * v2))
by RLVECT_1:def 5
.=
(((p * u1) + (p * u2)) + ((1 - p) * v1)) + ((1 - p) * v2)
by RLVECT_1:def 3
.=
(((p * u1) + ((1 - p) * v1)) + (p * u2)) + ((1 - p) * v2)
by RLVECT_1:def 3
.=
((p * u1) + ((1 - p) * v1)) + ((p * u2) + ((1 - p) * v2))
by RLVECT_1:def 3
;
then
(p * (u1 + u2)) + ((1 - p) * (v1 + v2)) in { (x + y) where x, y is VECTOR of V : ( x in r1 * M1 & y in r2 * M2 ) }
by A23, A22;
hence
(p * u) + ((1 - p) * v) in (r1 * M1) + (r2 * M2)
by A9, A6, RUSUB_4:def 9; verum