let r be Element of REAL ; :: thesis: for p, q being Element of REAL 3
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
( (r * p) <X> q = r * (p <X> q) & (r * p) <X> q = p <X> (r * q) )
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
( (r * p) <X> q = r * (p <X> q) & (r * p) <X> q = p <X> (r * 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
( (r * p) <X> q = r * (p <X> q) & (r * p) <X> q = p <X> (r * q) )
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t & q = (VFunc g1,g2,g3) . t implies ( (r * p) <X> q = r * (p <X> q) & (r * p) <X> q = p <X> (r * q) ) )
assume A1: ( p = (VFunc f1,f2,f3) . t & q = (VFunc g1,g2,g3) . t ) ; :: thesis: ( (r * p) <X> q = r * (p <X> q) & (r * p) <X> q = p <X> (r * q) )
A2: (r * p) <X> q = |[(r * (f1 . t)),(r * (f2 . t)),(r * (f3 . t))]| <X> q by A1, Th38
.= |[(r * (f1 . t)),(r * (f2 . t)),(r * (f3 . t))]| <X> |[(g1 . t),(g2 . t),(g3 . t)]| by A1, Def1
.= |[(((r * (f2 . t)) * (g3 . t)) - ((r * (f3 . t)) * (g2 . t))),(((r * (f3 . t)) * (g1 . t)) - ((r * (f1 . t)) * (g3 . t))),(((r * (f1 . t)) * (g2 . t)) - ((r * (f2 . t)) * (g1 . t)))]| by Lm11 ;
A3: (r * p) <X> q = |[(r * (((f2 . t) * (g3 . t)) - ((f3 . t) * (g2 . t)))),(r * (((f3 . t) * (g1 . t)) - ((f1 . t) * (g3 . t)))),(r * (((f1 . t) * (g2 . t)) - ((f2 . t) * (g1 . t))))]| by A2
.= r * |[(((f2 . t) * (g3 . t)) - ((f3 . t) * (g2 . t))),(((f3 . t) * (g1 . t)) - ((f1 . t) * (g3 . t))),(((f1 . t) * (g2 . t)) - ((f2 . t) * (g1 . t)))]| by LmA8
.= r * (p <X> q) by A1, Th55 ;
(r * p) <X> q = |[(((f2 . t) * (r * (g3 . t))) - ((f3 . t) * (r * (g2 . t)))),(((f3 . t) * (r * (g1 . t))) - ((f1 . t) * (r * (g3 . t)))),(((f1 . t) * (r * (g2 . t))) - ((f2 . t) * (r * (g1 . t))))]| by A2
.= |[(f1 . t),(f2 . t),(f3 . t)]| <X> |[(r * (g1 . t)),(r * (g2 . t)),(r * (g3 . t))]| by Lm11
.= p <X> |[(r * (g1 . t)),(r * (g2 . t)),(r * (g3 . t))]| by A1, Def1
.= p <X> (r * q) by A1, Th38 ;
hence ( (r * p) <X> q = r * (p <X> q) & (r * p) <X> q = p <X> (r * q) ) by A3; :: thesis: verum