let R be Ring; for X, Y being LeftMod of R
for L being linear-transformation of X,Y st L is bijective holds
ex K being linear-transformation of Y,X st
( K = L " & K is bijective )
let X, Y be LeftMod of R; for L being linear-transformation of X,Y st L is bijective holds
ex K being linear-transformation of Y,X st
( K = L " & K is bijective )
let L be linear-transformation of X,Y; ( L is bijective implies ex K being linear-transformation of Y,X st
( K = L " & K is bijective ) )
assume A1:
L is bijective
; ex K being linear-transformation of Y,X st
( K = L " & K is bijective )
then P2:
rng L = the carrier of Y
by FUNCT_2:def 3;
then reconsider K = L " as Function of Y,X by A1, FUNCT_2:25;
D0:
dom L = the carrier of X
by FUNCT_2:def 1;
B0:
K is additive
proof
let x,
y be
Element of
Y;
VECTSP_1:def 19 K . (x + y) = (K . x) + (K . y)
consider a being
Element of
X such that B01:
x = L . a
by P2, FUNCT_2:113;
consider b being
Element of
X such that B02:
y = L . b
by P2, FUNCT_2:113;
B03:
K . x = a
by A1, FUNCT_1:34, D0, B01;
B04:
K . y = b
by A1, FUNCT_1:34, D0, B02;
x + y = L . (a + b)
by VECTSP_1:def 20, B01, B02;
hence
K . (x + y) = (K . x) + (K . y)
by B03, B04, A1, FUNCT_1:34, D0;
verum
end;
for r being Element of R
for x being Element of Y holds K . (r * x) = r * (K . x)
then reconsider K = K as linear-transformation of Y,X by B0, MOD_2:def 2;
take
K
; ( K = L " & K is bijective )
rng K = the carrier of X
by D0, FUNCT_1:33, A1;
then
K is onto
by FUNCT_2:def 3;
hence
( K = L " & K is bijective )
by A1; verum