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