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) <X> q = (p1 <X> q) + (p2 <X> 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) <X> q = (p1 <X> q) + (p2 <X> 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) <X> q = (p1 <X> q) + (p2 <X> q) )
assume A1: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t ) ; :: thesis: (p1 + p2) <X> q = (p1 <X> q) + (p2 <X> q)
A2: p1 + p2 = |[((f1 . t1) + (f1 . t2)),((f2 . t1) + (f2 . t2)),((f3 . t1) + (f3 . t2))]| by A1, Th44;
A3: (p1 + p2) . 1 = (f1 . t1) + (f1 . t2) by A2, FINSEQ_1:62;
A4: (p1 + p2) . 2 = (f2 . t1) + (f2 . t2) by A2, FINSEQ_1:62;
A5: (p1 + p2) . 3 = (f3 . t1) + (f3 . t2) by A2, FINSEQ_1:62;
B2: q = |[(g1 . t),(g2 . t),(g3 . t)]| by A1, Def1;
B3: q . 1 = g1 . t by B2, FINSEQ_1:62;
B4: q . 2 = g2 . t by B2, FINSEQ_1:62;
B5: q . 3 = g3 . t by B2, FINSEQ_1:62;
(p1 <X> q) + (p2 <X> q) = |[(((f2 . t1) * (g3 . t)) - ((f3 . t1) * (g2 . t))),(((f3 . t1) * (g1 . t)) - ((f1 . t1) * (g3 . t))),(((f1 . t1) * (g2 . t)) - ((f2 . t1) * (g1 . t)))]| + (p2 <X> q) by A1, Th55
.= |[(((f2 . t1) * (g3 . t)) - ((f3 . t1) * (g2 . t))),(((f3 . t1) * (g1 . t)) - ((f1 . t1) * (g3 . t))),(((f1 . t1) * (g2 . t)) - ((f2 . t1) * (g1 . t)))]| + |[(((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
.= |[((((f2 . t1) * (g3 . t)) - ((f3 . t1) * (g2 . t))) + (((f2 . t2) * (g3 . t)) - ((f3 . t2) * (g2 . t)))),((((f3 . t1) * (g1 . t)) - ((f1 . t1) * (g3 . t))) + (((f3 . t2) * (g1 . t)) - ((f1 . t2) * (g3 . t)))),((((f1 . t1) * (g2 . t)) - ((f2 . t1) * (g1 . t))) + (((f1 . t2) * (g2 . t)) - ((f2 . t2) * (g1 . t))))]| by LmA31
.= |[((((p1 + p2) . 2) * (q . 3)) - (((p1 + p2) . 3) * (q . 2))),((((p1 + p2) . 3) * (q . 1)) - (((p1 + p2) . 1) * (q . 3))),((((p1 + p2) . 1) * (q . 2)) - (((p1 + p2) . 2) * (q . 1)))]| by A3, A4, A5, B5, B4, B3 ;
hence (p1 + p2) <X> q = (p1 <X> q) + (p2 <X> q) ; :: thesis: verum