let X, Y, W be RealNormSpace; for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st Z is open holds
( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z iff ( f is_differentiable_on Z & f `| Z is_continuous_on Z ) )
let Z be Subset of [:X,Y:]; for f being PartFunc of [:X,Y:],W st Z is open holds
( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z iff ( f is_differentiable_on Z & f `| Z is_continuous_on Z ) )
let f be PartFunc of [:X,Y:],W; ( Z is open implies ( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z iff ( f is_differentiable_on Z & f `| Z is_continuous_on Z ) ) )
assume AS:
Z is open
; ( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z iff ( f is_differentiable_on Z & f `| Z is_continuous_on 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;
((IsoCPNrSP (X,Y)) ") " Z = (IsoCPNrSP (X,Y)) .: Z
by FUNCT_1:84;
then OP1:
((IsoCPNrSP (X,Y)) ") " Z is open
by AS, LM025;
D1: dom <*X,Y*> =
Seg (len <*X,Y*>)
by FINSEQ_1:def 3
.=
Seg 2
by FINSEQ_1:44
;
then D2:
1 in dom <*X,Y*>
;
then
In (1,(dom <*X,Y*>)) = 1
by SUBSET_1:def 8;
then BX1:
<*X,Y*> . (In (1,(dom <*X,Y*>))) = X
by FINSEQ_1:44;
D3:
2 in dom <*X,Y*>
by D1;
then
In (2,(dom <*X,Y*>)) = 2
by SUBSET_1:def 8;
then BX2:
<*X,Y*> . (In (2,(dom <*X,Y*>))) = Y
by FINSEQ_1:44;
JE1: (IsoCPNrSP (X,Y)) " (((IsoCPNrSP (X,Y)) ") " Z) =
((IsoCPNrSP (X,Y)) ") .: (((IsoCPNrSP (X,Y)) ") " Z)
by FUNCT_1:85
.=
Z
by X1, FUNCT_1:77
;
hereby ( f is_differentiable_on Z & f `| Z is_continuous_on Z implies ( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z ) )
assume P1:
(
f is_partial_differentiable_on`1 Z &
f is_partial_differentiable_on`2 Z &
f `partial`1| Z is_continuous_on Z &
f `partial`2| Z is_continuous_on Z )
;
( f is_differentiable_on Z & f `| Z is_continuous_on Z )P2:
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1
by P1, LM300;
P3:
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2
by P1, LM300;
P4:
f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))
by LM400, P1;
P5:
f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))
by LM401, P1;
for
i being
set st
i in dom <*X,Y*> holds
(
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,
i &
(f * ((IsoCPNrSP (X,Y)) ")) `partial| (
(((IsoCPNrSP (X,Y)) ") " Z),
i)
is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )
proof
let i be
set ;
( i in dom <*X,Y*> implies ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,i & (f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),i) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z ) )
assume CX:
i in dom <*X,Y*>
;
( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,i & (f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),i) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )
then C1:
(
i = 1 or
i = 2 )
by D1, TARSKI:def 2, FINSEQ_1:2;
thus
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,
i
by CX, D1, P2, P3, TARSKI:def 2, FINSEQ_1:2;
(f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),i) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z
thus
(f * ((IsoCPNrSP (X,Y)) ")) `partial| (
(((IsoCPNrSP (X,Y)) ") " Z),
i)
is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z
by BX1, BX2, C1, P1, P4, P5, JE1, LM045;
verum
end; then GF1:
(
f * ((IsoCPNrSP (X,Y)) ") is_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z &
(f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )
by NDIFF_5:57, OP1;
hence
f is_differentiable_on Z
by LM155;
f `| Z is_continuous_on Zhence
f `| Z is_continuous_on Z
by GF1, LMX1;
verum
end;
assume X0:
( f is_differentiable_on Z & f `| Z is_continuous_on Z )
; ( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z )
then X1:
f * ((IsoCPNrSP (X,Y)) ") is_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z
by LM155;
X3:
(f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z
by X0, LMX1;
P2:
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1
by D2, OP1, X1, X3, NDIFF_5:57;
hence
f is_partial_differentiable_on`1 Z
by LM300; ( f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z )
P3:
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2
by D3, OP1, X1, X3, NDIFF_5:57;
hence
f is_partial_differentiable_on`2 Z
by LM300; ( f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z )
P6:
(f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z
by D2, OP1, X1, X3, NDIFF_5:57;
P7:
(f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z
by D3, OP1, X1, X3, NDIFF_5:57;
f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))
by P2, LM300, LM400;
hence
f `partial`1| Z is_continuous_on Z
by BX1, P6, LM045, JE1; f `partial`2| Z is_continuous_on Z
f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))
by P3, LM300, LM401;
hence
f `partial`2| Z is_continuous_on Z
by BX2, P7, LM045, JE1; verum