let r be Element of REAL ; for f1, f2, f3 being PartFunc of REAL,REAL
for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 & r <> 0 holds
VFuncdiff (((r (#) f1) ^),((r (#) f2) ^),((r (#) f3) ^),t0) = - ((1 / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)
let f1, f2, f3 be PartFunc of REAL,REAL; for t0 being Real st f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 & r <> 0 holds
VFuncdiff (((r (#) f1) ^),((r (#) f2) ^),((r (#) f3) ^),t0) = - ((1 / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)
let t0 be Real; ( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 & f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 & r <> 0 implies VFuncdiff (((r (#) f1) ^),((r (#) f2) ^),((r (#) f3) ^),t0) = - ((1 / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|) )
assume that
A1:
( f1 is_differentiable_in t0 & f2 is_differentiable_in t0 & f3 is_differentiable_in t0 )
and
A2:
( f1 . t0 <> 0 & f2 . t0 <> 0 & f3 . t0 <> 0 )
and
B0:
r <> 0
; VFuncdiff (((r (#) f1) ^),((r (#) f2) ^),((r (#) f3) ^),t0) = - ((1 / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)
A3:
( r (#) f1 is_differentiable_in t0 & r (#) f2 is_differentiable_in t0 & r (#) f3 is_differentiable_in t0 )
by A1, FDIFF_1:23;
B1:
(r (#) f1) . t0 = r * (f1 . t0)
by VALUED_1:6;
B2:
(r (#) f2) . t0 = r * (f2 . t0)
by VALUED_1:6;
B3:
(r (#) f3) . t0 = r * (f3 . t0)
by VALUED_1:6;
then VFuncdiff (((r (#) f1) ^),((r (#) f2) ^),((r (#) f3) ^),t0) =
- |[((diff ((r (#) f1),t0)) / (((r (#) f1) . t0) ^2)),((diff ((r (#) f2),t0)) / (((r (#) f2) . t0) ^2)),((diff ((r (#) f3),t0)) / (((r (#) f3) . t0) ^2))]|
by A3, B1, B2, A2, B0, Th63
.=
- |[((r * (diff (f1,t0))) / (((r (#) f1) . t0) ^2)),((diff ((r (#) f2),t0)) / (((r (#) f2) . t0) ^2)),((diff ((r (#) f3),t0)) / (((r (#) f3) . t0) ^2))]|
by A1, FDIFF_1:23
.=
- |[((r * (diff (f1,t0))) / (((r (#) f1) . t0) ^2)),((r * (diff (f2,t0))) / (((r (#) f2) . t0) ^2)),((diff ((r (#) f3),t0)) / (((r (#) f3) . t0) ^2))]|
by A1, FDIFF_1:23
.=
- |[((r * (diff (f1,t0))) / (((r (#) f1) . t0) ^2)),((r * (diff (f2,t0))) / (((r (#) f2) . t0) ^2)),((r * (diff (f3,t0))) / (((r (#) f3) . t0) ^2))]|
by A1, FDIFF_1:23
.=
- |[(r * ((diff (f1,t0)) / (((r (#) f1) . t0) ^2))),((r * (diff (f2,t0))) / (((r (#) f2) . t0) ^2)),((r * (diff (f3,t0))) / (((r (#) f3) . t0) ^2))]|
by XCMPLX_1:75
.=
- |[(r * ((diff (f1,t0)) / (((r (#) f1) . t0) ^2))),(r * ((diff (f2,t0)) / (((r (#) f2) . t0) ^2))),((r * (diff (f3,t0))) / (((r (#) f3) . t0) ^2))]|
by XCMPLX_1:75
.=
- |[(r * ((diff (f1,t0)) / (((r (#) f1) . t0) ^2))),(r * ((diff (f2,t0)) / (((r (#) f2) . t0) ^2))),(r * ((diff (f3,t0)) / (((r (#) f3) . t0) ^2)))]|
by XCMPLX_1:75
.=
- (r * |[((diff (f1,t0)) / ((r ^2) * ((f1 . t0) ^2))),((diff (f2,t0)) / ((r ^2) * ((f2 . t0) ^2))),((diff (f3,t0)) / ((r ^2) * ((f3 . t0) ^2)))]|)
by B3, B2, B1, LmA8
.=
- (r * |[(((diff (f1,t0)) / (r ^2)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((r ^2) * ((f2 . t0) ^2))),((diff (f3,t0)) / ((r ^2) * ((f3 . t0) ^2)))]|)
by XCMPLX_1:79
.=
- (r * |[(((diff (f1,t0)) / (r ^2)) / ((f1 . t0) ^2)),(((diff (f2,t0)) / (r ^2)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((r ^2) * ((f3 . t0) ^2)))]|)
by XCMPLX_1:79
.=
- (r * |[(((diff (f1,t0)) / (r ^2)) / ((f1 . t0) ^2)),(((diff (f2,t0)) / (r ^2)) / ((f2 . t0) ^2)),(((diff (f3,t0)) / (r ^2)) / ((f3 . t0) ^2))]|)
by XCMPLX_1:79
.=
- (r * |[(((diff (f1,t0)) / ((f1 . t0) ^2)) / (r ^2)),(((diff (f2,t0)) / (r ^2)) / ((f2 . t0) ^2)),(((diff (f3,t0)) / (r ^2)) / ((f3 . t0) ^2))]|)
by XCMPLX_1:48
.=
- (r * |[(((diff (f1,t0)) / ((f1 . t0) ^2)) / (r ^2)),(((diff (f2,t0)) / ((f2 . t0) ^2)) / (r ^2)),(((diff (f3,t0)) / (r ^2)) / ((f3 . t0) ^2))]|)
by XCMPLX_1:48
.=
- (r * |[(((diff (f1,t0)) / ((f1 . t0) ^2)) / (r ^2)),(((diff (f2,t0)) / ((f2 . t0) ^2)) / (r ^2)),(((diff (f3,t0)) / ((f3 . t0) ^2)) / (r ^2))]|)
by XCMPLX_1:48
.=
- (r * |[(((diff (f1,t0)) / ((f1 . t0) ^2)) / ((1 / (r ^2)) ")),(((diff (f2,t0)) / ((f2 . t0) ^2)) / (r ^2)),(((diff (f3,t0)) / ((f3 . t0) ^2)) / (r ^2))]|)
by XCMPLX_1:219
.=
- (r * |[((1 / (r ^2)) * ((diff (f1,t0)) / ((f1 . t0) ^2))),(((diff (f2,t0)) / ((f2 . t0) ^2)) / (r ^2)),(((diff (f3,t0)) / ((f3 . t0) ^2)) / (r ^2))]|)
by XCMPLX_1:221
.=
- (r * |[((1 / (r ^2)) * ((diff (f1,t0)) / ((f1 . t0) ^2))),(((diff (f2,t0)) / ((f2 . t0) ^2)) / ((1 / (r ^2)) ")),(((diff (f3,t0)) / ((f3 . t0) ^2)) / (r ^2))]|)
by XCMPLX_1:219
.=
- (r * |[((1 / (r ^2)) * ((diff (f1,t0)) / ((f1 . t0) ^2))),((1 / (r ^2)) * ((diff (f2,t0)) / ((f2 . t0) ^2))),(((diff (f3,t0)) / ((f3 . t0) ^2)) / (r ^2))]|)
by XCMPLX_1:221
.=
- (r * |[((1 / (r ^2)) * ((diff (f1,t0)) / ((f1 . t0) ^2))),((1 / (r ^2)) * ((diff (f2,t0)) / ((f2 . t0) ^2))),(((diff (f3,t0)) / ((f3 . t0) ^2)) / ((1 / (r ^2)) "))]|)
by XCMPLX_1:219
.=
- (r * |[((1 / (r ^2)) * ((diff (f1,t0)) / ((f1 . t0) ^2))),((1 / (r ^2)) * ((diff (f2,t0)) / ((f2 . t0) ^2))),((1 / (r ^2)) * ((diff (f3,t0)) / ((f3 . t0) ^2)))]|)
by XCMPLX_1:221
.=
- (r * ((1 / (r ^2)) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|))
by LmA8
.=
- ((r * (1 / (r ^2))) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)
by EUCLID_4:4
.=
- (((r * 1) / (r ^2)) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)
by XCMPLX_1:75
.=
- (((r / r) / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)
by XCMPLX_1:79
.=
- ((1 / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)
by B0, XCMPLX_1:60
;
hence
VFuncdiff (((r (#) f1) ^),((r (#) f2) ^),((r (#) f3) ^),t0) = - ((1 / r) * |[((diff (f1,t0)) / ((f1 . t0) ^2)),((diff (f2,t0)) / ((f2 . t0) ^2)),((diff (f3,t0)) / ((f3 . t0) ^2))]|)
; verum