let p1, p2 be Element of REAL 3; :: thesis: |((- p1),p2)| = - |(p1,p2)|
A1: - p1 = |[(- (p1 . 1)),(- (p1 . 2)),(- (p1 . 3))]| by Th53;
then A2: (- p1) . 1 = - (p1 . 1) by FINSEQ_1:45;
A3: (- p1) . 2 = - (p1 . 2) by A1, FINSEQ_1:45;
A4: (- p1) . 3 = - (p1 . 3) by A1, FINSEQ_1:45;
A5: |(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 A2, A3, A4, Lm5;
hence |((- p1),p2)| = - |(p1,p2)| by A5; :: thesis: verum