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))

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

ZMtoMQV (V,p,(Sum l)) in Lin IQ

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

for IQ being Subset of (Z_MQ_VectSp (V,p))

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

ZMtoMQV (V,p,(Sum l)) in Lin IQ

let I be Basis of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp (V,p))

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

ZMtoMQV (V,p,(Sum l)) in Lin IQ

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

ZMtoMQV (V,p,(Sum l)) in Lin IQ

let l be Linear_Combination of I; :: thesis: ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies ZMtoMQV (V,p,(Sum l)) in Lin IQ )

assume A1: IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: ZMtoMQV (V,p,(Sum l)) in Lin IQ

consider G being FinSequence of V such that

A2: ( G is one-to-one & rng G = Carrier l & Sum l = Sum (l (#) G) ) by VECTSP_6:def 6;

for I being Basis of V

for IQ being Subset of (Z_MQ_VectSp (V,p))

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

ZMtoMQV (V,p,(Sum l)) in Lin IQ

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

for IQ being Subset of (Z_MQ_VectSp (V,p))

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

ZMtoMQV (V,p,(Sum l)) in Lin IQ

let I be Basis of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp (V,p))

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

ZMtoMQV (V,p,(Sum l)) in Lin IQ

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

ZMtoMQV (V,p,(Sum l)) in Lin IQ

let l be Linear_Combination of I; :: thesis: ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies ZMtoMQV (V,p,(Sum l)) in Lin IQ )

assume A1: IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: ZMtoMQV (V,p,(Sum l)) in Lin IQ

consider G being FinSequence of V such that

A2: ( G is one-to-one & rng G = Carrier l & Sum l = Sum (l (#) G) ) by VECTSP_6:def 6;

now :: thesis: for i being Element of NAT st i in dom (l (#) G) holds

ex si being Vector of V st

( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ )

hence
ZMtoMQV (V,p,(Sum l)) in Lin IQ
by A1, A2, Th33; :: thesis: verumex si being Vector of V st

( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ )

let i be Element of NAT ; :: thesis: ( i in dom (l (#) G) implies ex si being Vector of V st

( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ ) )

assume i in dom (l (#) G) ; :: thesis: ex si being Vector of V st

( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ )

then i in Seg (len (l (#) G)) by FINSEQ_1:def 3;

then i in Seg (len G) by VECTSP_6:def 5;

then A3: i in dom G by FINSEQ_1:def 3;

then G . i in rng G by FUNCT_1:3;

then reconsider v = G . i as Element of V ;

A4: (l (#) G) . i = (l . v) * v by A3, ZMODUL02:13;

reconsider b = (l . v) mod p as Element of (GF p) by Lm3;

reconsider a = (l . v) mod p as Element of INT.Ring ;

reconsider k = l . v as Element of INT.Ring ;

reconsider t = ZMtoMQV (V,p,v) as Element of (Z_MQ_VectSp (V,p)) ;

A5: b * t = ZMtoMQV (V,p,(a * v)) by Th30

.= ZMtoMQV (V,p,(k * v)) by Lm4 ;

A6: v in Carrier l by A3, A2, FUNCT_1:3;

Carrier l c= I by VECTSP_6:def 4;

then t in IQ by A1, A6;

then b * t in Lin IQ by VECTSP_4:21, VECTSP_7:8;

hence ex si being Vector of V st

( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ ) by A5, A4; :: thesis: verum

end;( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ ) )

assume i in dom (l (#) G) ; :: thesis: ex si being Vector of V st

( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ )

then i in Seg (len (l (#) G)) by FINSEQ_1:def 3;

then i in Seg (len G) by VECTSP_6:def 5;

then A3: i in dom G by FINSEQ_1:def 3;

then G . i in rng G by FUNCT_1:3;

then reconsider v = G . i as Element of V ;

A4: (l (#) G) . i = (l . v) * v by A3, ZMODUL02:13;

reconsider b = (l . v) mod p as Element of (GF p) by Lm3;

reconsider a = (l . v) mod p as Element of INT.Ring ;

reconsider k = l . v as Element of INT.Ring ;

reconsider t = ZMtoMQV (V,p,v) as Element of (Z_MQ_VectSp (V,p)) ;

A5: b * t = ZMtoMQV (V,p,(a * v)) by Th30

.= ZMtoMQV (V,p,(k * v)) by Lm4 ;

A6: v in Carrier l by A3, A2, FUNCT_1:3;

Carrier l c= I by VECTSP_6:def 4;

then t in IQ by A1, A6;

then b * t in Lin IQ by VECTSP_4:21, VECTSP_7:8;

hence ex si being Vector of V st

( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ ) by A5, A4; :: thesis: verum