let p, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t1, t2 being Real st p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 holds
|((- p),(- q))| = |(p,q)|
let f1, f2, f3, g1, g2, g3 be PartFunc of ,; :: thesis: for t1, t2 being Real st p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 holds
|((- p),(- q))| = |(p,q)|
let t1, t2 be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 implies |((- p),(- q))| = |(p,q)| )
assume B0: ( p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 ) ; :: thesis: |((- p),(- q))| = |(p,q)|
A0: p = |[(f1 . t1),(f2 . t1),(f3 . t1)]| by B0, Def1;
B1: p . 1 = f1 . t1 by A0, FINSEQ_1:62;
B2: p . 2 = f2 . t1 by A0, FINSEQ_1:62;
B3: p . 3 = f3 . t1 by A0, FINSEQ_1:62;
A2: - p = |[(- (f1 . t1)),(- (f2 . t1)),(- (f3 . t1))]| by B0, Th39;
A3: (- p) . 1 = - (f1 . t1) by A2, FINSEQ_1:62;
A4: (- p) . 2 = - (f2 . t1) by A2, FINSEQ_1:62;
A5: (- p) . 3 = - (f3 . t1) by A2, FINSEQ_1:62;
C0: q = |[(g1 . t2),(g2 . t2),(g3 . t2)]| by B0, Def1;
C1: q . 1 = g1 . t2 by C0, FINSEQ_1:62;
C2: q . 2 = g2 . t2 by C0, FINSEQ_1:62;
C3: q . 3 = g3 . t2 by C0, FINSEQ_1:62;
C4: - q = |[(- (g1 . t2)),(- (g2 . t2)),(- (g3 . t2))]| by B0, Th39;
C5: (- q) . 1 = - (g1 . t2) by C4, FINSEQ_1:62;
C6: (- q) . 2 = - (g2 . t2) by C4, FINSEQ_1:62;
C7: (- q) . 3 = - (g3 . t2) by C4, FINSEQ_1:62;
|((- p),(- q))| = (((- (f1 . t1)) * (- (g1 . t2))) + ((- (f2 . t1)) * (- (g2 . t2)))) + ((- (f3 . t1)) * (- (g3 . t2))) by A3, A4, A5, C5, C6, C7, Lm8
.= (((f1 . t1) * (g1 . t2)) + ((f2 . t1) * (g2 . t2))) + ((f3 . t1) * (g3 . t2))
.= |(p,q)| by B1, B2, B3, C1, C2, C3, Lm8 ;
hence |((- p),(- q))| = |(p,q)| ; :: thesis: verum