let t, s be Real; :: thesis: for n being Element of NAT
for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
let n be Element of NAT ; :: thesis: for B being Subset of (TOP-REAL n) st B is convex & 0 < t & 0 < s holds
(s + t) (.) B = (s (.) B) (+) (t (.) B)
let B be Subset of (TOP-REAL n); :: thesis: ( B is convex & 0 < t & 0 < s implies (s + t) (.) B = (s (.) B) (+) (t (.) B) )
assume that
A1: B is convex and
A2: ( 0 < t & 0 < s ) ; :: thesis: (s + t) (.) B = (s (.) B) (+) (t (.) B)
thus (s + t) (.) B c= (s (.) B) (+) (t (.) B) :: according to XBOOLE_0:def 10 :: thesis: (s (.) B) (+) (t (.) B) c= (s + t) (.) B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (s + t) (.) B or x in (s (.) B) (+) (t (.) B) )
assume x in (s + t) (.) B ; :: thesis: x in (s (.) B) (+) (t (.) B)
then consider b being Point of (TOP-REAL n) such that
A3: x = (s + t) * b and
A4: b in B ;
A5: t * b in t (.) B by A4;
( x = (s * b) + (t * b) & s * b in s (.) B ) by A3, A4, RLVECT_1:def 6;
hence x in (s (.) B) (+) (t (.) B) by A5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (s (.) B) (+) (t (.) B) or x in (s + t) (.) B )
assume x in (s (.) B) (+) (t (.) B) ; :: thesis: x in (s + t) (.) B
then consider s1, s2 being Point of (TOP-REAL n) such that
A6: x = s1 + s2 and
A7: s1 in s (.) B and
A8: s2 in t (.) B ;
consider b2 being Point of (TOP-REAL n) such that
A9: s2 = t * b2 and
A10: b2 in B by A8;
consider b1 being Point of (TOP-REAL n) such that
A11: s1 = s * b1 and
A12: b1 in B by A7;
s / (s + t) < (s + t) / (s + t) by A2, XREAL_1:29, XREAL_1:74;
then s / (s + t) < 1 by A2, XCMPLX_1:60;
then ((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2) in B by A1, A2, A12, A10;
then (s + t) * (((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2)) in { ((s + t) * zz) where zz is Point of (TOP-REAL n) : zz in B } ;
then ((s + t) * ((s / (s + t)) * b1)) + ((s + t) * ((1 - (s / (s + t))) * b2)) in (s + t) (.) B by RLVECT_1:def 5;
then (((s + t) * (s / (s + t))) * b1) + ((s + t) * ((1 - (s / (s + t))) * b2)) in (s + t) (.) B by RLVECT_1:def 7;
then (((s + t) * (s / (s + t))) * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B by RLVECT_1:def 7;
then (s * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) in (s + t) (.) B by A2, XCMPLX_1:87;
then (s * b1) + (((s + t) * (((s + t) / (s + t)) - (s / (s + t)))) * b2) in (s + t) (.) B by A2, XCMPLX_1:60;
then (s * b1) + (((s + t) * (((s + t) - s) / (s + t))) * b2) in (s + t) (.) B by XCMPLX_1:120;
hence x in (s + t) (.) B by A2, A6, A11, A9, XCMPLX_1:87; :: thesis: verum