let V be RealLinearSpace; :: thesis: for M being Subset of V
for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) c= (r1 + r2) * M
let M be Subset of V; :: thesis: for r1, r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds
(r1 * M) + (r2 * M) c= (r1 + r2) * M
let r1, r2 be Real; :: thesis: ( r1 >= 0 & r2 >= 0 & M is convex implies (r1 * M) + (r2 * M) c= (r1 + r2) * M )
assume that
A1: r1 >= 0 and
A2: r2 >= 0 and
A3: M is convex ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
per cases ( M is empty or not M is empty ) ;
suppose M is empty ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
then ( r1 * M = {} & (r1 + r2) * M = {} ) by Lm7;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by Lm8; :: thesis: verum
end;
suppose A4: not M is empty ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
per cases ( r1 = 0 or r2 = 0 or ( r1 <> 0 & r2 <> 0 ) ) ;
suppose A5: r1 = 0 ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
then r1 * M = {(0. V)} by A4, Lm2;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A5, Lm9; :: thesis: verum
end;
suppose A6: r2 = 0 ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
then r2 * M = {(0. V)} by A4, Lm2;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A6, Lm9; :: thesis: verum
end;
suppose A7: ( r1 <> 0 & r2 <> 0 ) ; :: thesis: (r1 * M) + (r2 * M) c= (r1 + r2) * M
then r1 + r2 > r1 by A2, XREAL_1:29;
then A8: r1 / (r1 + r2) < 1 by A1, XREAL_1:189;
0 < r1 / (r1 + r2) by A1, A2, A7, XREAL_1:139;
then ((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M) c= M by A3, A8, Th4;
then A9: (r1 + r2) * (((r1 / (r1 + r2)) * M) + ((1 - (r1 / (r1 + r2))) * M)) c= (r1 + r2) * M by Lm6;
1 - (r1 / (r1 + r2)) = ((r1 + r2) / (r1 + r2)) - (r1 / (r1 + r2)) by A1, A2, A7, XCMPLX_1:60
.= ((r1 + r2) - r1) / (r1 + r2) by XCMPLX_1:120
.= r2 / (r1 + r2) ;
then A10: (r1 + r2) * ((1 - (r1 / (r1 + r2))) * M) = ((r2 / (r1 + r2)) * (r1 + r2)) * M by Lm4
.= r2 * M by A1, A2, A7, XCMPLX_1:87 ;
(r1 + r2) * ((r1 / (r1 + r2)) * M) = ((r1 / (r1 + r2)) * (r1 + r2)) * M by Lm4
.= r1 * M by A1, A2, A7, XCMPLX_1:87 ;
hence (r1 * M) + (r2 * M) c= (r1 + r2) * M by A9, A10, Lm5; :: thesis: verum
end;
end;
end;
end;