let i be Nat; for E, F, G being RealNormSpace
for Z being non empty Subset of [:E,F:]
for f being PartFunc of [:E,F:],G st f is_differentiable_on i + 1,Z holds
( f `partial`1| Z is_differentiable_on i,Z & f `partial`2| Z is_differentiable_on i,Z )
let E, F, G be RealNormSpace; for Z being non empty Subset of [:E,F:]
for f being PartFunc of [:E,F:],G st f is_differentiable_on i + 1,Z holds
( f `partial`1| Z is_differentiable_on i,Z & f `partial`2| Z is_differentiable_on i,Z )
let Z be non empty Subset of [:E,F:]; for f being PartFunc of [:E,F:],G st f is_differentiable_on i + 1,Z holds
( f `partial`1| Z is_differentiable_on i,Z & f `partial`2| Z is_differentiable_on i,Z )
let f be PartFunc of [:E,F:],G; ( f is_differentiable_on i + 1,Z implies ( f `partial`1| Z is_differentiable_on i,Z & f `partial`2| Z is_differentiable_on i,Z ) )
assume A1:
f is_differentiable_on i + 1,Z
; ( f `partial`1| Z is_differentiable_on i,Z & f `partial`2| Z is_differentiable_on i,Z )
0 <= i
by NAT_1:2;
then
f is_differentiable_on 0 + 1,Z
by A1, NDIFF_6:17, XREAL_1:7;
then A2:
f is_differentiable_on Z
by NDIFF_6:15, Th3;
then A3:
( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & ( for z being Point of [:E,F:] st z in Z holds
( ( for dx being Point of E holds ((f `partial`1| Z) /. z) . dx = ((f `| Z) /. z) . (dx,(0. F)) ) & ( for dy being Point of F holds ((f `partial`2| Z) /. z) . dy = ((f `| Z) /. z) . ((0. E),dy) ) ) ) )
by Th45;
A4:
Z is open
by A2, NDIFF_1:32;
set PD1 = f `partial`1| Z;
set PD2 = f `partial`2| Z;
A5:
( dom (f `partial`1| Z) = Z & dom (f `partial`2| Z) = Z )
by A3, NDIFF_7:def 10, NDIFF_7:def 11;
consider L10 being Lipschitzian LinearOperator of E,[:E,F:] such that
A6:
for dx being Point of E holds L10 . dx = [dx,(0. F)]
by Th46;
consider L20 being Lipschitzian LinearOperator of F,[:E,F:] such that
A7:
for dy being Point of F holds L20 . dy = [(0. E),dy]
by Th47;
set BL1 = R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]);
set BL2 = R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]);
A8:
( dom (Z --> L10) = Z & rng (Z --> L10) c= {L10} )
by FUNCOP_1:13;
L10 in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]))
by LOPBAN_1:def 9;
then
{L10} c= the carrier of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]))
by ZFMISC_1:31;
then A9:
rng (Z --> L10) c= the carrier of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]))
by XBOOLE_1:1;
reconsider L1 = Z --> L10 as PartFunc of [:E,F:],(R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])) by A8, A9, RELSET_1:4;
reconsider L100 = L10 as Point of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])) by LOPBAN_1:def 9;
L1 = Z --> L100
;
then A10:
L1 is_differentiable_on i,Z
by A4, Th50;
A11:
for z being Point of [:E,F:] st z in Z holds
(f `partial`1| Z) /. z = ((f `| Z) /. z) * (L1 /. z)
proof
let z be
Point of
[:E,F:];
( z in Z implies (f `partial`1| Z) /. z = ((f `| Z) /. z) * (L1 /. z) )
assume A12:
z in Z
;
(f `partial`1| Z) /. z = ((f `| Z) /. z) * (L1 /. z)
then A13:
L1 /. z =
L1 . z
by A8, PARTFUN1:def 6
.=
L10
by A12, FUNCOP_1:7
;
reconsider H1 =
(f `| Z) /. z as
Lipschitzian LinearOperator of
[:E,F:],
G by LOPBAN_1:def 9;
reconsider H2 =
L1 /. z as
Lipschitzian LinearOperator of
E,
[:E,F:] by A13;
A14:
(f `partial`1| Z) /. z is
Lipschitzian LinearOperator of
E,
G
by LOPBAN_1:def 9;
then A15:
dom ((f `partial`1| Z) /. z) = the
carrier of
E
by FUNCT_2:def 1;
A16:
modetrans (
(L1 /. z),
E,
[:E,F:])
= H2
by LOPBAN_1:def 11;
A17:
dom (H1 * H2) = the
carrier of
E
by FUNCT_2:def 1;
A18:
for
dx being
object st
dx in dom ((f `partial`1| Z) /. z) holds
((f `partial`1| Z) /. z) . dx = (H1 * H2) . dx
(f `partial`1| Z) /. z = H1 * H2
by A15, A17, A18, FUNCT_1:2;
hence
(f `partial`1| Z) /. z = ((f `| Z) /. z) * (L1 /. z)
by A16, LOPBAN_1:def 11;
verum
end;
A20:
f `| Z is_differentiable_on i,Z
by A1, Th36;
consider B being Lipschitzian BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)),(R_NormSpace_of_BoundedLinearOperators (E,G)) such that
A21:
for u being Point of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:]))
for v being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) holds B . (u,v) = v * u
by Th38;
set w2 = <:L1,(f `| Z):>;
A22: dom <:L1,(f `| Z):> =
(dom (f `| Z)) /\ (dom L1)
by FUNCT_3:def 7
.=
Z /\ (dom L1)
by A2, NDIFF_1:def 9
.=
Z
by A8
;
A23:
rng <:L1,(f `| Z):> c= [:(rng L1),(rng (f `| Z)):]
by FUNCT_3:51;
[:(rng L1),(rng (f `| Z)):] c= [: the carrier of (R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])), the carrier of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by ZFMISC_1:96;
then
rng <:L1,(f `| Z):> c= the carrier of [:(R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by A23, XBOOLE_1:1;
then reconsider w2 = <:L1,(f `| Z):> as PartFunc of [:E,F:],[:(R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):] by RELSET_1:4, A22;
reconsider W = B * w2 as PartFunc of [:E,F:],(R_NormSpace_of_BoundedLinearOperators (E,G)) ;
A24:
W is_differentiable_on i,Z
by A10, A20, Th39;
dom B = the carrier of [:(R_NormSpace_of_BoundedLinearOperators (E,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by FUNCT_2:def 1;
then
rng w2 c= dom B
;
then A25:
dom W = Z
by A22, RELAT_1:27;
for x0 being object st x0 in dom (f `partial`1| Z) holds
(f `partial`1| Z) . x0 = W . x0
proof
let x0 be
object ;
( x0 in dom (f `partial`1| Z) implies (f `partial`1| Z) . x0 = W . x0 )
assume A26:
x0 in dom (f `partial`1| Z)
;
(f `partial`1| Z) . x0 = W . x0
then reconsider x =
x0 as
Point of
[:E,F:] ;
A27:
(f `partial`1| Z) . x0 =
(f `partial`1| Z) /. x
by A26, PARTFUN1:def 6
.=
((f `| Z) /. x) * (L1 /. x)
by A11, A26, A5
.=
B . (
(L1 /. x),
((f `| Z) /. x))
by A21
.=
B . [(L1 /. x),((f `| Z) /. x)]
by BINOP_1:def 1
;
A28:
dom (f `| Z) = Z
by A2, NDIFF_1:def 9;
A29:
dom <:L1,(f `| Z):> =
(dom L1) /\ (dom (f `| Z))
by FUNCT_3:def 7
.=
Z
by A8, A28
;
[(L1 /. x),((f `| Z) /. x)] =
[(L1 . x),((f `| Z) /. x)]
by A5, A8, A26, PARTFUN1:def 6
.=
[(L1 . x),((f `| Z) . x)]
by A5, A26, A28, PARTFUN1:def 6
.=
w2 . x
by A5, A26, A29, FUNCT_3:def 7
;
hence
(f `partial`1| Z) . x0 = W . x0
by A5, A26, A27, A29, FUNCT_1:13;
verum
end;
hence
f `partial`1| Z is_differentiable_on i,Z
by A5, A24, A25, FUNCT_1:2; f `partial`2| Z is_differentiable_on i,Z
A30:
( dom (Z --> L20) = Z & rng (Z --> L20) c= {L20} )
by FUNCOP_1:13;
L20 in the carrier of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]))
by LOPBAN_1:def 9;
then
{L20} c= the carrier of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]))
by ZFMISC_1:31;
then A31:
rng (Z --> L20) c= the carrier of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]))
by XBOOLE_1:1;
reconsider L2 = Z --> L20 as PartFunc of [:E,F:],(R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])) by A30, A31, RELSET_1:4;
reconsider L100 = L20 as Point of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])) by LOPBAN_1:def 9;
L2 = Z --> L100
;
then A32:
L2 is_differentiable_on i,Z
by A4, Th50;
A33:
( dom (Z --> L20) = Z & rng (Z --> L20) c= {L20} )
by FUNCOP_1:13;
A34:
for z being Point of [:E,F:] st z in Z holds
(f `partial`2| Z) /. z = ((f `| Z) /. z) * (L2 /. z)
proof
let z be
Point of
[:E,F:];
( z in Z implies (f `partial`2| Z) /. z = ((f `| Z) /. z) * (L2 /. z) )
assume A35:
z in Z
;
(f `partial`2| Z) /. z = ((f `| Z) /. z) * (L2 /. z)
then A36:
L2 /. z =
L2 . z
by A33, PARTFUN1:def 6
.=
L20
by A35, FUNCOP_1:7
;
reconsider H1 =
(f `| Z) /. z as
Lipschitzian LinearOperator of
[:E,F:],
G by LOPBAN_1:def 9;
reconsider H2 =
L2 /. z as
Lipschitzian LinearOperator of
F,
[:E,F:] by A36;
A37:
(f `partial`2| Z) /. z is
Lipschitzian LinearOperator of
F,
G
by LOPBAN_1:def 9;
then A38:
dom ((f `partial`2| Z) /. z) = the
carrier of
F
by FUNCT_2:def 1;
A39:
modetrans (
(L2 /. z),
F,
[:E,F:])
= H2
by LOPBAN_1:def 11;
A40:
dom (H1 * H2) = the
carrier of
F
by FUNCT_2:def 1;
A41:
for
dx being
object st
dx in dom ((f `partial`2| Z) /. z) holds
((f `partial`2| Z) /. z) . dx = (H1 * H2) . dx
(f `partial`2| Z) /. z = H1 * H2
by A38, A40, A41, FUNCT_1:2;
hence
(f `partial`2| Z) /. z = ((f `| Z) /. z) * (L2 /. z)
by A39, LOPBAN_1:def 11;
verum
end;
A43:
f `| Z is_differentiable_on i,Z
by A1, Th36;
consider B being Lipschitzian BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)),(R_NormSpace_of_BoundedLinearOperators (F,G)) such that
A44:
for u being Point of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:]))
for v being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) holds B . (u,v) = v * u
by Th38;
set w2 = <:L2,(f `| Z):>;
A45: dom <:L2,(f `| Z):> =
(dom (f `| Z)) /\ (dom L2)
by FUNCT_3:def 7
.=
Z /\ (dom L2)
by A2, NDIFF_1:def 9
.=
Z
by A33
;
A46:
rng <:L2,(f `| Z):> c= [:(rng L2),(rng (f `| Z)):]
by FUNCT_3:51;
[:(rng L2),(rng (f `| Z)):] c= [: the carrier of (R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])), the carrier of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by ZFMISC_1:96;
then
rng <:L2,(f `| Z):> c= the carrier of [:(R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by A46, XBOOLE_1:1;
then reconsider w2 = <:L2,(f `| Z):> as PartFunc of [:E,F:],[:(R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):] by A45, RELSET_1:4;
reconsider W = B * w2 as PartFunc of [:E,F:],(R_NormSpace_of_BoundedLinearOperators (F,G)) ;
dom B = the carrier of [:(R_NormSpace_of_BoundedLinearOperators (F,[:E,F:])),(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)):]
by FUNCT_2:def 1;
then
rng w2 c= dom B
;
then A47:
dom W = Z
by A45, RELAT_1:27;
for x0 being object st x0 in dom (f `partial`2| Z) holds
(f `partial`2| Z) . x0 = W . x0
proof
let x0 be
object ;
( x0 in dom (f `partial`2| Z) implies (f `partial`2| Z) . x0 = W . x0 )
assume A48:
x0 in dom (f `partial`2| Z)
;
(f `partial`2| Z) . x0 = W . x0
then reconsider x =
x0 as
Point of
[:E,F:] ;
A49:
(f `partial`2| Z) . x0 =
(f `partial`2| Z) /. x
by A48, PARTFUN1:def 6
.=
((f `| Z) /. x) * (L2 /. x)
by A5, A34, A48
.=
B . (
(L2 /. x),
((f `| Z) /. x))
by A44
.=
B . [(L2 /. x),((f `| Z) /. x)]
by BINOP_1:def 1
;
A50:
dom (f `| Z) = Z
by A2, NDIFF_1:def 9;
A51:
dom <:L2,(f `| Z):> =
(dom L2) /\ (dom (f `| Z))
by FUNCT_3:def 7
.=
Z
by A33, A50
;
[(L2 /. x),((f `| Z) /. x)] =
[(L2 . x),((f `| Z) /. x)]
by A5, A33, A48, PARTFUN1:def 6
.=
[(L2 . x),((f `| Z) . x)]
by A5, A48, A50, PARTFUN1:def 6
.=
w2 . x
by A5, A48, A51, FUNCT_3:def 7
;
hence
(f `partial`2| Z) . x0 = W . x0
by A5, A48, A49, A51, FUNCT_1:13;
verum
end;
then
f `partial`2| Z = W
by A5, A47, FUNCT_1:2;
hence
f `partial`2| Z is_differentiable_on i,Z
by A32, A43, Th39; verum