let X, Y, W be RealNormSpace; for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( ( f is_partial_differentiable_on`1 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z ) & ( f is_partial_differentiable_on`2 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z ) )
let Z be Subset of [:X,Y:]; for f being PartFunc of [:X,Y:],W holds
( ( f is_partial_differentiable_on`1 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z ) & ( f is_partial_differentiable_on`2 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z ) )
let f be PartFunc of [:X,Y:],W; ( ( f is_partial_differentiable_on`1 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z ) & ( f is_partial_differentiable_on`2 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z ) )
set I = (IsoCPNrSP (X,Y)) " ;
set J = IsoCPNrSP (X,Y);
set g = f * ((IsoCPNrSP (X,Y)) ");
set E = ((IsoCPNrSP (X,Y)) ") " Z;
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;
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;
A1:
dom (f * ((IsoCPNrSP (X,Y)) ")) = ((IsoCPNrSP (X,Y)) ") " (dom f)
by RELAT_1:147;
A2:
dom (IsoCPNrSP (X,Y)) = the carrier of [:X,Y:]
by FUNCT_2:def 1;
thus
( f is_partial_differentiable_on`1 Z iff f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 )
( f is_partial_differentiable_on`2 Z iff f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 )proof
hereby ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z )
assume P2:
f is_partial_differentiable_on`1 Z
;
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1
for
w being
Point of
(product <*X,Y*>) st
w in ((IsoCPNrSP (X,Y)) ") " Z holds
(f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,1
proof
let w be
Point of
(product <*X,Y*>);
( w in ((IsoCPNrSP (X,Y)) ") " Z implies (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,1 )
assume A4:
w in ((IsoCPNrSP (X,Y)) ") " Z
;
(f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,1
consider z being
Point of
[:X,Y:] such that F4:
w = (IsoCPNrSP (X,Y)) . z
by X2, FUNCT_2:113;
((IsoCPNrSP (X,Y)) ") . w = z
by A2, F4, FUNCT_1:34;
then
z in Z
by A4, FUNCT_2:38;
then
(f | Z) * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1
by P2, LM200;
hence
(f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,1
by F4, FX1;
verum
end; hence
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1
by A1, P2, RELAT_1:143;
verum
end;
assume P2:
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1
;
f is_partial_differentiable_on`1 Z
then P3:
((IsoCPNrSP (X,Y)) ") " Z c= ((IsoCPNrSP (X,Y)) ") " (dom f)
by RELAT_1:147;
for
z being
Point of
[:X,Y:] st
z in Z holds
f | Z is_partial_differentiable_in`1 z
proof
let z be
Point of
[:X,Y:];
( z in Z implies f | Z is_partial_differentiable_in`1 z )
assume A4:
z in Z
;
f | Z is_partial_differentiable_in`1 z
set w =
(IsoCPNrSP (X,Y)) . z;
((IsoCPNrSP (X,Y)) ") . ((IsoCPNrSP (X,Y)) . z) = z
by A2, FUNCT_1:34;
then F4:
(IsoCPNrSP (X,Y)) . z in ((IsoCPNrSP (X,Y)) ") " Z
by FUNCT_2:38, A4;
(f | Z) * ((IsoCPNrSP (X,Y)) ") = (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z)
by FX1;
hence
f | Z is_partial_differentiable_in`1 z
by F4, P2, LM200;
verum
end;
hence
f is_partial_differentiable_on`1 Z
by P3, X1, FUNCT_1:88;
verum
end;
thus
( f is_partial_differentiable_on`2 Z iff f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 )
verumproof
hereby ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z )
assume P2:
f is_partial_differentiable_on`2 Z
;
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2
for
w being
Point of
(product <*X,Y*>) st
w in ((IsoCPNrSP (X,Y)) ") " Z holds
(f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,2
proof
let w be
Point of
(product <*X,Y*>);
( w in ((IsoCPNrSP (X,Y)) ") " Z implies (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,2 )
assume A4:
w in ((IsoCPNrSP (X,Y)) ") " Z
;
(f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,2
consider z being
Point of
[:X,Y:] such that F4:
w = (IsoCPNrSP (X,Y)) . z
by X2, FUNCT_2:113;
F8:
((IsoCPNrSP (X,Y)) ") . w = z
by A2, F4, FUNCT_1:34;
((IsoCPNrSP (X,Y)) ") . w in Z
by FUNCT_2:38, A4;
then
(f | Z) * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2
by F8, P2, LM200;
hence
(f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,2
by F4, FX1;
verum
end; hence
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2
by A1, P2, RELAT_1:143;
verum
end;
assume P2:
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2
;
f is_partial_differentiable_on`2 Z
P3:
((IsoCPNrSP (X,Y)) ") " Z c= ((IsoCPNrSP (X,Y)) ") " (dom f)
by P2, RELAT_1:147;
for
z being
Point of
[:X,Y:] st
z in Z holds
f | Z is_partial_differentiable_in`2 z
proof
let z be
Point of
[:X,Y:];
( z in Z implies f | Z is_partial_differentiable_in`2 z )
assume A4:
z in Z
;
f | Z is_partial_differentiable_in`2 z
set w =
(IsoCPNrSP (X,Y)) . z;
((IsoCPNrSP (X,Y)) ") . ((IsoCPNrSP (X,Y)) . z) = z
by A2, FUNCT_1:34;
then F4:
(IsoCPNrSP (X,Y)) . z in ((IsoCPNrSP (X,Y)) ") " Z
by FUNCT_2:38, A4;
(f | Z) * ((IsoCPNrSP (X,Y)) ") = (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z)
by FX1;
hence
f | Z is_partial_differentiable_in`2 z
by F4, P2, LM200;
verum
end;
hence
f is_partial_differentiable_on`2 Z
by P3, X1, FUNCT_1:88;
verum
end;