let p, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t being Real st p = (VFunc f1,f2,f3) . t & q = (VFunc g1,g2,g3) . t holds
|((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
let f1, f2, f3, g1, g2, g3 be PartFunc of ,; :: thesis: for t being Real st p = (VFunc f1,f2,f3) . t & q = (VFunc g1,g2,g3) . t holds
|((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t & q = (VFunc g1,g2,g3) . t implies |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| )
assume A1: ( p = (VFunc f1,f2,f3) . t & q = (VFunc g1,g2,g3) . t ) ; :: thesis: |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
A2: p = |[(f1 . t),(f2 . t),(f3 . t)]| by A1, Def1;
A3: p . 1 = f1 . t by A2, FINSEQ_1:62;
A4: p . 2 = f2 . t by A2, FINSEQ_1:62;
A5: p . 3 = f3 . t by A2, FINSEQ_1:62;
A6: q = |[(g1 . t),(g2 . t),(g3 . t)]| by A1, Def1;
A7: q . 1 = g1 . t by A6, FINSEQ_1:62;
A8: q . 2 = g2 . t by A6, FINSEQ_1:62;
A9: q . 3 = g3 . t by A6, FINSEQ_1:62;
set p1 = p - q;
A11: p - q = |[((f1 . t) - (g1 . t)),((f2 . t) - (g2 . t)),((f3 . t) - (g3 . t))]| by A1, Th49;
|((p - q),(p - q))| = ((((p - q) . 1) * ((p - q) . 1)) + (((p - q) . 2) * ((p - q) . 2))) + (((p - q) . 3) * ((p - q) . 3)) by Lm8
.= ((((f1 . t) - (g1 . t)) * ((p - q) . 1)) + (((p - q) . 2) * ((p - q) . 2))) + (((p - q) . 3) * ((p - q) . 3)) by A11, FINSEQ_1:62
.= ((((f1 . t) - (g1 . t)) * ((p - q) . 1)) + (((f2 . t) - (g2 . t)) * ((p - q) . 2))) + (((p - q) . 3) * ((p - q) . 3)) by A11, FINSEQ_1:62
.= ((((f1 . t) - (g1 . t)) * ((p - q) . 1)) + (((f2 . t) - (g2 . t)) * ((p - q) . 2))) + (((f3 . t) - (g3 . t)) * ((p - q) . 3)) by A11, FINSEQ_1:62
.= ((((f1 . t) - (g1 . t)) * ((f1 . t) - (g1 . t))) + (((f2 . t) - (g2 . t)) * ((p - q) . 2))) + (((f3 . t) - (g3 . t)) * ((p - q) . 3)) by A11, FINSEQ_1:62
.= ((((f1 . t) - (g1 . t)) * ((f1 . t) - (g1 . t))) + (((f2 . t) - (g2 . t)) * ((f2 . t) - (g2 . t)))) + (((f3 . t) - (g3 . t)) * ((p - q) . 3)) by A11, FINSEQ_1:62
.= ((((((f1 . t) * (f1 . t)) - ((f1 . t) * (g1 . t))) - ((g1 . t) * (f1 . t))) + ((g1 . t) * (g1 . t))) + (((((f2 . t) * (f2 . t)) - ((f2 . t) * (g2 . t))) - ((g2 . t) * (f2 . t))) + ((g2 . t) * (g2 . t)))) + (((f3 . t) - (g3 . t)) * ((f3 . t) - (g3 . t))) by A11, FINSEQ_1:62
.= ((((((f1 . t) * (f1 . t)) + ((f2 . t) * (f2 . t))) + ((f3 . t) * (f3 . t))) - ((((f1 . t) * (g1 . t)) + ((f2 . t) * (g2 . t))) + ((f3 . t) * (g3 . t)))) - ((((g1 . t) * (f1 . t)) + ((g2 . t) * (f2 . t))) + ((g3 . t) * (f3 . t)))) + ((((g1 . t) * (g1 . t)) + ((g2 . t) * (g2 . t))) + ((g3 . t) * (g3 . t)))
.= ((|(p,p)| - ((((f1 . t) * (g1 . t)) + ((f2 . t) * (g2 . t))) + ((f3 . t) * (g3 . t)))) - ((((g1 . t) * (f1 . t)) + ((g2 . t) * (f2 . t))) + ((g3 . t) * (f3 . t)))) + ((((g1 . t) * (g1 . t)) + ((g2 . t) * (g2 . t))) + ((g3 . t) * (g3 . t))) by A3, A4, A5, Lm8
.= ((|(p,p)| - |(p,q)|) - ((((g1 . t) * (f1 . t)) + ((g2 . t) * (f2 . t))) + ((g3 . t) * (f3 . t)))) + ((((g1 . t) * (g1 . t)) + ((g2 . t) * (g2 . t))) + ((g3 . t) * (g3 . t))) by A3, A4, A5, A7, A8, A9, Lm8
.= ((|(p,p)| - |(p,q)|) - |(q,p)|) + ((((g1 . t) * (g1 . t)) + ((g2 . t) * (g2 . t))) + ((g3 . t) * (g3 . t))) by A3, A4, A5, A7, A8, A9, Lm8
.= ((|(p,p)| - |(p,q)|) - |(q,p)|) + |(q,q)| by A7, A8, A9, Lm8 ;
hence |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ; :: thesis: verum