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