let p1, p2, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t1, t2 being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 holds
|((p1 - p2),q)| = |(p1,q)| - |(p2,q)|
let f1, f2, f3, g1, g2, g3 be PartFunc of ,; :: thesis: for t1, t2 being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 holds
|((p1 - p2),q)| = |(p1,q)| - |(p2,q)|
let t1, t2 be Real; :: thesis: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 implies |((p1 - p2),q)| = |(p1,q)| - |(p2,q)| )
assume B0: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 ) ; :: thesis: |((p1 - p2),q)| = |(p1,q)| - |(p2,q)|
A0: p1 = |[(f1 . t1),(f2 . t1),(f3 . t1)]| by B0, Def1;
B1: p1 . 1 = f1 . t1 by A0, FINSEQ_1:62;
B2: p1 . 2 = f2 . t1 by A0, FINSEQ_1:62;
B3: p1 . 3 = f3 . t1 by A0, FINSEQ_1:62;
A2: p2 = |[(f1 . t2),(f2 . t2),(f3 . t2)]| by B0, Def1;
A3: p2 . 1 = f1 . t2 by A2, FINSEQ_1:62;
A4: p2 . 2 = f2 . t2 by A2, FINSEQ_1:62;
A5: p2 . 3 = f3 . t2 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;
A8: p1 - p2 = |[((p1 . 1) - (p2 . 1)),((p1 . 2) - (p2 . 2)),((p1 . 3) - (p2 . 3))]| by Lm7;
set p = p1 - p2;
A10: (p1 - p2) . 2 = (p1 . 2) - (p2 . 2) by A8, FINSEQ_1:62;
A11: (p1 - p2) . 3 = (p1 . 3) - (p2 . 3) by A8, FINSEQ_1:62;
A12: |((p1 - p2),q)| = ((((p1 - p2) . 1) * (q . 1)) + (((p1 - p2) . 2) * (q . 2))) + (((p1 - p2) . 3) * (q . 3)) by Lm8;
|((p1 - p2),q)| = ((((f1 . t1) - (f1 . t2)) * (g1 . t2)) + (((f2 . t1) - (f2 . t2)) * (g2 . t2))) + (((f3 . t1) - (f3 . t2)) * (g3 . t2)) by C1, C2, C3, A3, A4, A5, B1, B2, B3, A8, A10, A11, A12, FINSEQ_1:62
.= ((((f1 . t1) * (g1 . t2)) + ((f2 . t1) * (g2 . t2))) + ((f3 . t1) * (g3 . t2))) - ((((f2 . t2) * (g2 . t2)) + ((f1 . t2) * (g1 . t2))) + ((f3 . t2) * (g3 . t2)))
.= |(p1,q)| - ((((f2 . t2) * (g2 . t2)) + ((f1 . t2) * (g1 . t2))) + ((f3 . t2) * (g3 . t2))) by B1, B2, B3, C1, C2, C3, Lm8
.= |(p1,q)| - |(p2,q)| by A3, A4, A5, C1, C2, C3, Lm8 ;
hence |((p1 - p2),q)| = |(p1,q)| - |(p2,q)| ; :: thesis: verum