let X, Y be 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)) ) )
set S = R_NormSpace_of_BoundedLinearOperators (X,Y);
set K = R_NormSpace_of_BoundedLinearOperators (Y,X);
consider I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) such that
A1:
( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_continuous_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_continuous_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 ) )
by LOPBAN13:25;
consider J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (X,Y)) such that
A2:
( J = I " & J is one-to-one & dom J = InvertibleOperators (Y,X) & rng J = InvertibleOperators (X,Y) & J is_continuous_on InvertibleOperators (Y,X) )
by A1;
take
I
; ( 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)) ) )
A4:
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I is_differentiable_in u
by A1, LM80;
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) st v in InvertibleOperators (Y,X) holds
J . v = Inv v
proof
let v be
Point of
(R_NormSpace_of_BoundedLinearOperators (Y,X));
( v in InvertibleOperators (Y,X) implies J . v = Inv v )
assume
v in InvertibleOperators (
Y,
X)
;
J . v = Inv v
then consider u being
object such that A5:
(
u in dom I &
v = I . u )
by A1, FUNCT_1:def 3;
reconsider u =
u as
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) by A5;
A7:
ex
u0 being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
(
u = u0 &
u0 is
invertible )
by A1, A5;
thus J . v =
u
by A1, A2, A5, FUNCT_1:34
.=
Inv (Inv u)
by A7, LOPBAN13:15
.=
Inv v
by A1, A5
;
verum
end;
then
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) st v in InvertibleOperators (Y,X) holds
J is_differentiable_in v
by A2, LM80;
then
J is_differentiable_on InvertibleOperators (Y,X)
by A2, NDIFF_1:31;
hence
( 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)) ) )
by A1, A2, A4, LM80, NDIFF_1:31; verum