let E be RealNormSpace; for r being Real
for z, y1, y2 being Point of E st y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) holds
[.y1,y2.] c= cl_Ball (z,r)
let r be Real; for z, y1, y2 being Point of E st y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) holds
[.y1,y2.] c= cl_Ball (z,r)
let z, y1, y2 be Point of E; ( y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) implies [.y1,y2.] c= cl_Ball (z,r) )
assume A1:
( y1 in cl_Ball (z,r) & y2 in cl_Ball (z,r) )
; [.y1,y2.] c= cl_Ball (z,r)
then A2:
ex y1q being Element of E st
( y1 = y1q & ||.(z - y1q).|| <= r )
;
A3:
ex y2q being Element of E st
( y2 = y2q & ||.(z - y2q).|| <= r )
by A1;
A4:
[.y1,y2.] = { (((1 - r) * y1) + (r * y2)) where r is Real : ( 0 <= r & r <= 1 ) }
by RLTOPSP1:def 2;
let s be object ; TARSKI:def 3 ( not s in [.y1,y2.] or s in cl_Ball (z,r) )
assume
s in [.y1,y2.]
; s in cl_Ball (z,r)
then consider p being Real such that
A5:
( s = ((1 - p) * y1) + (p * y2) & 0 <= p & p <= 1 )
by A4;
reconsider w = s as Point of E by A5;
((1 - p) * z) + (p * z) =
((1 - p) + p) * z
by RLVECT_1:def 6
.=
z
by RLVECT_1:def 8
;
then z - w =
((((1 - p) * z) + (p * z)) - ((1 - p) * y1)) - (p * y2)
by A5, RLVECT_1:27
.=
((((1 - p) * z) + (- ((1 - p) * y1))) + (p * z)) - (p * y2)
by RLVECT_1:def 3
.=
(((1 - p) * z) - ((1 - p) * y1)) + ((p * z) + (- (p * y2)))
by RLVECT_1:def 3
.=
((1 - p) * (z - y1)) + ((p * z) - (p * y2))
by RLVECT_1:34
.=
((1 - p) * (z - y1)) + (p * (z - y2))
by RLVECT_1:34
;
then
||.(z - w).|| <= ||.((1 - p) * (z - y1)).|| + ||.(p * (z - y2)).||
by NORMSP_1:def 1;
then
||.(z - w).|| <= (|.(1 - p).| * ||.(z - y1).||) + ||.(p * (z - y2)).||
by NORMSP_1:def 1;
then A7:
||.(z - w).|| <= (|.(1 - p).| * ||.(z - y1).||) + (|.p.| * ||.(z - y2).||)
by NORMSP_1:def 1;
A8:
( |.(1 - p).| = 1 - p & |.p.| = p )
by A5, COMPLEX1:43, XREAL_1:48;
0 <= 1 - p
by A5, XREAL_1:48;
then A9:
(1 - p) * ||.(z - y1).|| <= (1 - p) * r
by A2, XREAL_1:64;
p * ||.(z - y2).|| <= p * r
by A3, A5, XREAL_1:64;
then
((1 - p) * ||.(z - y1).||) + (p * ||.(z - y2).||) <= ((1 - p) * r) + (p * r)
by A9, XREAL_1:7;
then
||.(z - w).|| <= ((1 - p) * r) + (p * r)
by A7, A8, XXREAL_0:2;
hence
s in cl_Ball (z,r)
; verum