let p be prime Element of INT.Ring; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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);

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; :: thesis: 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; :: thesis: 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); :: thesis: 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 )
;

end;

suppose A1:
I is empty
; :: thesis: 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)) )

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 l = the Linear_Combination of I;

take the Linear_Combination of I ; :: thesis: 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) & the Linear_Combination of I . w = lq . (ZMtoMQV (V,p,v)) )

thus 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) & the Linear_Combination of I . w = lq . (ZMtoMQV (V,p,v)) ) by A1; :: thesis: verum

end;take the Linear_Combination of I ; :: thesis: 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) & the Linear_Combination of I . w = lq . (ZMtoMQV (V,p,v)) )

thus 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) & the Linear_Combination of I . w = lq . (ZMtoMQV (V,p,v)) ) by A1; :: thesis: verum

suppose A2:
not I is empty
; :: thesis: 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)) )

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 } ;

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 S_{1}[ 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 S_{1}[x,v]

A7: for x being Element of X holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A5);

defpred S_{2}[ 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 S_{2}[v,y]

consider f being Function of the carrier of V,(GF p) such that

A15: for v being Element of V holds S_{2}[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)) )

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 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 ; :: thesis: 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)) )

ex w being Vector of V st

( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) ) ; :: thesis: verum

end;now :: thesis: for x being object st x in { (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } holds

x in the carrier of (Z_MQ_VectSp (V,p))

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;x in the carrier of (Z_MQ_VectSp (V,p))

let x be object ; :: thesis: ( x in { (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } implies x in the carrier of (Z_MQ_VectSp (V,p)) )

assume x in { (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V,p))

then consider v being Vector of V such that

A3: ( x = ZMtoMQV (V,p,v) & v in I ) ;

thus x in the carrier of (Z_MQ_VectSp (V,p)) by A3; :: thesis: verum

end;assume x in { (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V,p))

then consider v being Vector of V such that

A3: ( x = ZMtoMQV (V,p,v) & v in I ) ;

thus x in the carrier of (Z_MQ_VectSp (V,p)) by A3; :: thesis: verum

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 S

A5: for x being Element of X ex v being Element of V st S

proof

consider F being Function of X, the carrier of V such that
let x be Element of X; :: thesis: ex v being Element of V st S_{1}[x,v]

x in X ;

then consider v being Vector of V such that

A6: ( x = ZMtoMQV (V,p,v) & v in I ) ;

thus ex v being Element of V st S_{1}[x,v]
by A6, ZMODUL01:58; :: thesis: verum

end;x in X ;

then consider v being Vector of V such that

A6: ( x = ZMtoMQV (V,p,v) & v in I ) ;

thus ex v being Element of V st S

A7: for x being Element of X holds S

A8: now :: thesis: for y being object st y in rng F holds

y in I

then A10:
rng F c= I
;y in I

let y be object ; :: thesis: ( y in rng F implies y in I )

assume y in rng F ; :: thesis: y in I

then consider x being object such that

A9: ( x in X & F . x = y ) by FUNCT_2:11;

reconsider x = x as Element of X by A9;

thus y in I by A9, A7; :: thesis: verum

end;assume y in rng F ; :: thesis: y in I

then consider x being object such that

A9: ( x in X & F . x = y ) by FUNCT_2:11;

reconsider x = x as Element of X by A9;

thus y in I by A9, A7; :: thesis: verum

defpred S

A11: for v being Element of V ex y being Element of (GF p) st S

proof

A14:
Segm p c= INT
by NUMBERS:17;
let v be Element of V; :: thesis: ex y being Element of (GF p) st S_{2}[v,y]

end;per cases
( v in rng F or not v in rng F )
;

end;

suppose A12:
v in rng F
; :: thesis: ex y being Element of (GF p) st S_{2}[v,y]

reconsider y = lq . (ZMtoMQV (V,p,v)) as Element of (GF p) ;

take y ; :: thesis: S_{2}[v,y]

thus S_{2}[v,y]
by A12; :: thesis: verum

end;take y ; :: thesis: S

thus S

suppose A13:
not v in rng F
; :: thesis: ex y being Element of (GF p) st S_{2}[v,y]

0. (GF p) is Element of (GF p)
;

then reconsider F0 = 0 as Element of (GF p) by EC_PF_1:11;

take F0 ; :: thesis: S_{2}[v,F0]

thus S_{2}[v,F0]
by A13; :: thesis: verum

end;then reconsider F0 = 0 as Element of (GF p) by EC_PF_1:11;

take F0 ; :: thesis: S

thus S

consider f being Function of the carrier of V,(GF p) such that

A15: for v being Element of V holds S

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

reconsider l = f as Function of the carrier of V,INT by A14, FUNCT_2:7;
let v be Vector of V; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) )

