let n be Nat; :: thesis: for a, b, r being Real
for x, y, z being Point of (TOP-REAL n) st a + b = 1 & |.a.| + |.b.| = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds
(a * x) + (b * y) in Ball (z,r)
let a, b, r be Real; :: thesis: for x, y, z being Point of (TOP-REAL n) st a + b = 1 & |.a.| + |.b.| = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds
(a * x) + (b * y) in Ball (z,r)
let x, y, z be Point of (TOP-REAL n); :: thesis: ( a + b = 1 & |.a.| + |.b.| = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) implies (a * x) + (b * y) in Ball (z,r) )
assume that
A1: a + b = 1 and
A2: |.a.| + |.b.| = 1 and
A3: b <> 0 and
A4: x in cl_Ball (z,r) and
A5: y in Ball (z,r) ; :: thesis: (a * x) + (b * y) in Ball (z,r)
|.(y - z).| < r by A5, Th5;
then A6: |.(z - y).| < r by TOPRNS_1:27;
|.(x - z).| <= r by A4, Th6;
then ( 0 <= |.a.| & |.(z - x).| <= r ) by COMPLEX1:46, TOPRNS_1:27;
then A7: |.a.| * |.(z - x).| <= |.a.| * r by XREAL_1:64;
0 < |.b.| by A3, COMPLEX1:47;
then |.b.| * |.(z - y).| < |.b.| * r by A6, XREAL_1:68;
then (|.a.| * |.(z - x).|) + (|.b.| * |.(z - y).|) < (|.a.| * r) + (|.b.| * r) by A7, XREAL_1:8;
then ( a is Real & (|.a.| * |.(z - x).|) + (|.b.| * |.(z - y).|) < (|.a.| + |.b.|) * r ) ;
then ( b is Real & |.(a * (z - x)).| + (|.b.| * |.(z - y).|) < 1 * r ) by A2, TOPRNS_1:7;
then A8: |.(a * (z - x)).| + |.(b * (z - y)).| < r by TOPRNS_1:7;
|.(((a * z) + (b * z)) - ((a * x) + (b * y))).| = |.(((a * z) - ((a * x) + (b * y))) + (b * z)).| by RLVECT_1:def 3
.= |.((((a * z) - (a * x)) - (b * y)) + (b * z)).| by RLVECT_1:27
.= |.((((a * z) - (a * x)) + (b * z)) - (b * y)).| by RLVECT_1:def 3
.= |.(((a * z) - (a * x)) + ((b * z) - (b * y))).| by RLVECT_1:def 3
.= |.((a * (z - x)) + ((b * z) - (b * y))).| by RLVECT_1:34
.= |.((a * (z - x)) + (b * (z - y))).| by RLVECT_1:34 ;
then |.(((a * z) + (b * z)) - ((a * x) + (b * y))).| <= |.(a * (z - x)).| + |.(b * (z - y)).| by TOPRNS_1:29;
then |.(((a * z) + (b * z)) - ((a * x) + (b * y))).| < r by A8, XXREAL_0:2;
then A9: |.(((a * x) + (b * y)) - ((a * z) + (b * z))).| < r by TOPRNS_1:27;
(a * z) + (b * z) = (a + b) * z by RLVECT_1:def 6
.= z by A1, RLVECT_1:def 8 ;
hence (a * x) + (b * y) in Ball (z,r) by A9; :: thesis: verum