let p be prime Element of INT.Ring; for V being free Z_Module
for I being Subset 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; for I being Subset 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 Subset 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 IQ be 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 l be Linear_Combination of I; ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies ZMtoMQV (V,p,(Sum l)) in Lin IQ )
assume AS:
IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I }
; ZMtoMQV (V,p,(Sum l)) in Lin IQ
consider G being FinSequence of V such that
P1:
( G is one-to-one & rng G = Carrier l & Sum l = Sum (l (#) G) )
by VECTSP_6:def 6;
now 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 )let i be
Element of
NAT ;
( 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)
;
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 Y3:
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 ;
Y5:
(l (#) G) . i = (l . v) * v
by Y3, ZMODUL02:13;
reconsider b =
(l . v) mod p as
Element of
(GF p) by EC_PF_1:14;
reconsider a =
(l . v) mod p as
Element of
INT.Ring ;
reconsider k =
l . v as
Element of
INT.Ring ;
reconsider si =
(l . v) * v as
Element of
V ;
reconsider t =
ZMtoMQV (
V,
p,
v) as
Element of
(Z_MQ_VectSp (V,p)) ;
Y7:
b * t =
ZMtoMQV (
V,
p,
(a * v))
by ZMODUL03:30
.=
ZMtoMQV (
V,
p,
(k * v))
by LMX2
;
H1:
v in Carrier l
by Y3, P1, FUNCT_1:3;
Carrier l c= I
by VECTSP_6:def 4;
then
t in IQ
by AS, H1;
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 Y7, Y5;
verum end;
hence
ZMtoMQV (V,p,(Sum l)) in Lin IQ
by AS, P1, ZMODUL03:33; verum