let R be Ring; :: thesis: for X, Y being LeftMod of R

for A being Subset of X

for L being linear-transformation of X,Y st L is bijective holds

( A is linearly-independent iff L .: A is linearly-independent )

let X, Y be LeftMod of R; :: thesis: for A being Subset of X

for L being linear-transformation of X,Y st L is bijective holds

( A is linearly-independent iff L .: A is linearly-independent )

let A be Subset of X; :: thesis: for L being linear-transformation of X,Y st L is bijective holds

( A is linearly-independent iff L .: A is linearly-independent )

let L be linear-transformation of X,Y; :: thesis: ( L is bijective implies ( A is linearly-independent iff L .: A is linearly-independent ) )

assume AS1: L is bijective ; :: thesis: ( A is linearly-independent iff L .: A is linearly-independent )

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

consider K being linear-transformation of Y,X such that

AS3: ( K = L " & K is bijective ) by HM1, AS1;

thus ( A is linearly-independent implies L .: A is linearly-independent ) by AS1, HM4; :: thesis: ( L .: A is linearly-independent implies A is linearly-independent )

assume L .: A is linearly-independent ; :: thesis: A is linearly-independent

then K .: (L .: A) is linearly-independent by AS3, HM4;

hence A is linearly-independent by D1, AS1, AS3, FUNCT_1:107; :: thesis: verum

for A being Subset of X

for L being linear-transformation of X,Y st L is bijective holds

( A is linearly-independent iff L .: A is linearly-independent )

let X, Y be LeftMod of R; :: thesis: for A being Subset of X

for L being linear-transformation of X,Y st L is bijective holds

( A is linearly-independent iff L .: A is linearly-independent )

let A be Subset of X; :: thesis: for L being linear-transformation of X,Y st L is bijective holds

( A is linearly-independent iff L .: A is linearly-independent )

let L be linear-transformation of X,Y; :: thesis: ( L is bijective implies ( A is linearly-independent iff L .: A is linearly-independent ) )

assume AS1: L is bijective ; :: thesis: ( A is linearly-independent iff L .: A is linearly-independent )

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

consider K being linear-transformation of Y,X such that

AS3: ( K = L " & K is bijective ) by HM1, AS1;

thus ( A is linearly-independent implies L .: A is linearly-independent ) by AS1, HM4; :: thesis: ( L .: A is linearly-independent implies A is linearly-independent )

assume L .: A is linearly-independent ; :: thesis: A is linearly-independent

then K .: (L .: A) is linearly-independent by AS3, HM4;

hence A is linearly-independent by D1, AS1, AS3, FUNCT_1:107; :: thesis: verum