let W be RealNormSpace; for X, Y being RealNormSpace
for f being PartFunc of [:X,Y:],W
for D being Subset of [:X,Y:] st f is_differentiable_on D holds
for z being Point of [: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 [:X,Y:],W
for D being Subset of [:X,Y:] st f is_differentiable_on D holds
for z being Point of [: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 [:X,Y:],W; for D being Subset of [:X,Y:] st f is_differentiable_on D holds
for z being Point of [: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 [:X,Y:]; ( f is_differentiable_on D implies for z being Point of [: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 [: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)) " = (IsoCPNrSP (X,Y)) " & (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. [:X,Y:] = ((IsoCPNrSP (X,Y)) ") . (0. (product <*X,Y*>)) & (IsoCPNrSP (X,Y)) " is isometric )
by defISOA1, defISOA2;
set J = IsoCPNrSP (X,Y);
X2:
( 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;
P1:
( dom (f `| D) = D & ( for x being Point of [: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 [: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
[: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 F1X:
z in dom (f `| D)
;
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")
then F1:
z in D
by AS2, NDIFF_1:def 9;
F2:
(f `| D) . z =
(f `| D) /. z
by F1X, PARTFUN1:def 6
.=
diff (
f,
z)
by F1X, P1
;
F3:
f is_differentiable_in z
by F1, OP1, AS2, NDIFF_1:31;
consider w being
Point of
(product <*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 ((product <*X,Y*>),[:X,Y:])) by LOPBAN_1:def 9;
F9:
((diff (f,z)) * I0) * (I0 ") = (diff ((f * ((IsoCPNrSP (X,Y)) ")),w)) * (I0 ")
by F3, F4, LM120;
F11:
((diff (f,z)) * I0) * (I0 ") =
(modetrans ((diff (f,z)),[:X,Y:],W)) * ((modetrans (I0,(product <*X,Y*>),[:X,Y:])) * (I0 "))
by RELAT_1:36
.=
(modetrans ((diff (f,z)),[:X,Y:],W)) * (((IsoCPNrSP (X,Y)) ") * (((IsoCPNrSP (X,Y)) ") "))
by LOPBAN_1:def 11
.=
(modetrans ((diff (f,z)),[:X,Y:],W)) * (id (rng I0))
by FUNCT_1:39
.=
modetrans (
(diff (f,z)),
[:X,Y:],
W)
by X1, FUNCT_2:17
.=
(f `| D) . z
by F2, LOPBAN_1:def 11
;
w in ((IsoCPNrSP (X,Y)) ") " D
by F4, F1, FUNCT_2:38;
then
(((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. w) * (I0 ") = (diff ((f * ((IsoCPNrSP (X,Y)) ")),w)) * (I0 ")
by P3, NDIFF_1:def 9;
hence
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")
by F4, F9, F11, X2, FUNCT_1:35;
verum
end;
hence
for z being Point of [: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