let W be RealNormSpace; for X, Y being RealNormSpace
for f being PartFunc of (product <*X,Y*>),W
for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds
for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")
let X, Y be RealNormSpace; for f being PartFunc of (product <*X,Y*>),W
for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds
for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")
let f be PartFunc of (product <*X,Y*>),W; for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds
for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")
let D be Subset of (product <*X,Y*>); ( f is_differentiable_on D implies for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ") )
assume AS2:
f is_differentiable_on D
; for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")
then OP1:
D is open
by NDIFF_1:32;
set I = IsoCPNrSP (X,Y);
X1:
( IsoCPNrSP (X,Y) is one-to-one & IsoCPNrSP (X,Y) is onto & ( for x being Point of X
for y being Point of Y holds (IsoCPNrSP (X,Y)) . (x,y) = <*x,y*> ) & 0. (product <*X,Y*>) = (IsoCPNrSP (X,Y)) . (0. [:X,Y:]) & IsoCPNrSP (X,Y) is isometric )
by defISO, ZeZe;
set J = (IsoCPNrSP (X,Y)) " ;
P1:
( dom (f `| D) = D & ( for x being Point of (product <*X,Y*>) st x in D holds
(f `| D) /. x = diff (f,x) ) )
by NDIFF_1:def 9, AS2;
set g = f * (IsoCPNrSP (X,Y));
set E = (IsoCPNrSP (X,Y)) " D;
P3:
f * (IsoCPNrSP (X,Y)) is_differentiable_on (IsoCPNrSP (X,Y)) " D
by LM155, AS2;
for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")
proof
let z be
Point of
(product <*X,Y*>);
( z in dom (f `| D) implies (f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ") )
assume F1:
z in dom (f `| D)
;
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")
then F2:
(f `| D) . z =
(f `| D) /. z
by PARTFUN1:def 6
.=
diff (
f,
z)
by F1, P1
;
F3:
f is_differentiable_in z
by F1, OP1, P1, AS2, NDIFF_1:31;
consider w being
Point of
[:X,Y:] such that F4:
z = (IsoCPNrSP (X,Y)) . w
by X1, FUNCT_2:113;
reconsider I0 =
IsoCPNrSP (
X,
Y) as
Point of
(R_NormSpace_of_BoundedLinearOperators ([:X,Y:],(product <*X,Y*>))) by LOPBAN_1:def 9;
F11:
((diff (f,z)) * I0) * (I0 ") =
(modetrans ((diff (f,z)),(product <*X,Y*>),W)) * ((modetrans (I0,[:X,Y:],(product <*X,Y*>))) * (I0 "))
by RELAT_1:36
.=
(modetrans ((diff (f,z)),(product <*X,Y*>),W)) * ((IsoCPNrSP (X,Y)) * ((IsoCPNrSP (X,Y)) "))
by LOPBAN_1:def 11
.=
(modetrans ((diff (f,z)),(product <*X,Y*>),W)) * (id (rng I0))
by FUNCT_1:39
.=
modetrans (
(diff (f,z)),
(product <*X,Y*>),
W)
by X1, FUNCT_2:17
.=
(f `| D) . z
by F2, LOPBAN_1:def 11
;
w in (IsoCPNrSP (X,Y)) " D
by F1, F4, P1, FUNCT_2:38;
then F12:
(((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. w) * (I0 ") = (diff ((f * (IsoCPNrSP (X,Y))),w)) * (I0 ")
by P3, NDIFF_1:def 9;
F13:
w = ((IsoCPNrSP (X,Y)) ") . z
by F4, FUNCT_2:26;
thus
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")
by F3, F4, F11, F12, F13, LM120;
verum
end;
hence
for z being Point of (product <*X,Y*>) st z in dom (f `| D) holds
(f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ")
; verum