let p1, p2 be Element of REAL 3; |((- p1),(- p2))| = |(p1,p2)|
A3:
- p1 = |[(- (p1 . 1)),(- (p1 . 2)),(- (p1 . 3))]|
by Th39;
A4:
- p2 = |[(- (p2 . 1)),(- (p2 . 2)),(- (p2 . 3))]|
by Th39;
A5:
(- p1) . 1 = - (p1 . 1)
by A3, FINSEQ_1:62;
A6:
(- p1) . 2 = - (p1 . 2)
by A3, FINSEQ_1:62;
A7:
(- p1) . 3 = - (p1 . 3)
by A3, FINSEQ_1:62;
A8:
(- p2) . 1 = - (p2 . 1)
by A4, FINSEQ_1:62;
A9:
(- p2) . 2 = - (p2 . 2)
by A4, FINSEQ_1:62;
A10:
(- p2) . 3 = - (p2 . 3)
by A4, FINSEQ_1:62;
A11:
|(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))
by Lm8;
|((- p1),(- p2))| = (((- (p1 . 1)) * (- (p2 . 1))) + ((- (p1 . 2)) * (- (p2 . 2)))) + ((- (p1 . 3)) * (- (p2 . 3)))
by A5, A6, A7, A8, A9, A10, Lm8;
hence
|((- p1),(- p2))| = |(p1,p2)|
by A11; verum