let X be non trivial RealBanachSpace; for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))
for w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st v = w holds
( ( v is invertible implies w is invertible ) & ( w is invertible implies v is invertible ) & ( w is invertible implies v " = w " ) )
let v be Point of (R_NormSpace_of_BoundedLinearOperators (X,X)); for w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st v = w holds
( ( v is invertible implies w is invertible ) & ( w is invertible implies v is invertible ) & ( w is invertible implies v " = w " ) )
let w be Point of (R_Normed_Algebra_of_BoundedLinearOperators X); ( v = w implies ( ( v is invertible implies w is invertible ) & ( w is invertible implies v is invertible ) & ( w is invertible implies v " = w " ) ) )
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
assume A1:
v = w
; ( ( v is invertible implies w is invertible ) & ( w is invertible implies v is invertible ) & ( w is invertible implies v " = w " ) )
A2:
v is Lipschitzian LinearOperator of X,X
by LOPBAN_1:def 9;
A4:
( v is invertible implies w is invertible )
proof
assume A5:
v is
invertible
;
w is invertible
then reconsider x =
v " as
Point of
(R_Normed_Algebra_of_BoundedLinearOperators X) ;
A7:
v " is
Lipschitzian LinearOperator of
X,
X
by A5, LOPBAN_1:def 9;
reconsider zx =
x,
zv =
v as
Element of
BoundedLinearOperators (
X,
X) ;
(
dom v = the
carrier of
X &
rng v = the
carrier of
X )
by A2, A5, FUNCT_2:def 1;
then A9:
(
(v ") * v = id X &
v * (v ") = id X )
by A5, FUNCT_1:39;
A10:
(
v " = modetrans (
(v "),
X,
X) &
v = modetrans (
v,
X,
X) )
by A2, A7, LOPBAN_1:29;
then A11:
(v ") * v =
zx * zv
.=
x * w
by A1, LOPBAN_2:def 4
;
v * (v ") =
zv * zx
by A10
.=
w * x
by A1, LOPBAN_2:def 4
;
hence
w is
invertible
by A9, A11;
verum
end;
( w is invertible implies ( v is invertible & v " = w " ) )
proof
assume A13:
w is
invertible
;
( v is invertible & v " = w " )
A14:
v is
Lipschitzian LinearOperator of
X,
X
by LOPBAN_1:def 9;
reconsider y =
w " as
Lipschitzian LinearOperator of
X,
X by LOPBAN_1:def 9;
reconsider zy =
y,
zw =
w as
Element of
BoundedLinearOperators (
X,
X) ;
A15:
(
y = modetrans (
y,
X,
X) &
v = modetrans (
v,
X,
X) )
by A14, LOPBAN_1:29;
then A16:
y * v =
zy * zw
by A1
.=
(w ") * w
by LOPBAN_2:def 4
.=
id X
by A13, LOPBAN_3:def 8
;
A17:
v * y =
zw * zy
by A1, A15
.=
w * (w ")
by LOPBAN_2:def 4
.=
id X
by A13, LOPBAN_3:def 8
;
reconsider y0 =
y,
v0 =
v as
Function of the
carrier of
X, the
carrier of
X by LOPBAN_1:def 9;
A18:
dom v = the
carrier of
X
by A14, FUNCT_2:def 1;
A19:
(
v0 is
one-to-one &
v0 is
onto )
by A16, A17, FUNCT_2:23;
then
dom y = rng v
by FUNCT_2:def 1;
hence
(
v is
invertible &
v " = w " )
by A16, A18, A19, FUNCT_1:41;
verum
end;
hence
( ( v is invertible implies w is invertible ) & ( w is invertible implies v is invertible ) & ( w is invertible implies v " = w " ) )
by A4; verum