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:24;
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 Th58
.= (|[((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, Th60
.= (|[((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, Th60
.= (|[((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 LmA62
.= |[(((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 LmA63
.= |[(((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 LmA63 ;
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