let R be Ring; 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 & A is linearly-independent holds
L .: A is linearly-independent
let X, Y be LeftMod of R; for A being Subset of X
for L being linear-transformation of X,Y st L is bijective & A is linearly-independent holds
L .: A is linearly-independent
let A be Subset of X; for L being linear-transformation of X,Y st L is bijective & A is linearly-independent holds
L .: A is linearly-independent
let L be linear-transformation of X,Y; ( L is bijective & A is linearly-independent implies L .: A is linearly-independent )
assume that
AS1:
L is bijective
and
AS2:
A is linearly-independent
; L .: A is linearly-independent
consider K being linear-transformation of Y,X such that
AS3:
( K = L " & K is bijective )
by HM1, AS1;
D1:
dom L = the carrier of X
by FUNCT_2:def 1;
R1:
rng L = the carrier of Y
by FUNCT_2:def 3, AS1;
for l being Linear_Combination of L .: A st Sum l = 0. Y holds
Carrier l = {}
proof
let l be
Linear_Combination of
L .: A;
( Sum l = 0. Y implies Carrier l = {} )
assume P0:
Sum l = 0. Y
;
Carrier l = {}
reconsider m =
K @* l as
Linear_Combination of
K .: (Carrier l) by ZMODUL05:44;
P2:
Sum m =
K . (0. Y)
by P0, ZMODUL05:46
.=
0. X
by HM0
;
K .: (Carrier l) c= K .: (L .: A)
by RELAT_1:123, VECTSP_6:def 4;
then P4:
K .: (Carrier l) c= A
by D1, AS1, AS3, FUNCT_1:107;
K | (Carrier l) is
one-to-one
by AS3, FUNCT_1:52;
then P5:
K .: (Carrier l) = Carrier (K @* l)
by ZMODUL05:56;
then
m is
Linear_Combination of
A
by VECTSP_6:def 4, P4;
then P6:
L .: (K .: (Carrier l)) =
L .: {}
by P5, AS2, P2
.=
{}
;
L .: (K .: (Carrier l)) =
L .: (L " (Carrier l))
by FUNCT_1:85, AS1, AS3
.=
Carrier l
by R1, FUNCT_1:77
;
hence
Carrier l = {}
by P6;
verum
end;
hence
L .: A is linearly-independent
; verum