let X, Y be non trivial RealBanachSpace; :: thesis: 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_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 ) )
set S = R_NormSpace_of_BoundedLinearOperators (X,Y);
set K = R_NormSpace_of_BoundedLinearOperators (Y,X);
consider J being Function of (InvertibleOperators (X,Y)),(InvertibleOperators (Y,X)) such that
A1: ( J is one-to-one & J is onto & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
J . u = Inv u ) ) by LM70;
A2: ( InvertibleOperators (X,Y) <> {} implies InvertibleOperators (Y,X) <> {} )
proof
assume InvertibleOperators (X,Y) <> {} ; :: thesis: InvertibleOperators (Y,X) <> {}
then consider x being object such that
A3: x in InvertibleOperators (X,Y) by XBOOLE_0:def 1;
consider u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) such that
A4: ( x = u & u is invertible ) by A3;
Inv u is invertible by A4, LM60;
then Inv u in InvertibleOperators (Y,X) ;
hence InvertibleOperators (Y,X) <> {} ; :: thesis: verum
end;
then dom J = InvertibleOperators (X,Y) by FUNCT_2:def 1;
then J in PFuncs ( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)), the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X))) by A1, PARTFUN1:def 3;
then reconsider I = J as PartFunc of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)), the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)) by PARTFUN1:46;
take I ; :: thesis: ( 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 ) )
thus A9: dom I = InvertibleOperators (X,Y) by A2, FUNCT_2:def 1; :: thesis: ( 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 ) )
thus rng I = InvertibleOperators (Y,X) by A1; :: thesis: ( 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 ) )
thus I is one-to-one by A1; :: thesis: ( 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 ) )
reconsider L = J " as Function of (InvertibleOperators (Y,X)),(InvertibleOperators (X,Y)) by A1, FUNCT_2:25;
A14: dom (J ") = InvertibleOperators (Y,X) by A1, FUNCT_1:33;
A16: rng (J ") = dom J by A1, FUNCT_1:33
.= InvertibleOperators (X,Y) by A2, FUNCT_2:def 1 ;
then L in PFuncs ( the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)), the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) by A14, PARTFUN1:def 3;
then reconsider L = L as PartFunc of the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,X)), the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by PARTFUN1:46;
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) st v in InvertibleOperators (Y,X) holds
L . v = Inv v
proof
let v be Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)); :: thesis: ( v in InvertibleOperators (Y,X) implies L . v = Inv v )
assume v in InvertibleOperators (Y,X) ; :: thesis: L . v = Inv v
then consider u being object such that
A23: ( u in InvertibleOperators (X,Y) & J . u = v ) by A1, FUNCT_2:11;
reconsider u = u as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by A23;
A24: ex u0 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( u = u0 & u0 is invertible ) by A23;
Inv v = Inv (Inv u) by A1, A23
.= u by A24, LM60 ;
hence L . v = Inv v by A1, A2, A23, FUNCT_2:26; :: thesis: verum
end;
hence ( 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 A1, A9, A14, A16, LM80; :: thesis: verum