let S, T be RealLinearSpace; for I being LinearOperator of S,T st I is bijective holds
ex J being LinearOperator of T,S st
( J = I " & J is bijective )
let I be LinearOperator of S,T; ( I is bijective implies ex J being LinearOperator of T,S st
( J = I " & J is bijective ) )
assume A1:
I is bijective
; ex J being LinearOperator of T,S st
( J = I " & J is bijective )
then a1:
( I is one-to-one & I is onto )
;
then A2:
( rng I = the carrier of T & dom I = the carrier of S )
by FUNCT_2:def 1;
A3:
( rng I = dom (I ") & dom I = rng (I ") )
by A1, FUNCT_1:33;
then reconsider J = I " as Function of T,S by A2, FUNCT_2:1;
A4:
for v, w being Point of T holds J . (v + w) = (J . v) + (J . w)
proof
let v,
w be
Point of
T;
J . (v + w) = (J . v) + (J . w)
consider t being
Point of
S such that A5:
v = I . t
by FUNCT_2:113, a1;
consider s being
Point of
S such that A6:
w = I . s
by FUNCT_2:113, a1;
A7:
J . (v + w) =
J . (I . (t + s))
by A5, A6, VECTSP_1:def 20
.=
t + s
by A1, A2, FUNCT_1:34
;
J . w = s
by A1, A2, A6, FUNCT_1:34;
hence
J . (v + w) = (J . v) + (J . w)
by A1, A2, A5, A7, FUNCT_1:34;
verum
end;
for v being Point of T
for r being Real holds J . (r * v) = r * (J . v)
then reconsider J = J as LinearOperator of T,S by A4, LOPBAN_1:def 5, VECTSP_1:def 20;
take
J
; ( J = I " & J is bijective )
thus
J = I "
; J is bijective
( J is one-to-one & J is onto )
by A1, A3, FUNCT_2:def 1;
hence
J is bijective
; verum