let p1, p2, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t1, t2, t being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t holds
|{p1,p2,q}| = |((p1 <X> p2),q)|
let f1, f2, f3, g1, g2, g3 be PartFunc of ,; :: thesis: for t1, t2, t being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t holds
|{p1,p2,q}| = |((p1 <X> p2),q)|
let t1, t2, t be Real; :: thesis: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t implies |{p1,p2,q}| = |((p1 <X> p2),q)| )
assume A1: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t ) ; :: thesis: |{p1,p2,q}| = |((p1 <X> p2),q)|
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 <X> q = |[(((f2 . t2) * (g3 . t)) - ((f3 . t2) * (g2 . t))),(((f3 . t2) * (g1 . t)) - ((f1 . t2) * (g3 . t))),(((f1 . t2) * (g2 . t)) - ((f2 . t2) * (g1 . t)))]| by A1, Th55;
A7: (p2 <X> q) . 1 = ((f2 . t2) * (g3 . t)) - ((f3 . t2) * (g2 . t)) by A6, FINSEQ_1:62;
A8: (p2 <X> q) . 2 = ((f3 . t2) * (g1 . t)) - ((f1 . t2) * (g3 . t)) by A6, FINSEQ_1:62;
A9: (p2 <X> q) . 3 = ((f1 . t2) * (g2 . t)) - ((f2 . t2) * (g1 . t)) by A6, FINSEQ_1:62;
A10: p1 <X> p2 = |[(((f2 . t1) * (f3 . t2)) - ((f3 . t1) * (f2 . t2))),(((f3 . t1) * (f1 . t2)) - ((f1 . t1) * (f3 . t2))),(((f1 . t1) * (f2 . t2)) - ((f2 . t1) * (f1 . t2)))]| by A1, Th55;
A12: q = |[(g1 . t),(g2 . t),(g3 . t)]| by A1, Def1;
|{p1,p2,q}| = (((f1 . t1) * (((f2 . t2) * (g3 . t)) - ((f3 . t2) * (g2 . t)))) + ((f2 . t1) * (((f3 . t2) * (g1 . t)) - ((f1 . t2) * (g3 . t))))) + ((f3 . t1) * (((f1 . t2) * (g2 . t)) - ((f2 . t2) * (g1 . t)))) by A9, A8, A7, A5, A4, A3, Lm8
.= (((((f2 . t1) * (f3 . t2)) - ((f3 . t1) * (f2 . t2))) * (g1 . t)) + ((((f3 . t1) * (f1 . t2)) - ((f1 . t1) * (f3 . t2))) * (g2 . t))) + ((((f1 . t1) * (f2 . t2)) - ((f2 . t1) * (f1 . t2))) * (g3 . t))
.= |((p1 <X> p2),q)| by A12, A10, LmA52 ;
hence |{p1,p2,q}| = |((p1 <X> p2),q)| ; :: thesis: verum