let n be Nat; for r being Real st r > 0 holds
for x, y, z being Element of (Euclid n) st x = 0* n holds
for p being Element of (TOP-REAL n) st p = y & r * p = z holds
r * (dist (x,y)) = dist (x,z)
let r be Real; ( r > 0 implies for x, y, z being Element of (Euclid n) st x = 0* n holds
for p being Element of (TOP-REAL n) st p = y & r * p = z holds
r * (dist (x,y)) = dist (x,z) )
assume A1:
r > 0
; for x, y, z being Element of (Euclid n) st x = 0* n holds
for p being Element of (TOP-REAL n) st p = y & r * p = z holds
r * (dist (x,y)) = dist (x,z)
let x, y, z be Element of (Euclid n); ( x = 0* n implies for p being Element of (TOP-REAL n) st p = y & r * p = z holds
r * (dist (x,y)) = dist (x,z) )
assume A2:
x = 0* n
; for p being Element of (TOP-REAL n) st p = y & r * p = z holds
r * (dist (x,y)) = dist (x,z)
let p be Element of (TOP-REAL n); ( p = y & r * p = z implies r * (dist (x,y)) = dist (x,z) )
assume that
A3:
p = y
and
A4:
r * p = z
; r * (dist (x,y)) = dist (x,z)
reconsider x1 = x, y1 = y as Element of REAL n ;
A5: dist (x,z) =
(Pitag_dist n) . (x,z)
.=
|.(x1 - (r * y1)).|
by A3, A4, EUCLID:def 6
;
A6: r * x1 =
n |-> (0 * r)
by A2, RVSUM_1:48
.=
x1
by A2
;
dist (x,y) =
(Pitag_dist n) . (x,y)
.=
|.(x1 - y1).|
by EUCLID:def 6
;
hence r * (dist (x,y)) =
|.r.| * |.(x1 - y1).|
by A1, ABSVALUE:def 1
.=
|.(r * (x1 - y1)).|
by EUCLID:11
.=
|.((r * x1) + (r * (- y1))).|
by RVSUM_1:51
.=
|.((r * x1) + (((- 1) * r) * y1)).|
by RVSUM_1:49
.=
dist (x,z)
by A5, A6, RVSUM_1:49
;
verum