let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; 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; ( 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
; for r being Real holds (r * M) + ((1 - r) * N) is convex
let r be Real; (r * M) + ((1 - r) * N) is convex
let u, v be VECTOR of V; CONVEX1:def 2 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; ( 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)
; (p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N)
A6:
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 9;
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 9;
then consider x2, y2 being VECTOR of V such that
A7:
v = x2 + y2
and
A8:
x2 in r * M
and
A9:
y2 in (1 - r) * N
;
consider x1, y1 being VECTOR of V such that
A10:
u = x1 + y1
and
A11:
x1 in r * M
and
A12:
y1 in (1 - r) * N
by A6;
consider mx2 being VECTOR of V such that
A13:
x2 = r * mx2
and
A14:
mx2 in M
by A8;
consider mx1 being VECTOR of V such that
A15:
x1 = r * mx1
and
A16:
mx1 in M
by A11;
A17: (p * x1) + ((1 - p) * x2) =
((p * r) * mx1) + ((1 - p) * (r * mx2))
by A15, A13, RLVECT_1:def 7
.=
((p * r) * mx1) + (((1 - p) * r) * mx2)
by RLVECT_1:def 7
.=
(r * (p * mx1)) + (((1 - p) * r) * mx2)
by RLVECT_1:def 7
.=
(r * (p * mx1)) + (r * ((1 - p) * mx2))
by RLVECT_1:def 7
.=
r * ((p * mx1) + ((1 - p) * mx2))
by RLVECT_1:def 5
;
consider ny2 being VECTOR of V such that
A18:
y2 = (1 - r) * ny2
and
A19:
ny2 in N
by A9;
consider ny1 being VECTOR of V such that
A20:
y1 = (1 - r) * ny1
and
A21:
ny1 in N
by A12;
A22: (p * y1) + ((1 - p) * y2) =
((p * (1 - r)) * ny1) + ((1 - p) * ((1 - r) * ny2))
by A20, A18, RLVECT_1:def 7
.=
((p * (1 - r)) * ny1) + (((1 - p) * (1 - r)) * ny2)
by RLVECT_1:def 7
.=
((1 - r) * (p * ny1)) + (((1 - p) * (1 - r)) * ny2)
by RLVECT_1:def 7
.=
((1 - r) * (p * ny1)) + ((1 - r) * ((1 - p) * ny2))
by RLVECT_1:def 7
.=
(1 - r) * ((p * ny1) + ((1 - p) * ny2))
by RLVECT_1:def 5
;
(p * ny1) + ((1 - p) * ny2) in N
by A2, A3, A21, A19;
then A23:
(p * y1) + ((1 - p) * y2) in (1 - r) * N
by A22;
(p * mx1) + ((1 - p) * mx2) in M
by A1, A3, A16, A14;
then A24:
(p * x1) + ((1 - p) * x2) in { (r * w) where w is VECTOR of V : w in M }
by A17;
(p * u) + ((1 - p) * v) =
((p * x1) + (p * y1)) + ((1 - p) * (x2 + y2))
by A10, A7, RLVECT_1:def 5
.=
((p * x1) + (p * y1)) + (((1 - p) * x2) + ((1 - p) * y2))
by RLVECT_1:def 5
.=
(((p * x1) + (p * y1)) + ((1 - p) * x2)) + ((1 - p) * y2)
by RLVECT_1:def 3
.=
(((p * x1) + ((1 - p) * x2)) + (p * y1)) + ((1 - p) * y2)
by RLVECT_1:def 3
.=
((p * x1) + ((1 - p) * x2)) + ((p * y1) + ((1 - p) * y2))
by RLVECT_1:def 3
;
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 A24, A23;
hence
(p * u) + ((1 - p) * v) in (r * M) + ((1 - r) * N)
by RUSUB_4:def 9; verum