let V be ComplexLinearSpace; :: thesis: for M being Subset of V
for v being VECTOR of V holds
( M is convex iff v + M is convex )
let M be Subset of V; :: thesis: for v being VECTOR of V holds
( M is convex iff v + M is convex )
let v be VECTOR of V; :: thesis: ( M is convex iff v + M is convex )
A1: ( v + M is convex implies M is convex )

proof

assume A2: v + M is convex ; :: thesis: M is convex
let w1, w2 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 ) & w1 in M & w2 in M holds
(z * w1) + ((1r - z) * w2) in M
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & w1 in M & w2 in M implies (z * w1) + ((1r - z) * w2) in M )
assume that
A3: ex r being Real st
( z = r & 0 < r & r < 1 ) and
A4: ( w1 in M & w2 in M ) ; :: thesis: (z * w1) + ((1r - z) * w2) in M
set x1 = v + w1;
set x2 = v + w2;
( v + w1 in v + M & v + w2 in { (v + w) where w is VECTOR of V : w in M } ) by A4;
then A5: (z * (v + w1)) + ((1r - z) * (v + w2)) in v + M by A2, A3;
(z * (v + w1)) + ((1r - z) * (v + w2)) = ((z * v) + (z * w1)) + ((1r - z) * (v + w2)) by CLVECT_1:def 2
.= ((z * v) + (z * w1)) + (((1r - z) * v) + ((1r - z) * w2)) by CLVECT_1:def 2
.= (((z * v) + (z * w1)) + ((1r - z) * v)) + ((1r - z) * w2) by RLVECT_1:def 3
.= (((z * v) + ((1r - z) * v)) + (z * w1)) + ((1r - z) * w2) by RLVECT_1:def 3
.= (((z + (1r - z)) * v) + (z * w1)) + ((1r - z) * w2) by CLVECT_1:def 3
.= (v + (z * w1)) + ((1r - z) * w2) by CLVECT_1:def 5
.= v + ((z * w1) + ((1r - z) * w2)) by RLVECT_1:def 3 ;
then ex w being VECTOR of V st
( v + ((z * w1) + ((1r - z) * w2)) = v + w & w in M ) by A5;
hence (z * w1) + ((1r - z) * w2) in M by RLVECT_1:8; :: thesis: verum

end;

( M is convex implies v + M is convex )

proof

assume A6: M is convex ; :: thesis: v + M is convex
let w1, w2 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 ) & w1 in v + M & w2 in v + M holds
(z * w1) + ((1r - z) * w2) in v + M
let z be Complex; :: thesis: ( ex r being Real st
( z = r & 0 < r & r < 1 ) & w1 in v + M & w2 in v + M implies (z * w1) + ((1r - z) * w2) in v + M )
assume that
A7: ex r being Real st
( z = r & 0 < r & r < 1 ) and
A8: w1 in v + M and
A9: w2 in v + M ; :: thesis: (z * w1) + ((1r - z) * w2) in v + M
consider x2 being VECTOR of V such that
A10: w2 = v + x2 and
A11: x2 in M by A9;
consider x1 being VECTOR of V such that
A12: w1 = v + x1 and
A13: x1 in M by A8;
A14: (z * w1) + ((1r - z) * w2) = ((z * v) + (z * x1)) + ((1r - z) * (v + x2)) by A12, A10, CLVECT_1:def 2
.= ((z * v) + (z * x1)) + (((1r - z) * v) + ((1r - z) * x2)) by CLVECT_1:def 2
.= (((z * v) + (z * x1)) + ((1r - z) * v)) + ((1r - z) * x2) by RLVECT_1:def 3
.= (((z * v) + ((1r - z) * v)) + (z * x1)) + ((1r - z) * x2) by RLVECT_1:def 3
.= (((z + (1r - z)) * v) + (z * x1)) + ((1r - z) * x2) by CLVECT_1:def 3
.= (v + (z * x1)) + ((1r - z) * x2) by CLVECT_1:def 5
.= v + ((z * x1) + ((1r - z) * x2)) by RLVECT_1:def 3 ;
(z * x1) + ((1r - z) * x2) in M by A6, A7, A13, A11;
hence (z * w1) + ((1r - z) * w2) in v + M by A14; :: thesis: verum

end;

hence ( M is convex iff v + M is convex ) by A1; :: thesis: verum