let X, Y, W be RealNormSpace; :: thesis: for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st f is_differentiable_on Z holds
( f `| Z is_continuous_on Z iff (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )
let Z be Subset of [:X,Y:]; :: thesis: for f being PartFunc of [:X,Y:],W st f is_differentiable_on Z holds
( f `| Z is_continuous_on Z iff (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )
let f be PartFunc of [:X,Y:],W; :: thesis: ( f is_differentiable_on Z implies ( f `| Z is_continuous_on Z iff (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z ) )
assume AS1: f is_differentiable_on Z ; :: thesis: ( f `| Z is_continuous_on Z iff (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )
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;
set g = f * ((IsoCPNrSP (X,Y)) ");
set E = ((IsoCPNrSP (X,Y)) ") " Z;
A2: dom (IsoCPNrSP (X,Y)) = the carrier of [:X,Y:] by FUNCT_2:def 1;
IJ1: ((IsoCPNrSP (X,Y)) ") " = IsoCPNrSP (X,Y) by FUNCT_1:43;
AS2: f * ((IsoCPNrSP (X,Y)) ") is_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z by LM155, AS1;
P1: dom (f `| Z) = Z by AS1, NDIFF_1:def 9;
P2: dom ((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) = ((IsoCPNrSP (X,Y)) ") " Z by AS2, NDIFF_1:def 9;
set F = f `| Z;
set G = (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z);
hereby :: thesis: ( (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z implies f `| Z is_continuous_on Z )
assume Q2: f `| Z is_continuous_on Z ; :: thesis: (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z
for y0 being Point of (product <*X,Y*>)
for r being Real st y0 in ((IsoCPNrSP (X,Y)) ") " Z & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product <*X,Y*>) st y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - y0).|| < s holds
||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r ) )
proof
let y0 be Point of (product <*X,Y*>); :: thesis: for r being Real st y0 in ((IsoCPNrSP (X,Y)) ") " Z & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product <*X,Y*>) st y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - y0).|| < s holds
||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r ) )
let r be Real; :: thesis: ( y0 in ((IsoCPNrSP (X,Y)) ") " Z & 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (product <*X,Y*>) st y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - y0).|| < s holds
||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r ) ) )
assume H1: ( y0 in ((IsoCPNrSP (X,Y)) ") " Z & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Point of (product <*X,Y*>) st y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - y0).|| < s holds
||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r ) )
consider x0 being Point of [:X,Y:] such that
F4: y0 = (IsoCPNrSP (X,Y)) . x0 by X2, FUNCT_2:113;
F8: ((IsoCPNrSP (X,Y)) ") . y0 = x0 by A2, F4, FUNCT_1:34;
then F9: x0 in Z by H1, FUNCT_2:38;
then consider s being Real such that
F10: ( 0 < s & ( for x1 being Point of [:X,Y:] st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r ) ) by Q2, H1, NFCONT_1:19;
take s ; :: thesis: ( 0 < s & ( for y1 being Point of (product <*X,Y*>) st y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - y0).|| < s holds
||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r ) )
thus 0 < s by F10; :: thesis: for y1 being Point of (product <*X,Y*>) st y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - y0).|| < s holds
||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r
thus for y1 being Point of (product <*X,Y*>) st y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - y0).|| < s holds
||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r :: thesis: verum
proof
let y1 be Point of (product <*X,Y*>); :: thesis: ( y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - y0).|| < s implies ||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r )
assume H3: ( y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - y0).|| < s ) ; :: thesis: ||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r
consider x1 being Point of [:X,Y:] such that
G4: y1 = (IsoCPNrSP (X,Y)) . x1 by X2, FUNCT_2:113;
G8: ((IsoCPNrSP (X,Y)) ") . y1 = x1 by A2, G4, FUNCT_1:34;
then G9: x1 in Z by H3, FUNCT_2:38;
||.(x1 - x0).|| = ||.(y1 - y0).|| by X1, F8, G8;
then H5: ||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r by F10, G9, H3;
H7: (f `| Z) /. x1 = (f `| Z) . x1 by G9, P1, PARTFUN1:def 6
.= (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) * (IsoCPNrSP (X,Y)) by AS1, G4, G9, P1, IJ1, LM166 ;
H8: (f `| Z) /. x0 = (f `| Z) . x0 by F9, P1, PARTFUN1:def 6
.= (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0) * (IsoCPNrSP (X,Y)) by AS1, F4, F9, P1, IJ1, LM166 ;
reconsider Gy1y0 = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0) as Lipschitzian LinearOperator of (product <*X,Y*>),W by LOPBAN_1:def 9;
reconsider Fx1x0 = ((f `| Z) /. x1) - ((f `| Z) /. x0) as Lipschitzian LinearOperator of [:X,Y:],W by LOPBAN_1:def 9;
now :: thesis: for t being VECTOR of [:X,Y:] holds (Gy1y0 * (IsoCPNrSP (X,Y))) . t = Fx1x0 . t
let t be VECTOR of [:X,Y:]; :: thesis: (Gy1y0 * (IsoCPNrSP (X,Y))) . t = Fx1x0 . t
U2: (((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)) * (IsoCPNrSP (X,Y))) . t = ((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)) . ((IsoCPNrSP (X,Y)) . t) by A2, FUNCT_1:13
.= ((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) . ((IsoCPNrSP (X,Y)) . t)) - ((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0) . ((IsoCPNrSP (X,Y)) . t)) by LOPBAN_1:40 ;
U3: ((f `| Z) /. x1) . t = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) . ((IsoCPNrSP (X,Y)) . t) by A2, H7, FUNCT_1:13;
((f `| Z) /. x0) . t = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0) . ((IsoCPNrSP (X,Y)) . t) by A2, H8, FUNCT_1:13;
hence (Gy1y0 * (IsoCPNrSP (X,Y))) . t = Fx1x0 . t by U2, U3, LOPBAN_1:40; :: thesis: verum
end;
then Gy1y0 * (IsoCPNrSP (X,Y)) = Fx1x0 ;
hence ||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y0)).|| < r by H5, LMX00; :: thesis: verum
end;
end;
hence (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z by P2, NFCONT_1:19; :: thesis: verum
end;
assume Q2: (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z ; :: thesis: f `| Z is_continuous_on Z
for x0 being Point of [:X,Y:]
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of [:X,Y:] st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r ) )
proof
let x0 be Point of [:X,Y:]; :: thesis: for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of [:X,Y:] st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r ) )
let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of [:X,Y:] st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r ) ) )
assume H1: ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of [:X,Y:] st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r ) )
set y0 = (IsoCPNrSP (X,Y)) . x0;
((IsoCPNrSP (X,Y)) ") . ((IsoCPNrSP (X,Y)) . x0) = x0 by A2, FUNCT_1:34;
then (IsoCPNrSP (X,Y)) . x0 in ((IsoCPNrSP (X,Y)) ") " Z by FUNCT_2:38, H1;
then consider s being Real such that
F10: ( 0 < s & ( for y1 being Point of (product <*X,Y*>) st y1 in ((IsoCPNrSP (X,Y)) ") " Z & ||.(y1 - ((IsoCPNrSP (X,Y)) . x0)).|| < s holds
||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. y1) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x0))).|| < r ) ) by H1, Q2, NFCONT_1:19;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of [:X,Y:] st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r ) )
thus 0 < s by F10; :: thesis: for x1 being Point of [:X,Y:] st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r
let x1 be Point of [:X,Y:]; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s implies ||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r )
assume H3: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis: ||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r
set y1 = (IsoCPNrSP (X,Y)) . x1;
((IsoCPNrSP (X,Y)) ") . ((IsoCPNrSP (X,Y)) . x1) = x1 by A2, FUNCT_1:34;
then G9: (IsoCPNrSP (X,Y)) . x1 in ((IsoCPNrSP (X,Y)) ") " Z by FUNCT_2:38, H3;
||.(((IsoCPNrSP (X,Y)) . x1) - ((IsoCPNrSP (X,Y)) . x0)).|| = ||.(x1 - x0).|| by X2;
then H5: ||.((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x1)) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x0))).|| < r by F10, G9, H3;
H7: (f `| Z) /. x1 = (f `| Z) . x1 by H3, P1, PARTFUN1:def 6
.= (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x1)) * (IsoCPNrSP (X,Y)) by AS1, H3, IJ1, P1, LM166 ;
H8: (f `| Z) /. x0 = (f `| Z) . x0 by H1, P1, PARTFUN1:def 6
.= (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x0)) * (IsoCPNrSP (X,Y)) by AS1, H1, IJ1, P1, LM166 ;
reconsider Gy1y0 = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x1)) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x0)) as Lipschitzian LinearOperator of (product <*X,Y*>),W by LOPBAN_1:def 9;
reconsider Fx1x0 = ((f `| Z) /. x1) - ((f `| Z) /. x0) as Lipschitzian LinearOperator of [:X,Y:],W by LOPBAN_1:def 9;
now :: thesis: for t being VECTOR of [:X,Y:] holds (Gy1y0 * (IsoCPNrSP (X,Y))) . t = Fx1x0 . t
let t be VECTOR of [:X,Y:]; :: thesis: (Gy1y0 * (IsoCPNrSP (X,Y))) . t = Fx1x0 . t
U2: (((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x1)) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x0))) * (IsoCPNrSP (X,Y))) . t = ((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x1)) - (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x0))) . ((IsoCPNrSP (X,Y)) . t) by A2, FUNCT_1:13
.= ((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x1)) . ((IsoCPNrSP (X,Y)) . t)) - ((((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x0)) . ((IsoCPNrSP (X,Y)) . t)) by LOPBAN_1:40 ;
U3: ((f `| Z) /. x1) . t = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x1)) . ((IsoCPNrSP (X,Y)) . t) by A2, H7, FUNCT_1:13;
((f `| Z) /. x0) . t = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z)) /. ((IsoCPNrSP (X,Y)) . x0)) . ((IsoCPNrSP (X,Y)) . t) by A2, H8, FUNCT_1:13;
hence (Gy1y0 * (IsoCPNrSP (X,Y))) . t = Fx1x0 . t by U2, U3, LOPBAN_1:40; :: thesis: verum
end;
then Gy1y0 * (IsoCPNrSP (X,Y)) = Fx1x0 ;
hence ||.(((f `| Z) /. x1) - ((f `| Z) /. x0)).|| < r by H5, LMX00; :: thesis: verum
end;
hence f `| Z is_continuous_on Z by P1, NFCONT_1:19; :: thesis: verum