let p1, p2 be Element of REAL 3; |((- p1),(- p2))| = |(p1,p2)|
A1:
- p1 = |[(- (p1 . 1)),(- (p1 . 2)),(- (p1 . 3))]|
by Th53;
A2:
- p2 = |[(- (p2 . 1)),(- (p2 . 2)),(- (p2 . 3))]|
by Th53;
A3:
(- p1) . 1 = - (p1 . 1)
by A1, FINSEQ_1:45;
A4:
(- p1) . 2 = - (p1 . 2)
by A1, FINSEQ_1:45;
A5:
(- p1) . 3 = - (p1 . 3)
by A1, FINSEQ_1:45;
A6:
(- p2) . 1 = - (p2 . 1)
by A2, FINSEQ_1:45;
A7:
(- p2) . 2 = - (p2 . 2)
by A2, FINSEQ_1:45;
A8:
(- p2) . 3 = - (p2 . 3)
by A2, FINSEQ_1:45;
A9:
|(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))
by Lm5;
|((- p1),(- p2))| = (((- (p1 . 1)) * (- (p2 . 1))) + ((- (p1 . 2)) * (- (p2 . 2)))) + ((- (p1 . 3)) * (- (p2 . 3)))
by A3, A4, A5, A6, A7, A8, Lm5;
hence
|((- p1),(- p2))| = |(p1,p2)|
by A9; verum