thus w in ZMtoMQV (V,p,v) by A7, A17; :: thesis: f . w = lq . (ZMtoMQV (V,p,v))

thus f . w = lq . (ZMtoMQV (V,p,v)) by A17, A19, A7, ZMODUL01:67; :: thesis: verum

end;( w in I & w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) ) )

assume v in I ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) )

thus w in ZMtoMQV (V,p,v) by A7, A17; :: thesis: f . w = lq . (ZMtoMQV (V,p,v))

thus f . w = lq . (ZMtoMQV (V,p,v)) by A17, A19, A7, ZMODUL01:67; :: thesis: verum

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 } ;

A20: now :: thesis: for v being object st v in { v where v is Element of V : l . v <> 0 } holds

v in the carrier of V

v in the carrier of V

let v be object ; :: thesis: ( v in { v where v is Element of V : l . v <> 0 } implies v in the carrier of V )

assume v in { v where v is Element of V : l . v <> 0 } ; :: thesis: v in the carrier of V

then ex v1 being Element of V st

( v1 = v & l . v1 <> 0 ) ;

hence v in the carrier of V ; :: thesis: verum

end;assume v in { v where v is Element of V : l . v <> 0 } ; :: thesis: v in the carrier of V

then ex v1 being Element of V st

( v1 = v & l . v1 <> 0 ) ;

hence v in the carrier of V ; :: thesis: verum

A21: now :: thesis: for x being object st x in { v where v is Element of V : l . v <> 0 } holds

x in rng F

then A23:
{ v where v is Element of V : l . v <> 0 } c= rng F
;x in rng F

let x be object ; :: thesis: ( x in { v where v is Element of V : l . v <> 0 } implies x in rng F )

assume x in { v where v is Element of V : l . v <> 0 } ; :: thesis: x in rng F

then consider v being Element of V such that

A22: ( x = v & l . v <> 0 ) ;

thus x in rng F by A15, A22; :: thesis: verum

end;assume x in { v where v is Element of V : l . v <> 0 } ; :: thesis: x in rng F

then consider v being Element of V such that

A22: ( x = v & l . v <> 0 ) ;

thus x in rng F by A15, A22; :: thesis: verum

now :: thesis: for x being object st x in F " { v where v is Element of V : l . v <> 0 } holds

x in Carrier lq

then
F " { v where v is Element of V : l . v <> 0 } c= Carrier lq
;x in Carrier lq

let x be object ; :: thesis: ( 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 } ; :: thesis: x in Carrier lq

then 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: S_{2}[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; :: thesis: verum

end;assume A24: x in F " { v where v is Element of V : l . v <> 0 } ; :: thesis: x in Carrier lq

then 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: S

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; :: thesis: verum

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 ; :: thesis: 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 :: thesis: 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)) )

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

let v be Vector of V; :: thesis: ( 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 ; :: thesis: 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)) ) ; :: thesis: verum

end;( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) ) )

assume v in I ; :: thesis: 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)) ) ; :: thesis: verum

ex w being Vector of V st

( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) ) ; :: thesis: verum