let p1, p2 be Point of (TOP-REAL 2); :: thesis: for u1, u2 being Point of (Euclid 2) st u1 = p1 & u2 = p2 holds
(Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2))
let u1, u2 be Point of (Euclid 2); :: thesis: ( u1 = p1 & u2 = p2 implies (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) )
assume that
A1: u1 = p1 and
A2: u2 = p2 ; :: thesis: (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2))
reconsider v1 = u1, v2 = u2 as Element of REAL 2 ;
( p1 = |[(p1 `1),(p1 `2)]| & u2 = <*(p2 `1),(p2 `2)*> ) by A2, EUCLID:57;
then v1 - v2 = <*(diffreal . ((p1 `1),(p2 `1))),(diffreal . ((p1 `2),(p2 `2)))*> by A1, FINSEQ_2:89
.= <*((p1 `1) - (p2 `1)),(diffreal . ((p1 `2),(p2 `2)))*> by BINOP_2:def 10
.= <*((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))*> by BINOP_2:def 10 ;
then abs (v1 - v2) = <*(absreal . ((p1 `1) - (p2 `1))),(absreal . ((p1 `2) - (p2 `2)))*> by FINSEQ_2:40
.= <*(abs ((p1 `1) - (p2 `1))),(absreal . ((p1 `2) - (p2 `2)))*> by EUCLID:def 2
.= <*(abs ((p1 `1) - (p2 `1))),(abs ((p1 `2) - (p2 `2)))*> by EUCLID:def 2 ;
then A3: sqr (abs (v1 - v2)) = <*(sqrreal . (abs ((p1 `1) - (p2 `1)))),(sqrreal . (abs ((p1 `2) - (p2 `2))))*> by FINSEQ_2:40
.= <*((abs ((p1 `1) - (p2 `1))) ^2),(sqrreal . (abs ((p1 `2) - (p2 `2))))*> by RVSUM_1:def 2
.= <*((abs ((p1 `1) - (p2 `1))) ^2),((abs ((p1 `2) - (p2 `2))) ^2)*> by RVSUM_1:def 2
.= <*(((p1 `1) - (p2 `1)) ^2),((abs ((p1 `2) - (p2 `2))) ^2)*> by COMPLEX1:161
.= <*(((p1 `1) - (p2 `1)) ^2),(((p1 `2) - (p2 `2)) ^2)*> by COMPLEX1:161 ;
(Pitag_dist 2) . (u1,u2) = |.(v1 - v2).| by EUCLID:def 6
.= sqrt (Sum (sqr (abs (v1 - v2)))) by EUCLID:29 ;
hence (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) by A3, RVSUM_1:107; :: thesis: verum