let V be Z_Module; :: thesis: for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & I is linearly-independent holds
IQ is linearly-independent
let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & I is linearly-independent holds
IQ is linearly-independent
let IQ be Subset of (Z_MQ_VectSp V); :: thesis: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & I is linearly-independent implies IQ is linearly-independent )
assume AS: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & I is linearly-independent ) ; :: thesis: IQ is linearly-independent
assume not IQ is linearly-independent ; :: thesis: contradiction
then consider lq being Linear_Combination of IQ such that
P1: ( Sum lq = 0. (Z_MQ_VectSp V) & Carrier lq <> {} ) by VECTSP_7:def 1;
consider m being Element of INT.Ring, a being Element of F_Rat, l being Linear_Combination of I such that
P2: ( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l ) by ThEQRZMV3, AS;
a * (Sum lq) = 0. (Z_MQ_VectSp V) by P1, VECTSP_1:15;
then X2: (MorphsZQ V) . (Sum l) = 0. (Z_MQ_VectSp V) by AS, P2, ThEQRZMV3B;
X3: (MorphsZQ V) . (0. V) = 0. (Z_MQ_VectSp V) by AS, defMorph;
MorphsZQ V is one-to-one by AS, defMorph;
then P3: Sum l = 0. V by X2, X3, FUNCT_2:19;
H6: Carrier lq c= IQ by VECTSP_6:def 4;
IQ c= rng (MorphsZQ V) by AS, RELAT_1:111;
then H2: Carrier lq = (MorphsZQ V) .: (Carrier l) by H6, P2, FUNCT_1:77, XBOOLE_1:1;
Carrier l <> {} by H2, P1;
hence contradiction by AS, P3, VECTSP_7:def 1; :: thesis: verum