let X, Y, Z be RealNormSpace; :: thesis: for V being Subset of Y
for g being PartFunc of Y,Z
for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
let V be Subset of Y; :: thesis: for g being PartFunc of Y,Z
for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
let g be PartFunc of Y,Z; :: thesis: for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
let I be LinearOperator of X,Y; :: thesis: ( I is one-to-one & I is onto & I is isometric & g is_differentiable_on V implies ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V ) )
assume that
A1: ( I is one-to-one & I is onto & I is isometric ) and
A2: g is_differentiable_on V ; :: thesis: ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
consider J being LinearOperator of Y,X such that
A3: ( J = I " & J is one-to-one & J is onto & J is isometric ) by A1, NDIFF_7:9;
set f = g * I;
set U = I " V;
A4: dom J = the carrier of Y by FUNCT_2:def 1;
A5: g * I is_differentiable_on I " V by A1, A2, NDIFF_7:29;
A6: dom ((g * I) `| (I " V)) = I " V by A5, NDIFF_1:def 9;
A7: dom (g `| V) = V by A2, NDIFF_1:def 9;
set F = (g * I) `| (I " V);
set G = g `| V;
A8: ( g `| V is_continuous_on V implies (g * I) `| (I " V) is_continuous_on I " V )
proof
assume A10: g `| V is_continuous_on V ; :: thesis: (g * I) `| (I " V) is_continuous_on I " V
for x0 being Point of X
for e being Real st x0 in I " V & 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )
proof
let x0 be Point of X; :: thesis: for e being Real st x0 in I " V & 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )
let e be Real; :: thesis: ( x0 in I " V & 0 < e implies ex d being Real st
( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) ) )
assume A11: ( x0 in I " V & 0 < e ) ; :: thesis: ex d being Real st
( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )
consider y0 being Point of Y such that
A12: x0 = J . y0 by A3, FUNCT_2:113;
A13: I . x0 = y0 by A1, A3, A12, FUNCT_1:35;
then A14: y0 in V by A11, FUNCT_2:38;
then consider d being Real such that
A15: ( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) ) by A10, A11, NFCONT_1:19;
take d ; :: thesis: ( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )
thus 0 < d by A15; :: thesis: for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e
thus for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e :: thesis: verum
proof
let x1 be Point of X; :: thesis: ( x1 in I " V & ||.(x1 - x0).|| < d implies ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e )
assume A16: ( x1 in I " V & ||.(x1 - x0).|| < d ) ; :: thesis: ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e
consider y1 being Point of Y such that
A17: x1 = J . y1 by A3, FUNCT_2:113;
A18: I . x1 = y1 by A1, A3, A17, FUNCT_1:35;
then A19: y1 in V by A16, FUNCT_2:38;
||.(y1 - y0).|| = ||.(x1 - x0).|| by A1, A13, A18;
then A20: ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e by A15, A16, A19;
A21: (g `| V) /. y1 = (g `| V) . y1 by A7, A19, PARTFUN1:def 6
.= (((g * I) `| (I " V)) /. x1) * J by A1, A2, A3, A17, A19, Th9 ;
A22: (g `| V) /. y0 = (g `| V) . y0 by A7, A14, PARTFUN1:def 6
.= (((g * I) `| (I " V)) /. x0) * J by A1, A2, A3, A12, A14, Th9 ;
reconsider dF = (((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0) as Lipschitzian LinearOperator of X,Z by LOPBAN_1:def 9;
reconsider dG = ((g `| V) /. y1) - ((g `| V) /. y0) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
now :: thesis: for v being VECTOR of Y holds (dF * J) . v = dG . v
let v be VECTOR of Y; :: thesis: (dF * J) . v = dG . v
A23: (((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)) * J) . v = ((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)) . (J . v) by A4, FUNCT_1:13
.= ((((g * I) `| (I " V)) /. x1) . (J . v)) - ((((g * I) `| (I " V)) /. x0) . (J . v)) by LOPBAN_1:40 ;
A24: ((g `| V) /. y1) . v = (((g * I) `| (I " V)) /. x1) . (J . v) by A4, A21, FUNCT_1:13;
((g `| V) /. y0) . v = (((g * I) `| (I " V)) /. x0) . (J . v) by A4, A22, FUNCT_1:13;
hence (dF * J) . v = dG . v by A23, A24, LOPBAN_1:40; :: thesis: verum
end;
then dF * J = dG ;
hence ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e by A3, A20, NDIFF_7:22; :: thesis: verum
end;
end;
hence (g * I) `| (I " V) is_continuous_on I " V by A6, NFCONT_1:19; :: thesis: verum
end;
( (g * I) `| (I " V) is_continuous_on I " V implies g `| V is_continuous_on V )
proof
assume A25: (g * I) `| (I " V) is_continuous_on I " V ; :: thesis: g `| V is_continuous_on V
for y0 being Point of Y
for e being Real st y0 in V & 0 < e holds
ex d being Real st
( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )
proof
let y0 be Point of Y; :: thesis: for e being Real st y0 in V & 0 < e holds
ex d being Real st
( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )
let e be Real; :: thesis: ( y0 in V & 0 < e implies ex d being Real st
( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) ) )
assume A26: ( y0 in V & 0 < e ) ; :: thesis: ex d being Real st
( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )
set x0 = J . y0;
I . (J . y0) = y0 by A1, A3, FUNCT_1:35;
then J . y0 in I " V by A26, FUNCT_2:38;
then consider d being Real such that
A27: ( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - (J . y0)).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. (J . y0))).|| < e ) ) by A25, A26, NFCONT_1:19;
take d ; :: thesis: ( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )
thus 0 < d by A27; :: thesis: for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e
let y1 be Point of Y; :: thesis: ( y1 in V & ||.(y1 - y0).|| < d implies ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e )
assume A28: ( y1 in V & ||.(y1 - y0).|| < d ) ; :: thesis: ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e
set x1 = J . y1;
I . (J . y1) = y1 by A1, A3, FUNCT_1:35;
then A29: J . y1 in I " V by A28, FUNCT_2:38;
||.((J . y1) - (J . y0)).|| = ||.(y1 - y0).|| by A3;
then A30: ||.((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))).|| < e by A27, A28, A29;
A31: (g `| V) /. y1 = (g `| V) . y1 by A7, A28, PARTFUN1:def 6
.= (((g * I) `| (I " V)) /. (J . y1)) * J by A1, A2, A3, A28, Th9 ;
A32: (g `| V) /. y0 = (g `| V) . y0 by A7, A26, PARTFUN1:def 6
.= (((g * I) `| (I " V)) /. (J . y0)) * J by A1, A2, A3, A26, Th9 ;
reconsider dF = (((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0)) as Lipschitzian LinearOperator of X,Z by LOPBAN_1:def 9;
reconsider dG = ((g `| V) /. y1) - ((g `| V) /. y0) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
now :: thesis: for v being VECTOR of Y holds (dF * J) . v = dG . v
let v be VECTOR of Y; :: thesis: (dF * J) . v = dG . v
A33: (((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))) * J) . v = ((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))) . (J . v) by A4, FUNCT_1:13
.= ((((g * I) `| (I " V)) /. (J . y1)) . (J . v)) - ((((g * I) `| (I " V)) /. (J . y0)) . (J . v)) by LOPBAN_1:40 ;
A34: ((g `| V) /. y1) . v = (((g * I) `| (I " V)) /. (J . y1)) . (J . v) by A4, A31, FUNCT_1:13;
((g `| V) /. y0) . v = (((g * I) `| (I " V)) /. (J . y0)) . (J . v) by A4, A32, FUNCT_1:13;
hence (dF * J) . v = dG . v by A33, A34, LOPBAN_1:40; :: thesis: verum
end;
then dF * J = dG ;
hence ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e by A3, A30, NDIFF_7:22; :: thesis: verum
end;
hence g `| V is_continuous_on V by A7, NFCONT_1:19; :: thesis: verum
end;
hence ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V ) by A8; :: thesis: verum