let n be Nat; :: thesis: Pitag_dist n is_metric_of REAL n
let x, y, z be Element of REAL n; :: according to PCOMPS_1:def 6 :: thesis: ( ( not (Pitag_dist n) . (x,y) = 0 or x = y ) & ( not x = y or (Pitag_dist n) . (x,y) = 0 ) & (Pitag_dist n) . (x,y) = (Pitag_dist n) . (y,x) & (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z)) )
A1: (Pitag_dist n) . (y,z) = |.(y - z).| by Def6;
(Pitag_dist n) . (x,y) = |.(x - y).| by Def6;
hence ( (Pitag_dist n) . (x,y) = 0 iff x = y ) by Th13; :: thesis: ( (Pitag_dist n) . (x,y) = (Pitag_dist n) . (y,x) & (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z)) )
thus (Pitag_dist n) . (x,y) = |.(x - y).| by Def6
.= |.(y - x).| by Th15
.= (Pitag_dist n) . (y,x) by Def6 ; :: thesis: (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z))
( (Pitag_dist n) . (x,y) = |.(x - y).| & (Pitag_dist n) . (x,z) = |.(x - z).| ) by Def6;
hence (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z)) by A1, Th16; :: thesis: verum