let p be prime Element of INT.Ring; for V being free Z_Module
for I being Basis of V
for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp (V,p))
for lq being Linear_Combination of IQ st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } & ( for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ) holds
Sum lq = ZMtoMQV (V,p,(Sum l))
let V be free Z_Module; for I being Basis of V
for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp (V,p))
for lq being Linear_Combination of IQ st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } & ( for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ) holds
Sum lq = ZMtoMQV (V,p,(Sum l))
let I be Basis of V; for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp (V,p))
for lq being Linear_Combination of IQ st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } & ( for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ) holds
Sum lq = ZMtoMQV (V,p,(Sum l))
let l be Linear_Combination of I; for IQ being Subset of (Z_MQ_VectSp (V,p))
for lq being Linear_Combination of IQ st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } & ( for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ) holds
Sum lq = ZMtoMQV (V,p,(Sum l))
let IQ be Subset of (Z_MQ_VectSp (V,p)); for lq being Linear_Combination of IQ st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } & ( for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ) holds
Sum lq = ZMtoMQV (V,p,(Sum l))
let lq be Linear_Combination of IQ; ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } & ( for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ) implies Sum lq = ZMtoMQV (V,p,(Sum l)) )
assume A1:
IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I }
; ( ex v being Vector of V st
( v in I & not l . v = lq . (ZMtoMQV (V,p,v)) ) or Sum lq = ZMtoMQV (V,p,(Sum l)) )
assume A2:
for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v))
; Sum lq = ZMtoMQV (V,p,(Sum l))
per cases
( I is empty or not I is empty )
;
suppose
not
I is
empty
;
Sum lq = ZMtoMQV (V,p,(Sum l))then consider v0 being
object such that A7:
v0 in I
by XBOOLE_0:def 1;
reconsider v0 =
v0 as
Vector of
V by A7;
ZMtoMQV (
V,
p,
v0)
in IQ
by A7, A1;
then reconsider X =
IQ as non
empty Subset of
(Z_MQ_VectSp (V,p)) ;
consider F being
Function of
X, the
carrier of
V such that A8:
( ( for
u being
Vector of
V st
u in I holds
F . (ZMtoMQV (V,p,u)) = u ) &
F is
one-to-one &
dom F = X &
rng F = I )
by Th25, A1;
consider Gq being
FinSequence of
(Z_MQ_VectSp (V,p)) such that A9:
(
Gq is
one-to-one &
rng Gq = Carrier lq &
Sum lq = Sum (lq (#) Gq) )
by VECTSP_6:def 6;
set n =
len Gq;
A10:
dom Gq = Seg (len Gq)
by FINSEQ_1:def 3;
A11:
Carrier lq c= X
by VECTSP_6:def 4;
A12:
dom (F * Gq) = Seg (len Gq)
by A10, A9, A8, RELAT_1:27, VECTSP_6:def 4;
A13:
rng (F * Gq) c= the
carrier of
V
;
F * Gq is
FinSequence
by A8, A9, FINSEQ_1:16, VECTSP_6:def 4;
then reconsider FGq =
F * Gq as
FinSequence of
V by A13, FINSEQ_1:def 4;
for
x being
object holds
(
x in rng FGq iff
x in Carrier l )
proof
let x be
object ;
( x in rng FGq iff x in Carrier l )
hereby ( x in Carrier l implies x in rng FGq )
assume
x in rng FGq
;
x in Carrier lthen consider z being
object such that A14:
(
z in dom FGq &
x = FGq . z )
by FUNCT_1:def 3;
A15:
x = F . (Gq . z)
by A14, FUNCT_1:12;
A16:
(
z in dom Gq &
Gq . z in dom F )
by A14, FUNCT_1:11;
then consider u being
Vector of
V such that A17:
(
Gq . z = ZMtoMQV (
V,
p,
u) &
u in I )
by A1, A8;
A18:
F . (Gq . z) = u
by A8, A17;
consider w being
Element of
(Z_MQ_VectSp (V,p)) such that A19:
(
Gq . z = w &
lq . w <> 0. (GF p) )
by A9, A16, FUNCT_1:3, VECTSP_6:1;
l . u <> 0. (GF p)
by A2, A17, A19;
then
l . u <> 0
by EC_PF_1:11;
hence
x in Carrier l
by A15, A18;
verum
end;
assume A20:
x in Carrier l
;
x in rng FGq
then reconsider u =
x as
Vector of
V ;
A21:
l . u <> 0
by A20, ZMODUL02:8;
A22:
Carrier l c= I
by VECTSP_6:def 4;
then
lq . (ZMtoMQV (V,p,u)) <> 0
by A2, A21, A20;
then
lq . (ZMtoMQV (V,p,u)) <> 0. (GF p)
by EC_PF_1:11;
then A23:
ZMtoMQV (
V,
p,
u)
in rng Gq
by A9;
then consider z being
object such that A24:
(
z in dom Gq &
ZMtoMQV (
V,
p,
u)
= Gq . z )
by FUNCT_1:def 3;
A25:
F . (Gq . z) = u
by A20, A22, A24, A8;
A26:
z in dom FGq
by A11, A9, A24, A8, A23, FUNCT_1:11;
then
FGq . z = u
by A25, FUNCT_1:12;
hence
x in rng FGq
by A26, FUNCT_1:def 3;
verum
end; then
rng FGq = Carrier l
by TARSKI:2;
then A27:
Sum l = Sum (l (#) FGq)
by A9, A8, VECTSP_6:def 6;
A28:
len (l (#) FGq) = len FGq
by VECTSP_6:def 5;
then A29:
len (l (#) FGq) = len Gq
by A12, FINSEQ_1:def 3;
A30:
len (lq (#) Gq) = len Gq
by VECTSP_6:def 5;
now for i being Element of NAT st i in dom (l (#) FGq) holds
ex si being Vector of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = ZMtoMQV (V,p,si) )let i be
Element of
NAT ;
( i in dom (l (#) FGq) implies ex si being Vector of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = ZMtoMQV (V,p,si) ) )assume A31:
i in dom (l (#) FGq)
;
ex si being Vector of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = ZMtoMQV (V,p,si) )then
i in Seg (len FGq)
by A28, FINSEQ_1:def 3;
then A32:
i in dom FGq
by FINSEQ_1:def 3;
then
FGq . i in rng FGq
by FUNCT_1:3;
then reconsider v =
FGq . i as
Element of
V ;
A33:
(l (#) FGq) . i = (l . v) * v
by A32, ZMODUL02:13;
i in Seg (len Gq)
by A29, A31, FINSEQ_1:def 3;
then A34:
i in dom Gq
by FINSEQ_1:def 3;
then A35:
Gq . i in rng Gq
by FUNCT_1:3;
then A36:
Gq . i in X
by A9, A11;
reconsider w =
Gq . i as
Element of
(Z_MQ_VectSp (V,p)) by A35;
consider u being
Vector of
V such that A37:
(
Gq . i = ZMtoMQV (
V,
p,
u) &
u in I )
by A1, A36;
F . (Gq . i) = u
by A8, A37;
then A38:
v = u
by A32, FUNCT_1:12;
(lq (#) Gq) . i =
(lq . w) * w
by A34, VECTSP_6:8
.=
ZMtoMQV (
V,
p,
((l . v) * v))
by A2, A37, A38, Th30
;
hence
ex
si being
Vector of
V st
(
si = (l (#) FGq) . i &
(lq (#) Gq) . i = ZMtoMQV (
V,
p,
si) )
by A33;
verum end; hence
Sum lq = ZMtoMQV (
V,
p,
(Sum l))
by A9, A27, A29, A30, Th29;
verum end;