let X be RealLinearSpace; :: thesis: for M being Subset of X
for r being Real holds r * (conv M) = conv (r * M)
let M be Subset of X; :: thesis: for r being Real holds r * (conv M) = conv (r * M)
let r be Real; :: thesis: r * (conv M) = conv (r * M)
thus r * (conv M) c= conv (r * M) :: according to XBOOLE_0:def 10 :: thesis: conv (r * M) c= r * (conv M)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

per cases ( r = 0 or r <> 0 ) ;

suppose A1: r = 0 ; :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

per cases ( M = {} or M <> {} ) ;

suppose M = {} ; :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

hence ( not x in r * (conv M) or x in conv (r * M) ) by CONVEX1:33; :: thesis: verum

end;

suppose A2: M <> {} ; :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

then conv M <> {} by CONVEX1:41, XBOOLE_1:3;
then A3: r * (conv M) = {(0. X)} by A1, CONVEX1:34;
r * M = {(0. X)} by A1, A2, CONVEX1:34;
then {(0. X)} c= conv (r * M) by CONVEX1:41;
hence ( not x in r * (conv M) or x in conv (r * M) ) by A3; :: thesis: verum

end;

end;

end;

suppose A4: r <> 0 ; :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

assume x in r * (conv M) ; :: thesis: x in conv (r * M)
then consider v being Point of X such that
A5: x = r * v and
A6: v in conv M ;
A8: for V being set st V in Convex-Family (r * M) holds
r * v in V

proof

let V be set ; :: thesis: ( V in Convex-Family (r * M) implies r * v in V )
assume A9: V in Convex-Family (r * M) ; :: thesis: r * v in V
then reconsider V = V as Subset of X ;
A10: V is convex by A9, CONVEX1:def 4;
r * M c= V by A9, CONVEX1:def 4;
then (r " ) * (r * M) c= (r " ) * V by CONVEX1:39;
then ((r " ) * r) * M c= (r " ) * V by CONVEX1:37;
then 1 * M c= (r " ) * V by A4, XCMPLX_0:def 7;
then A11: M c= (r " ) * V by CONVEX1:32;
(r " ) * V is convex by A10, CONVEX1:1;
then (r " ) * V in Convex-Family M by A11, CONVEX1:def 4;
then v in (r " ) * V by A6, SETFAM_1:def 1;
then consider w being Point of X such that
A12: v = (r " ) * w and
A13: w in V ;
r * v = (r * (r " )) * w by A12, RLVECT_1:def 9
.= 1 * w by A4, XCMPLX_0:def 7
.= w by RLVECT_1:def 9 ;
hence r * v in V by A13; :: thesis: verum

end;

thus x in conv (r * M) by A5, A8, SETFAM_1:def 1; :: thesis: verum

end;

end;

end;

A14: r * M c= r * (conv M) by CONVEX1:39, CONVEX1:41;
r * (conv M) is convex by CONVEX1:1;
hence conv (r * M) c= r * (conv M) by A14, CONVEX1:30; :: thesis: verum