let p1, p2, q1, q2 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 & q1 = (VFunc g1,g2,g3) . t1 & q2 = (VFunc g1,g2,g3) . t2 holds
|((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
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 & q1 = (VFunc g1,g2,g3) . t1 & q2 = (VFunc g1,g2,g3) . t2 holds
|((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
let t1, t2 be Real; :: thesis: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q1 = (VFunc g1,g2,g3) . t1 & q2 = (VFunc g1,g2,g3) . t2 implies |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| )
assume A1: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q1 = (VFunc g1,g2,g3) . t1 & q2 = (VFunc g1,g2,g3) . t2 ) ; :: thesis: |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
A2: p1 = |[(f1 . t1),(f2 . t1),(f3 . t1)]| by A1, Def1;
A3: p1 . 1 = f1 . t1 by A2, FINSEQ_1:62;
A4: p1 . 2 = f2 . t1 by A2, FINSEQ_1:62;
A5: p1 . 3 = f3 . t1 by A2, FINSEQ_1:62;
A6: p2 = |[(f1 . t2),(f2 . t2),(f3 . t2)]| by A1, Def1;
A7: p2 . 1 = f1 . t2 by A6, FINSEQ_1:62;
A8: p2 . 2 = f2 . t2 by A6, FINSEQ_1:62;
A9: p2 . 3 = f3 . t2 by A6, FINSEQ_1:62;
A10: q1 = |[(g1 . t1),(g2 . t1),(g3 . t1)]| by A1, Def1;
A11: q1 . 1 = g1 . t1 by A10, FINSEQ_1:62;
A12: q1 . 2 = g2 . t1 by A10, FINSEQ_1:62;
A13: q1 . 3 = g3 . t1 by A10, FINSEQ_1:62;
A14: q2 = |[(g1 . t2),(g2 . t2),(g3 . t2)]| by A1, Def1;
A15: q2 . 1 = g1 . t2 by A14, FINSEQ_1:62;
A16: q2 . 2 = g2 . t2 by A14, FINSEQ_1:62;
A17: q2 . 3 = g3 . t2 by A14, FINSEQ_1:62;
set q = q1 - q2;
A19: q1 - q2 = |[((g1 . t1) - (g1 . t2)),((g2 . t1) - (g2 . t2)),((g3 . t1) - (g3 . t2))]| by A1, Th49;
set p = p1 - p2;
A21: p1 - p2 = |[((f1 . t1) - (f1 . t2)),((f2 . t1) - (f2 . t2)),((f3 . t1) - (f3 . t2))]| by A1, Th49;
|((p1 - p2),(q1 - q2))| = ((((p1 - p2) . 1) * ((q1 - q2) . 1)) + (((p1 - p2) . 2) * ((q1 - q2) . 2))) + (((p1 - p2) . 3) * ((q1 - q2) . 3)) by Lm8
.= ((((f1 . t1) - (f1 . t2)) * ((q1 - q2) . 1)) + (((p1 - p2) . 2) * ((q1 - q2) . 2))) + (((p1 - p2) . 3) * ((q1 - q2) . 3)) by A21, FINSEQ_1:62
.= ((((f1 . t1) - (f1 . t2)) * ((q1 - q2) . 1)) + (((f2 . t1) - (f2 . t2)) * ((q1 - q2) . 2))) + (((p1 - p2) . 3) * ((q1 - q2) . 3)) by A21, FINSEQ_1:62
.= ((((f1 . t1) - (f1 . t2)) * ((q1 - q2) . 1)) + (((f2 . t1) - (f2 . t2)) * ((q1 - q2) . 2))) + (((f3 . t1) - (f3 . t2)) * ((q1 - q2) . 3)) by A21, FINSEQ_1:62
.= ((((f1 . t1) - (f1 . t2)) * ((g1 . t1) - (g1 . t2))) + (((f2 . t1) - (f2 . t2)) * ((q1 - q2) . 2))) + (((f3 . t1) - (f3 . t2)) * ((q1 - q2) . 3)) by A19, FINSEQ_1:62
.= ((((f1 . t1) - (f1 . t2)) * ((g1 . t1) - (g1 . t2))) + (((f2 . t1) - (f2 . t2)) * ((g2 . t1) - (g2 . t2)))) + (((f3 . t1) - (f3 . t2)) * ((q1 - q2) . 3)) by A19, FINSEQ_1:62
.= ((((((f1 . t1) * (g1 . t1)) - ((f1 . t2) * (g1 . t1))) - ((f1 . t1) * (g1 . t2))) + ((f1 . t2) * (g1 . t2))) + (((((f2 . t1) * (g2 . t1)) - ((f2 . t2) * (g2 . t1))) - ((f2 . t1) * (g2 . t2))) + ((f2 . t2) * (g2 . t2)))) + (((f3 . t1) - (f3 . t2)) * ((g3 . t1) - (g3 . t2))) by A19, FINSEQ_1:62
.= ((((((f1 . t1) * (g1 . t1)) + ((f2 . t1) * (g2 . t1))) + ((f3 . t1) * (g3 . t1))) - ((((f1 . t1) * (g1 . t2)) + ((f2 . t1) * (g2 . t2))) + ((f3 . t1) * (g3 . t2)))) - ((((f1 . t2) * (g1 . t1)) + ((f2 . t2) * (g2 . t1))) + ((f3 . t2) * (g3 . t1)))) + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2)))
.= ((|(p1,q1)| - ((((f1 . t1) * (g1 . t2)) + ((f2 . t1) * (g2 . t2))) + ((f3 . t1) * (g3 . t2)))) - ((((f1 . t2) * (g1 . t1)) + ((f2 . t2) * (g2 . t1))) + ((f3 . t2) * (g3 . t1)))) + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2))) by A3, A4, A5, A11, A12, A13, Lm8
.= ((|(p1,q1)| - |(p1,q2)|) - ((((f1 . t2) * (g1 . t1)) + ((f2 . t2) * (g2 . t1))) + ((f3 . t2) * (g3 . t1)))) + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2))) by A3, A4, A5, A15, A16, A17, Lm8
.= ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2))) by A7, A8, A9, A11, A12, A13, Lm8
.= ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| by A7, A8, A9, A15, A16, A17, Lm8 ;
hence |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| ; :: thesis: verum