let p be prime Element of INT.Ring; for V being Z_Module
for I being Subset of V
for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )
let V be Z_Module; for I being Subset of V
for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )
let I be Subset of V; for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )
let lq be Linear_Combination of Z_MQ_VectSp (V,p); ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )
set ZQ = Z_MQ_VectSp (V,p);
per cases
( I is empty or not I is empty )
;
suppose A2:
not
I is
empty
;
ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )set X =
{ (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } ;
then reconsider X =
{ (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } as
Subset of
(Z_MQ_VectSp (V,p)) by TARSKI:def 3;
consider v0 being
object such that A4:
v0 in I
by A2, XBOOLE_0:def 1;
reconsider v0 =
v0 as
Vector of
V by A4;
ZMtoMQV (
V,
p,
v0)
in X
by A4;
then reconsider X =
X as non
empty Subset of
(Z_MQ_VectSp (V,p)) ;
defpred S1[
Element of
X,
Element of
V]
means ( $2
in $1 & $2
in I );
A5:
for
x being
Element of
X ex
v being
Element of
V st
S1[
x,
v]
consider F being
Function of
X, the
carrier of
V such that A7:
for
x being
Element of
X holds
S1[
x,
F . x]
from FUNCT_2:sch 3(A5);
then A10:
rng F c= I
;
defpred S2[
Element of
V,
Element of
(GF p)]
means ( ( $1
in rng F implies $2
= lq . (ZMtoMQV (V,p,$1)) ) & ( not $1
in rng F implies $2
= 0 ) );
A11:
for
v being
Element of
V ex
y being
Element of
(GF p) st
S2[
v,
y]
A14:
Segm p c= INT
by NUMBERS:17;
consider f being
Function of the
carrier of
V,
(GF p) such that A15:
for
v being
Element of
V holds
S2[
v,
f . v]
from FUNCT_2:sch 3(A11);
A16:
for
v being
Vector of
V st
v in I holds
ex
w being
Vector of
V st
(
w in I &
w in ZMtoMQV (
V,
p,
v) &
f . w = lq . (ZMtoMQV (V,p,v)) )
proof
let v be
Vector of
V;
( v in I implies ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) ) )
assume
v in I
;
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) )
then A17:
ZMtoMQV (
V,
p,
v)
in X
;
then A18:
F . (ZMtoMQV (V,p,v)) in rng F
by FUNCT_2:4;
reconsider w =
F . (ZMtoMQV (V,p,v)) as
Element of
V by A17, FUNCT_2:5;
take
w
;
( w in I & w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) )
A19:
f . w = lq . (ZMtoMQV (V,p,w))
by A15, A17, FUNCT_2:4;
thus
w in I
by A18, A8;
( w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) )
thus
w in ZMtoMQV (
V,
p,
v)
by A7, A17;
f . w = lq . (ZMtoMQV (V,p,v))
thus
f . w = lq . (ZMtoMQV (V,p,v))
by A17, A19, A7, ZMODUL01:67;
verum
end; reconsider l =
f as
Function of the
carrier of
V,
INT by A14, FUNCT_2:7;
reconsider l =
l as
Element of
Funcs ( the
carrier of
V,
INT)
by FUNCT_2:8;
set T =
{ v where v is Element of V : l . v <> 0 } ;
then A23:
{ v where v is Element of V : l . v <> 0 } c= rng F
;
now for x being object st x in F " { v where v is Element of V : l . v <> 0 } holds
x in Carrier lqlet x be
object ;
( x in F " { v where v is Element of V : l . v <> 0 } implies x in Carrier lq )assume A24:
x in F " { v where v is Element of V : l . v <> 0 }
;
x in Carrier lqthen A25:
(
x in X &
F . x in { v where v is Element of V : l . v <> 0 } )
by FUNCT_2:38;
then consider v being
Element of
V such that A26:
(
F . x = v &
l . v <> 0 )
;
A27:
S2[
v,
f . v]
by A15;
lq . (ZMtoMQV (V,p,v)) <> 0. (GF p)
by A26, A27, EC_PF_1:11;
then A28:
ZMtoMQV (
V,
p,
v)
in Carrier lq
;
reconsider w =
x as
Element of
X by A24;
A29:
(
F . w in w &
F . w in I )
by A7;
consider v1 being
Vector of
V such that A30:
(
w = ZMtoMQV (
V,
p,
v1) &
v1 in I )
by A25;
v in ZMtoMQV (
V,
p,
v)
by ZMODUL01:58;
then
(ZMtoMQV (V,p,v)) /\ (ZMtoMQV (V,p,v1)) <> {}
by A26, A29, A30, XBOOLE_0:def 4;
hence
x in Carrier lq
by A28, A30, Lm2;
verum end; then
F " { v where v is Element of V : l . v <> 0 } c= Carrier lq
;
then reconsider T =
{ v where v is Element of V : l . v <> 0 } as
finite Subset of
V by A20, A21, FINSET_1:9, TARSKI:def 3;
for
v being
Element of
V st not
v in T holds
l . v = 0. INT.Ring
;
then reconsider l =
l as
Linear_Combination of
V by VECTSP_6:def 1;
T = Carrier l
;
then reconsider l =
l as
Linear_Combination of
I by A23, A10, XBOOLE_1:1, VECTSP_6:def 4;
take
l
;
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )now for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )let v be
Vector of
V;
( v in I implies ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) ) )assume
v in I
;
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )then
ex
w being
Vector of
V st
(
w in I &
w in ZMtoMQV (
V,
p,
v) &
f . w = lq . (ZMtoMQV (V,p,v)) )
by A16;
hence
ex
w being
Vector of
V st
(
w in I &
w in ZMtoMQV (
V,
p,
v) &
l . w = lq . (ZMtoMQV (V,p,v)) )
;
verum end; hence
for
v being
Vector of
V st
v in I holds
ex
w being
Vector of
V st
(
w in I &
w in ZMtoMQV (
V,
p,
v) &
l . w = lq . (ZMtoMQV (V,p,v)) )
;
verum end;