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