let p be prime Element of INT.Ring; :: thesis: for V being free Z_Module

for I being Basis of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

IQ is linearly-independent

let V be free Z_Module; :: thesis: for I being Basis of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

IQ is linearly-independent

let I be Basis of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

IQ is linearly-independent

let IQ be Subset of (Z_MQ_VectSp (V,p)); :: thesis: ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies IQ is linearly-independent )

assume A1: IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: IQ is linearly-independent

assume not IQ is linearly-independent ; :: thesis: contradiction

then consider lq being Linear_Combination of IQ such that

A2: Sum lq = 0. (Z_MQ_VectSp (V,p)) and

A3: Carrier lq <> {} ;

consider Lq being Linear_Combination of Z_MQ_VectSp (V,p) such that

A4: Lq = lq ;

consider l being Linear_Combination of I such that

A5: for v being Vector of V st v in I holds

l . v = Lq . (ZMtoMQV (V,p,v)) by Th24;

set vq0 = Sum Lq;

set v0 = Sum l;

A6: Sum Lq = ZMtoMQV (V,p,(Sum l)) by A1, A5, A4, Th31;

A7: Sum Lq = 0. (VectQuot (V,(p (*) V))) by A2, A4

.= zeroCoset (V,(p (*) V)) by VECTSP10:def 6

.= (0. V) + (p (*) V) by ZMODUL01:59 ;

consider vp being Vector of V such that

A8: ( vp in p (*) V & (Sum l) + vp = 0. V ) by A6, A7, ZMODUL01:75;

reconsider pp = p as Element of INT.Ring ;

vp in { (pp * v) where v is Element of V : verum } by A8;

then consider vv being Element of V such that

A9: vp = pp * vv ;

A10: ( I is linearly-independent & Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by VECTSP_7:def 3;

consider lvv being Linear_Combination of I such that

A11: vv = Sum lvv by A10, STRUCT_0:def 5, ZMODUL02:64;

vp = Sum (p * lvv) by A9, A11, ZMODUL02:53;

then A12: 0. V = Sum (l + (p * lvv)) by A8, ZMODUL02:52;

reconsider pp = p as Element of INT.Ring ;

p * lvv is Linear_Combination of I by ZMODUL02:31;

then l + (pp * lvv) is Linear_Combination of I by ZMODUL02:27;

then consider lpv being Linear_Combination of I such that

A13: lpv = l + (pp * lvv) ;

ex vq being object st vq in Carrier lq by A3, XBOOLE_0:def 1;

then consider uq being Vector of (Z_MQ_VectSp (V,p)) such that

A14: uq in Carrier lq ;

uq in { v where v is Element of (Z_MQ_VectSp (V,p)) : lq . v <> 0. (GF p) } by A14;

then consider uuq being Vector of (Z_MQ_VectSp (V,p)) such that

A15: ( uuq = uq & lq . uuq <> 0. (GF p) ) ;

A16: lq . uuq <> 0 by A15;

Carrier lq c= IQ by VECTSP_6:def 4;

then uq in IQ by A14;

then consider uu being Vector of V such that

A17: ( uq = ZMtoMQV (V,p,uu) & uu in I ) by A1;

A18: lq . uuq = l . uu by A4, A5, A15, A17;

lpv . uu <> 0. INT.Ring

hence contradiction by A12, A13, VECTSP_7:def 3, VECTSP_7:def 1; :: thesis: verum

for I being Basis of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

IQ is linearly-independent

let V be free Z_Module; :: thesis: for I being Basis of V

for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

IQ is linearly-independent

let I be Basis of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds

IQ is linearly-independent

let IQ be Subset of (Z_MQ_VectSp (V,p)); :: thesis: ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies IQ is linearly-independent )

assume A1: IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: IQ is linearly-independent

assume not IQ is linearly-independent ; :: thesis: contradiction

then consider lq being Linear_Combination of IQ such that

A2: Sum lq = 0. (Z_MQ_VectSp (V,p)) and

A3: Carrier lq <> {} ;

consider Lq being Linear_Combination of Z_MQ_VectSp (V,p) such that

