:: Implicit Function Theorem -- Part {II}
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

theorem LMDIFF: :: NDIFF_9:1

for E, F being RealNormSpace
for f being PartFunc of E,F
for Z being Subset of E
for z being Point of E st Z is open & z in Z & Z c= dom f & f is_differentiable_in z holds
( f | Z is_differentiable_in z & diff (f,z) = diff ((f | Z),z) )

proof end;

theorem LMPDIFF: :: NDIFF_9:2

for E, F, G being RealNormSpace
for f being PartFunc of [:E,F:],G
for Z being Subset of [:E,F:]
for z being Point of [:E,F:] st Z is open & z in Z & Z c= dom f holds
( ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) & ( f is_partial_differentiable_in`2 z implies ( f | Z is_partial_differentiable_in`2 z & partdiff`2 (f,z) = partdiff`2 ((f | Z),z) ) ) )

proof end;

theorem LmTh47: :: NDIFF_9:3

for X, E, G, F being RealNormSpace
for BL being BilinearOperator of E,F,G
for f being PartFunc of X,E
for g being PartFunc of X,F
for S being Subset of X st BL is_continuous_on the carrier of [:E,F:] & S c= dom f & S c= dom g & ( for s being Point of X st s in S holds
f is_continuous_in s ) & ( for s being Point of X st s in S holds
g is_continuous_in s ) holds
ex H being PartFunc of X,G st
( dom H = S & ( for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )

proof end;

theorem LmTh471: :: NDIFF_9:4

for E, F being RealNormSpace
for g being PartFunc of E,F
for A being Subset of E st g is_continuous_on A & dom g = A holds
ex xg being PartFunc of E,[:E,F:] st
( dom xg = A & ( for x being Point of E st x in A holds
xg . x = [x,(g . x)] ) & xg is_continuous_on A )

proof end;

theorem NFCONT112: :: NDIFF_9:5

for S, T, V being RealNormSpace
for x0 being Point of V
for f1 being PartFunc of the carrier of V, the carrier of S
for f2 being PartFunc of the carrier of S, the carrier of T st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0

proof end;

theorem LM0: :: NDIFF_9:6

for E, F being RealNormSpace
for z being Point of [:E,F:]
for x being Point of E
for y being Point of F st z = [x,y] holds
||.z.|| <= ||.x.|| + ||.y.||

proof end;

theorem Th0: :: NDIFF_9:7

for E, F, G being RealNormSpace
for L being LinearOperator of [:E,F:],G ex L1 being LinearOperator of E,G ex L2 being LinearOperator of F,G st
( ( for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

proof end;

theorem Th0X: :: NDIFF_9:8

for E, F, G being RealNormSpace
for L being LinearOperator of [:E,F:],G
for L11 being LinearOperator of E,G
for L12 being LinearOperator of F,G
for L21 being LinearOperator of E,G
for L22 being LinearOperator of F,G st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ) holds
( L11 = L21 & L12 = L22 )

proof end;

theorem Th1: :: NDIFF_9:9

for E, F, G being RealNormSpace
for L1 being LinearOperator of E,G
for L2 being LinearOperator of F,G ex L being LinearOperator of [:E,F:],G st
( ( for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

proof end;

theorem Th2: :: NDIFF_9:10

for E, F, G being RealNormSpace
for L being Lipschitzian LinearOperator of [:E,F:],G ex L1 being Lipschitzian LinearOperator of E,G ex L2 being Lipschitzian LinearOperator of F,G st
( ( for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

proof end;

theorem :: NDIFF_9:11

for E, F, G being RealNormSpace
for L1 being Lipschitzian LinearOperator of E,G
for L2 being Lipschitzian LinearOperator of F,G ex L being Lipschitzian LinearOperator of [:E,F:],G st
( ( for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L /. [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L /. [(0. E),y] ) )

proof end;

theorem :: NDIFF_9:12

for E, F, G being RealNormSpace
for L being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) ex L1 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) ex L2 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st
( ( for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L . [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L . [(0. E),y] ) & ||.L.|| <= ||.L1.|| + ||.L2.|| & ||.L1.|| <= ||.L.|| & ||.L2.|| <= ||.L.|| )

proof end;

theorem :: NDIFF_9:13

for E, F, G being RealNormSpace
for L being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G))
for L11, L12 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G))
for L21, L22 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L21 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L12 . x) + (L22 . y) ) holds
( L11 = L12 & L21 = L22 )

proof end;

theorem Th4: :: NDIFF_9:14

for E, G, F being RealNormSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for z being Point of [:E,F:] st f is_differentiable_in z holds
( f is_partial_differentiable_in`1 z & f is_partial_differentiable_in`2 z & ( for dx being Point of E
for dy being Point of F holds (diff (f,z)) . [dx,dy] = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy) ) )

proof end;

theorem Th5: :: NDIFF_9:15

for E, G, F being RealNormSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for r1, r2 being Real
for g being PartFunc of E,F
for P being Lipschitzian LinearOperator of E,G
for Q being Lipschitzian LinearOperator of G,F st Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < r1 & 0 < r2 & dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g . a = b & g is_continuous_in a & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) holds
( g is_differentiable_in a & diff (g,a) = - (Q * P) )

proof end;

theorem LMTh3: :: NDIFF_9:16

for X, Y being non trivial RealBanachSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
ex K, s being Real st
( 0 <= K & 0 < s & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds
( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= K * (||.du.|| * ||.du.||) ) ) )

proof end;

theorem LM80: :: NDIFF_9:17

for X, Y being non trivial RealBanachSpace
for I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st dom I = InvertibleOperators (X,Y) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) holds
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
( I is_differentiable_in u & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )

proof end;

theorem :: NDIFF_9:18

for X, Y being non trivial RealBanachSpace ex I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st
( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_differentiable_on InvertibleOperators (X,Y) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_differentiable_on InvertibleOperators (Y,X) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) & ( for u, du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
(diff (I,u)) . du = - (((Inv u) * du) * (Inv u)) ) )

proof end;

theorem Th45: :: NDIFF_9:19

for E, G, F being RealNormSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )

proof end;

theorem Th47: :: NDIFF_9:20

for E being RealNormSpace
for G, F being non trivial RealBanachSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for c being Point of G
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) holds
( g is_differentiable_on A & g `| A is_continuous_on A & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )

proof end;

theorem :: NDIFF_9:21

for E being RealNormSpace
for G, F being non trivial RealBanachSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`2 (f,z) is invertible holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being Point of F st y1 in Ball (b,r2) & y2 in Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of E,F st
( dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g is_continuous_on Ball (a,r1) & g . a = b & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & g is_differentiable_on Ball (a,r1) & g `| (Ball (a,r1)) is_continuous_on Ball (a,r1) & ( for x being Point of E
for z being Point of [:E,F:] st x in Ball (a,r1) & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) & ( for x being Point of E
for z being Point of [:E,F:] st x in Ball (a,r1) & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= Ball (b,r2) & ( for x being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )

proof end;