let V be Z_Module; :: thesis: for v being Vector of V holds
( not v is torsion iff {v} is linearly-independent )
let v be Vector of V; :: thesis: ( not v is torsion iff {v} is linearly-independent )
A1: ( not v is torsion implies {v} is linearly-independent )
proof
assume B1: not v is torsion ; :: thesis: {v} is linearly-independent
let l be Linear_Combination of {v}; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume B4: Sum l = 0. V ; :: thesis: Carrier l = {}
now :: thesis: Carrier l = {}
end;
hence Carrier l = {} ; :: thesis: verum
end;
( {v} is linearly-independent implies not v is torsion )
proof
assume B1: {v} is linearly-independent ; :: thesis: not v is torsion
assume v is torsion ; :: thesis: contradiction
then consider i being Element of INT.Ring such that
C2: ( i <> 0 & i * v = 0. V ) ;
consider l being Linear_Combination of V such that
C3: ( l . v = 1 & ( for u being Vector of V st v <> u holds
l . u = 0. INT.Ring ) ) by ZMODUL03:1;
for u being Vector of V st u <> v holds
not u in Carrier l
proof
let u be Vector of V; :: thesis: ( u <> v implies not u in Carrier l )
assume u <> v ; :: thesis: not u in Carrier l
then l . u = 0 by C3;
hence not u in Carrier l by ZMODUL02:8; :: thesis: verum
end;
then for u being object holds
( u = v iff u in Carrier l ) by C3;
then C5: Carrier l = {v} by TARSKI:def 1;
then C6: Carrier (i * l) = {v} by C2, ZMODUL02:29;
C7: Carrier (i * l) <> {} by C2, C5, ZMODUL02:29;
reconsider li = i * l as Linear_Combination of {v} by C6, VECTSP_6:def 4;
Sum (i * l) = i * (Sum l) by ZMODUL02:53
.= i * ((1. INT.Ring) * v) by C3, C5, ZMODUL02:24
.= 0. V by C2, VECTSP_1:def 17 ;
then Sum li = 0. V ;
hence contradiction by B1, C7; :: thesis: verum
end;
hence ( not v is torsion iff {v} is linearly-independent ) by A1; :: thesis: verum