A4: Lq = lq ;

consider l being Linear_Combination of I such that

A5: for v being Vector of V st v in I holds

l . v = Lq . (ZMtoMQV (V,p,v)) by Th24;

set vq0 = Sum Lq;

set v0 = Sum l;

A6: Sum Lq = ZMtoMQV (V,p,(Sum l)) by A1, A5, A4, Th31;

A7: Sum Lq = 0. (VectQuot (V,(p (*) V))) by A2, A4

.= zeroCoset (V,(p (*) V)) by VECTSP10:def 6

.= (0. V) + (p (*) V) by ZMODUL01:59 ;

consider vp being Vector of V such that

A8: ( vp in p (*) V & (Sum l) + vp = 0. V ) by A6, A7, ZMODUL01:75;

reconsider pp = p as Element of INT.Ring ;

vp in { (pp * v) where v is Element of V : verum } by A8;

then consider vv being Element of V such that

A9: vp = pp * vv ;

A10: ( I is linearly-independent & Lin I = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) by VECTSP_7:def 3;

consider lvv being Linear_Combination of I such that

A11: vv = Sum lvv by A10, STRUCT_0:def 5, ZMODUL02:64;

vp = Sum (p * lvv) by A9, A11, ZMODUL02:53;

then A12: 0. V = Sum (l + (p * lvv)) by A8, ZMODUL02:52;

reconsider pp = p as Element of INT.Ring ;

p * lvv is Linear_Combination of I by ZMODUL02:31;

then l + (pp * lvv) is Linear_Combination of I by ZMODUL02:27;

then consider lpv being Linear_Combination of I such that

A13: lpv = l + (pp * lvv) ;

ex vq being object st vq in Carrier lq by A3, XBOOLE_0:def 1;

then consider uq being Vector of (Z_MQ_VectSp (V,p)) such that

A14: uq in Carrier lq ;

uq in { v where v is Element of (Z_MQ_VectSp (V,p)) : lq . v <> 0. (GF p) } by A14;

then consider uuq being Vector of (Z_MQ_VectSp (V,p)) such that

A15: ( uuq = uq & lq . uuq <> 0. (GF p) ) ;

A16: lq . uuq <> 0 by A15;

Carrier lq c= IQ by VECTSP_6:def 4;

then uq in IQ by A14;

then consider uu being Vector of V such that

A17: ( uq = ZMtoMQV (V,p,uu) & uu in I ) by A1;

A18: lq . uuq = l . uu by A4, A5, A15, A17;

lpv . uu <> 0. INT.Ring

proof

then
uu in Carrier lpv
;
assume A19:
lpv . uu = 0. INT.Ring
; :: thesis: contradiction

(l + (pp * lvv)) . uu = (l . uu) + ((pp * lvv) . uu) by VECTSP_6:22

.= (l . uu) + (pp * (lvv . uu)) by VECTSP_6:def 9 ;

then 0. INT.Ring = (l . uu) + (pp * (lvv . uu)) by A13, A19;

then l . uu = - (pp * (lvv . uu)) ;

then l . uu = pp * (- (lvv . uu)) ;

then pp divides l . uu by INT_1:def 3;

then A20: (l . uu) mod p = 0 by INT_1:62;

thus contradiction by A16, A18, A20, NAT_1:44, NAT_D:63; :: thesis: verum

end;(l + (pp * lvv)) . uu = (l . uu) + ((pp * lvv) . uu) by VECTSP_6:22

.= (l . uu) + (pp * (lvv . uu)) by VECTSP_6:def 9 ;

then 0. INT.Ring = (l . uu) + (pp * (lvv . uu)) by A13, A19;

then l . uu = - (pp * (lvv . uu)) ;

then l . uu = pp * (- (lvv . uu)) ;

then pp divides l . uu by INT_1:def 3;

then A20: (l . uu) mod p = 0 by INT_1:62;

thus contradiction by A16, A18, A20, NAT_1:44, NAT_D:63; :: thesis: verum

hence contradiction by A12, A13, VECTSP_7:def 3, VECTSP_7:def 1; :: thesis: verum