let f1, f2, f3, g1, g2, g3 be PartFunc of REAL,REAL; :: thesis: for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 holds
VFuncdiff (((f2 (#) g3) - (f3 (#) g2)),((f3 (#) g1) - (f1 (#) g3)),((f1 (#) g2) - (f2 (#) g1)),t0) = |[(((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0)))),(((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))),(((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))]| + |[(((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))),(((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))),(((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))]|
let t0 be Real; :: thesis: ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 implies VFuncdiff (((f2 (#) g3) - (f3 (#) g2)),((f3 (#) g1) - (f1 (#) g3)),((f1 (#) g2) - (f2 (#) g1)),t0) = |[(((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0)))),(((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))),(((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))]| + |[(((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))),(((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))),(((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))]| )
assume that
A1: ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 ) and
A2: ( g1 is_differentiable_in t0 & g2 is_differentiable_in t0 & g3 is_differentiable_in t0 ) ; :: thesis: VFuncdiff (((f2 (#) g3) - (f3 (#) g2)),((f3 (#) g1) - (f1 (#) g3)),((f1 (#) g2) - (f2 (#) g1)),t0) = |[(((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0)))),(((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))),(((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))]| + |[(((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))),(((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))),(((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))]|
( f2 (#) g3 is_differentiable_in t0 & f3 (#) g2 is_differentiable_in t0 & f3 (#) g1 is_differentiable_in t0 & f1 (#) g3 is_differentiable_in t0 & f1 (#) g2 is_differentiable_in t0 & f2 (#) g1 is_differentiable_in t0 ) by A1, A2, FDIFF_1:16;
then VFuncdiff (((f2 (#) g3) - (f3 (#) g2)),((f3 (#) g1) - (f1 (#) g3)),((f1 (#) g2) - (f2 (#) g1)),t0) = (VFuncdiff ((f2 (#) g3),(f3 (#) g1),(f1 (#) g2),t0)) - (VFuncdiff ((f3 (#) g2),(f1 (#) g3),(f2 (#) g1),t0)) by Th89
.= (|[((g3 . t0) * (diff (f2,t0))),((g1 . t0) * (diff (f3,t0))),((g2 . t0) * (diff (f1,t0)))]| + |[((f2 . t0) * (diff (g3,t0))),((f3 . t0) * (diff (g1,t0))),((f1 . t0) * (diff (g2,t0)))]|) - (VFuncdiff ((f3 (#) g2),(f1 (#) g3),(f2 (#) g1),t0)) by A1, A2, Th91
.= (|[((g3 . t0) * (diff (f2,t0))),((g1 . t0) * (diff (f3,t0))),((g2 . t0) * (diff (f1,t0)))]| + |[((f2 . t0) * (diff (g3,t0))),((f3 . t0) * (diff (g1,t0))),((f1 . t0) * (diff (g2,t0)))]|) - (|[((g2 . t0) * (diff (f3,t0))),((g3 . t0) * (diff (f1,t0))),((g1 . t0) * (diff (f2,t0)))]| + |[((f3 . t0) * (diff (g2,t0))),((f1 . t0) * (diff (g3,t0))),((f2 . t0) * (diff (g1,t0)))]|) by A1, A2, Th91
.= (|[((g3 . t0) * (diff (f2,t0))),((g1 . t0) * (diff (f3,t0))),((g2 . t0) * (diff (f1,t0)))]| - |[((g2 . t0) * (diff (f3,t0))),((g3 . t0) * (diff (f1,t0))),((g1 . t0) * (diff (f2,t0)))]|) + (|[((f2 . t0) * (diff (g3,t0))),((f3 . t0) * (diff (g1,t0))),((f1 . t0) * (diff (g2,t0)))]| - |[((f3 . t0) * (diff (g2,t0))),((f1 . t0) * (diff (g3,t0))),((f2 . t0) * (diff (g1,t0)))]|) by Lm10
.= |[(((g3 . t0) * (diff (f2,t0))) - ((g2 . t0) * (diff (f3,t0)))),(((g1 . t0) * (diff (f3,t0))) - ((g3 . t0) * (diff (f1,t0)))),(((g2 . t0) * (diff (f1,t0))) - ((g1 . t0) * (diff (f2,t0))))]| + (|[((f2 . t0) * (diff (g3,t0))),((f3 . t0) * (diff (g1,t0))),((f1 . t0) * (diff (g2,t0)))]| - |[((f3 . t0) * (diff (g2,t0))),((f1 . t0) * (diff (g3,t0))),((f2 . t0) * (diff (g1,t0)))]|) by Lm11
.= |[(((g3 . t0) * (diff (f2,t0))) - ((g2 . t0) * (diff (f3,t0)))),(((g1 . t0) * (diff (f3,t0))) - ((g3 . t0) * (diff (f1,t0)))),(((g2 . t0) * (diff (f1,t0))) - ((g1 . t0) * (diff (f2,t0))))]| + |[(((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0)))),(((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))),(((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))]| by Lm11 ;
hence VFuncdiff (((f2 (#) g3) - (f3 (#) g2)),((f3 (#) g1) - (f1 (#) g3)),((f1 (#) g2) - (f2 (#) g1)),t0) = |[(((f2 . t0) * (diff (g3,t0))) - ((f3 . t0) * (diff (g2,t0)))),(((f3 . t0) * (diff (g1,t0))) - ((f1 . t0) * (diff (g3,t0)))),(((f1 . t0) * (diff (g2,t0))) - ((f2 . t0) * (diff (g1,t0))))]| + |[(((diff (f2,t0)) * (g3 . t0)) - ((diff (f3,t0)) * (g2 . t0))),(((diff (f3,t0)) * (g1 . t0)) - ((diff (f1,t0)) * (g3 . t0))),(((diff (f1,t0)) * (g2 . t0)) - ((diff (f2,t0)) * (g1 . t0)))]| ; :: thesis: verum