let n be Nat; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( p = y & r * p = z implies r * (dist (x,y)) = dist (x,z) )
assume that
A3: p = y and
A4: r * p = z ; :: thesis: 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 ;
:: thesis: verum