let G be RealNormSpace-Sequence; for x, y, z, w being Point of (product G)
for i being Element of dom G
for d being Real
for p, q, r being Point of (G . i) st ||.(y - x).|| < d & ||.(z - x).|| < d & p = (proj i) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
||.(w - x).|| < d
let x, y, z, w be Point of (product G); for i being Element of dom G
for d being Real
for p, q, r being Point of (G . i) st ||.(y - x).|| < d & ||.(z - x).|| < d & p = (proj i) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
||.(w - x).|| < d
let i be Element of dom G; for d being Real
for p, q, r being Point of (G . i) st ||.(y - x).|| < d & ||.(z - x).|| < d & p = (proj i) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
||.(w - x).|| < d
let d be Real; for p, q, r being Point of (G . i) st ||.(y - x).|| < d & ||.(z - x).|| < d & p = (proj i) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
||.(w - x).|| < d
let p, q, r be Point of (G . i); ( ||.(y - x).|| < d & ||.(z - x).|| < d & p = (proj i) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r implies ||.(w - x).|| < d )
assume that
A1:
( ||.(y - x).|| < d & ||.(z - x).|| < d )
and
A2:
( p = (proj i) . y & z = (reproj (i,y)) . q )
and
A3:
r in [.p,q.]
and
A4:
w = (reproj (i,y)) . r
; ||.(w - x).|| < d
set wx = w - x;
set yx = y - x;
set zx = z - x;
reconsider xi = (proj i) . x as Point of (G . i) ;
r in { (((1 - t) * p) + (t * q)) where t is Real : ( 0 <= t & t <= 1 ) }
by A3, RLTOPSP1:def 2;
then consider t being Real such that
A5:
( r = ((1 - t) * p) + (t * q) & 0 <= t & t <= 1 )
;
A6:
( r = p + (t * (q - p)) & 0 <= t & t <= 1 )
by A5, Lm2;
reconsider wx0 = w - x, yx0 = y - x, zx0 = z - x as Element of product (carr G) by Th10;
reconsider Nwx = normsequence (G,wx0) as len G -element FinSequence of REAL ;
reconsider Nyx = normsequence (G,yx0) as len G -element FinSequence of REAL ;
reconsider Nzx = normsequence (G,zx0) as len G -element FinSequence of REAL ;
set tyz = ((1 - t) * (y - x)) + (t * (z - x));
reconsider tyz0 = ((1 - t) * (y - x)) + (t * (z - x)) as Element of product (carr G) by Th10;
reconsider Ntyz = normsequence (G,tyz0) as len G -element FinSequence of REAL ;
A7:
1 = (1 - t) + t
;
r =
p + ((t * q) - (t * p))
by A6, RLVECT_1:34
.=
(p + (- (t * p))) + (t * q)
by RLVECT_1:def 3
.=
((1 * p) - (t * p)) + (t * q)
by RLVECT_1:def 8
.=
((1 - t) * p) + (t * q)
by RLVECT_1:35
;
then A8: r - xi =
(((1 - t) * p) + (t * q)) - (1 * xi)
by RLVECT_1:def 8
.=
(((1 - t) * p) + (t * q)) - (((1 - t) * xi) + (t * xi))
by A7, RLVECT_1:def 6
.=
((((1 - t) * p) + (t * q)) - (t * xi)) - ((1 - t) * xi)
by RLVECT_1:27
.=
(((1 - t) * p) + ((t * q) - (t * xi))) - ((1 - t) * xi)
by RLVECT_1:28
.=
((t * q) - (t * xi)) + (((1 - t) * p) - ((1 - t) * xi))
by RLVECT_1:def 3
.=
(t * (q - xi)) + (((1 - t) * p) - ((1 - t) * xi))
by RLVECT_1:34
.=
(t * (q - xi)) + ((1 - t) * (p - xi))
by RLVECT_1:34
;
reconsider Swx = w - x as len G -element FinSequence ;
reconsider Syz = ((1 - t) * (y - x)) + (t * (z - x)) as len G -element FinSequence ;
A9:
( dom Swx = Seg (len G) & dom Syz = Seg (len G) )
by FINSEQ_1:89;
A10:
for k being Nat st k in dom Swx holds
Swx . k = Syz . k
A16:
( len Nwx = len G & len Ntyz = len G )
by CARD_1:def 7;
for k being Element of NAT st k in Seg (len Nwx) holds
( 0 <= Nwx . k & Nwx . k <= Ntyz . k )
then A19:
|.Nwx.| <= |.Ntyz.|
by A16, PRVECT_2:2;
A20:
||.(w - x).|| = (productnorm G) . (w - x)
by PRVECT_2:def 13;
||.(((1 - t) * (y - x)) + (t * (z - x))).|| =
(productnorm G) . (((1 - t) * (y - x)) + (t * (z - x)))
by PRVECT_2:def 13
.=
|.(normsequence (G,tyz0)).|
by PRVECT_2:def 12
;
then A21:
||.(w - x).|| <= ||.(((1 - t) * (y - x)) + (t * (z - x))).||
by A19, A20, PRVECT_2:def 12;
A22:
||.(((1 - t) * (y - x)) + (t * (z - x))).|| <= (|.(1 - t).| * ||.(y - x).||) + (|.t.| * ||.(z - x).||)
by NORMSP_1:5;
A23:
( |.(1 - t).| = 1 - t & |.t.| = t )
by A5, ABSVALUE:def 1, XREAL_1:48;
(|.(1 - t).| * ||.(y - x).||) + (|.t.| * ||.(z - x).||) < d
then
||.(((1 - t) * (y - x)) + (t * (z - x))).|| < d
by A22, XXREAL_0:2;
hence
||.(w - x).|| < d
by A21, XXREAL_0:2; verum