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

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