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

proof

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;

then uu in Carrier lpv ;
hence contradiction by A12, A13, VECTSP_7:def 3, VECTSP_7:def 1; :: thesis: verum