let X, Y be non trivial RealBanachSpace; ex I being Function of (InvertibleOperators (X,Y)),(InvertibleOperators (Y,X)) st
( I is one-to-one & I is onto & ( 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);
defpred S1[ object , object ] means ex u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( $1 = u & $2 = Inv u );
A1:
for x being object st x in InvertibleOperators (X,Y) holds
ex y being object st
( y in InvertibleOperators (Y,X) & S1[x,y] )
proof
let x be
object ;
( x in InvertibleOperators (X,Y) implies ex y being object st
( y in InvertibleOperators (Y,X) & S1[x,y] ) )
assume
x in InvertibleOperators (
X,
Y)
;
ex y being object st
( y in InvertibleOperators (Y,X) & S1[x,y] )
then consider u being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) such that A2:
(
x = u &
u is
invertible )
;
take y =
Inv u;
( y in InvertibleOperators (Y,X) & S1[x,y] )
y is
invertible
by A2, LM60;
hence
y in InvertibleOperators (
Y,
X)
;
S1[x,y]
thus
S1[
x,
y]
by A2;
verum
end;
consider I being Function of (InvertibleOperators (X,Y)),(InvertibleOperators (Y,X)) such that
A3:
for x being object st x in InvertibleOperators (X,Y) holds
S1[x,I . x]
from FUNCT_2:sch 1(A1);
take
I
; ( I is one-to-one & I is onto & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) )
A4:
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u
A5:
( InvertibleOperators (X,Y) <> {} implies InvertibleOperators (Y,X) <> {} )
B7:
for x1, x2 being object st x1 in InvertibleOperators (X,Y) & x2 in InvertibleOperators (X,Y) & I . x1 = I . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in InvertibleOperators (X,Y) & x2 in InvertibleOperators (X,Y) & I . x1 = I . x2 implies x1 = x2 )
assume that A8:
(
x1 in InvertibleOperators (
X,
Y) &
x2 in InvertibleOperators (
X,
Y) )
and A9:
I . x1 = I . x2
;
x1 = x2
reconsider u1 =
x1,
u2 =
x2 as
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) by A8;
A10:
( ex
v1 being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
(
u1 = v1 &
v1 is
invertible ) & ex
v2 being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,Y)) st
(
u2 = v2 &
v2 is
invertible ) )
by A8;
A11:
I . u1 = Inv u1
by A4, A8;
u1 =
Inv (Inv u1)
by A10, LM60
.=
Inv (Inv u2)
by A4, A8, A9, A11
.=
u2
by A10, LM60
;
hence
x1 = x2
;
verum
end;
now for y being object st y in InvertibleOperators (Y,X) holds
y in rng Ilet y be
object ;
( y in InvertibleOperators (Y,X) implies y in rng I )assume
y in InvertibleOperators (
Y,
X)
;
y in rng Ithen consider v being
Point of
(R_NormSpace_of_BoundedLinearOperators (Y,X)) such that A15:
(
y = v &
v is
invertible )
;
Inv v is
invertible
by A15, LM60;
then A16:
Inv v in InvertibleOperators (
X,
Y)
;
Inv (Inv v) = v
by A15, LM60;
then
y = I . (Inv v)
by A4, A15, A16;
hence
y in rng I
by A5, A16, FUNCT_2:4;
verum end;
then
InvertibleOperators (Y,X) c= rng I
by TARSKI:def 3;
hence
( I is one-to-one & I is onto & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) )
by A4, A5, B7, FUNCT_2:19, XBOOLE_0:def 10; verum