let X, Y be RealLinearSpace; :: thesis: for L being LinearOperator of X,Y st L is isomorphism holds

ex K being LinearOperator of Y,X st

( K = L " & K is isomorphism )

let L be LinearOperator of X,Y; :: thesis: ( L is isomorphism implies ex K being LinearOperator of Y,X st

( K = L " & K is isomorphism ) )

assume A1: L is isomorphism ; :: thesis: ex K being LinearOperator of Y,X st

( K = L " & K is isomorphism )

then A2: ( L is one-to-one & L is onto ) ;

reconsider K = L " as Function of Y,X by A2, FUNCT_2:25;

A3: dom L = the carrier of X by FUNCT_2:def 1;

A4: K is additive

take K ; :: thesis: ( K = L " & K is isomorphism )

K is onto by A1, A3, FUNCT_1:33;

hence ( K = L " & K is isomorphism ) by A1, FUNCT_1:40; :: thesis: verum

ex K being LinearOperator of Y,X st

( K = L " & K is isomorphism )

let L be LinearOperator of X,Y; :: thesis: ( L is isomorphism implies ex K being LinearOperator of Y,X st

( K = L " & K is isomorphism ) )

assume A1: L is isomorphism ; :: thesis: ex K being LinearOperator of Y,X st

( K = L " & K is isomorphism )

then A2: ( L is one-to-one & L is onto ) ;

reconsider K = L " as Function of Y,X by A2, FUNCT_2:25;

A3: dom L = the carrier of X by FUNCT_2:def 1;

A4: K is additive

proof

K is homogeneous
let x, y be Point of Y; :: according to VECTSP_1:def 19 :: thesis: K . (x + y) = (K . x) + (K . y)

consider a being Point of X such that

A5: x = L . a by A2, FUNCT_2:113;

consider b being Point of X such that

A6: y = L . b by A2, FUNCT_2:113;

A7: K . x = a by A1, A3, A5, FUNCT_1:34;

A8: K . y = b by A1, A3, A6, FUNCT_1:34;

x + y = L . (a + b) by A5, A6, VECTSP_1:def 20;

hence K . (x + y) = (K . x) + (K . y) by A1, A3, A7, A8, FUNCT_1:34; :: thesis: verum

end;consider a being Point of X such that

A5: x = L . a by A2, FUNCT_2:113;

consider b being Point of X such that

A6: y = L . b by A2, FUNCT_2:113;

A7: K . x = a by A1, A3, A5, FUNCT_1:34;

A8: K . y = b by A1, A3, A6, FUNCT_1:34;

x + y = L . (a + b) by A5, A6, VECTSP_1:def 20;

hence K . (x + y) = (K . x) + (K . y) by A1, A3, A7, A8, FUNCT_1:34; :: thesis: verum

proof

then reconsider K = K as LinearOperator of Y,X by A4;
let x be Point of Y; :: according to LOPBAN_1:def 5 :: thesis: for b_{1} being object holds K . (b_{1} * x) = b_{1} * (K . x)

let r be Real; :: thesis: K . (r * x) = r * (K . x)

consider a being Point of X such that

A10: x = L . a by A2, FUNCT_2:113;

A11: K . x = a by A1, A3, A10, FUNCT_1:34;

A12: r * x = L . (r * a) by A10, LOPBAN_1:def 5;

thus K . (r * x) = r * (K . x) by A1, A3, A11, A12, FUNCT_1:34; :: thesis: verum

end;let r be Real; :: thesis: K . (r * x) = r * (K . x)

consider a being Point of X such that

A10: x = L . a by A2, FUNCT_2:113;

A11: K . x = a by A1, A3, A10, FUNCT_1:34;

A12: r * x = L . (r * a) by A10, LOPBAN_1:def 5;

thus K . (r * x) = r * (K . x) by A1, A3, A11, A12, FUNCT_1:34; :: thesis: verum

take K ; :: thesis: ( K = L " & K is isomorphism )

K is onto by A1, A3, FUNCT_1:33;

hence ( K = L " & K is isomorphism ) by A1, FUNCT_1:40; :: thesis: verum