let V be Z_Module; :: thesis: for IQ being Subset of (Z_MQ_VectSp V)

for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

let IQ be Subset of (Z_MQ_VectSp V); :: thesis: for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

defpred S_{1}[ Nat] means for lq being Linear_Combination of IQ st card (Carrier lq) = $1 holds

ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT );

P1: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(P1, P2);

( m <> 0 & m = a & rng (a * lq) c= INT ) ; :: thesis: verum

for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

let IQ be Subset of (Z_MQ_VectSp V); :: thesis: for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

defpred S

ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT );

P1: S

proof

P2:
for n being Nat st S
let lq be Linear_Combination of IQ; :: thesis: ( card (Carrier lq) = 0 implies ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT ) )

assume P2: card (Carrier lq) = 0 ; :: thesis: ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

P3: Carrier lq = {} by P2;

reconsider m = 1 as Integer ;

reconsider a = m as Element of F_Rat ;

Carrier (a * lq) c= Carrier lq by VECTSP_6:28;

then Carrier (a * lq) = {} by P3;

then X1: a * lq = ZeroLC (Z_MQ_VectSp V) by VECTSP_6:def 3;

( m <> 0 & m = a & rng (a * lq) c= INT ) by TARSKI:def 3; :: thesis: verum

end;( m <> 0 & m = a & rng (a * lq) c= INT ) )

assume P2: card (Carrier lq) = 0 ; :: thesis: ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

P3: Carrier lq = {} by P2;

reconsider m = 1 as Integer ;

reconsider a = m as Element of F_Rat ;

Carrier (a * lq) c= Carrier lq by VECTSP_6:28;

then Carrier (a * lq) = {} by P3;

then X1: a * lq = ZeroLC (Z_MQ_VectSp V) by VECTSP_6:def 3;

now :: thesis: for y being object st y in rng (a * lq) holds

y in INT

hence
ex m being Integer ex a being Element of F_Rat st y in INT

let y be object ; :: thesis: ( y in rng (a * lq) implies y in INT )

assume y in rng (a * lq) ; :: thesis: y in INT

then consider x being Element of (Z_MQ_VectSp V) such that

X2: y = (a * lq) . x by FUNCT_2:113;

(a * lq) . x = 0. F_Rat by X1, VECTSP_6:3

.= 0 ;

hence y in INT by X2; :: thesis: verum

end;assume y in rng (a * lq) ; :: thesis: y in INT

then consider x being Element of (Z_MQ_VectSp V) such that

X2: y = (a * lq) . x by FUNCT_2:113;

(a * lq) . x = 0. F_Rat by X1, VECTSP_6:3

.= 0 ;

hence y in INT by X2; :: thesis: verum

( m <> 0 & m = a & rng (a * lq) c= INT ) by TARSKI:def 3; :: thesis: verum

S

proof

P3:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume P21: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume P21: S

now :: thesis: for lq being Linear_Combination of IQ st card (Carrier lq) = n + 1 holds

ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

hence
Sex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

let lq be Linear_Combination of IQ; :: thesis: ( card (Carrier lq) = n + 1 implies ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT ) )

assume P22: card (Carrier lq) = n + 1 ; :: thesis: ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

then Carrier lq <> {} ;

then consider x being object such that

P24: x in Carrier lq by XBOOLE_0:def 1;

reconsider x = x as Element of (Z_MQ_VectSp V) by P24;

P25: card ((Carrier lq) \ {x}) = (card (Carrier lq)) - (card {x}) by P24, CARD_2:44, ZFMISC_1:31

.= (n + 1) - 1 by P22, CARD_2:42

.= n ;

defpred S_{2}[ Element of (Z_MQ_VectSp V), Element of F_Rat] means ( ( $1 in {x} implies $2 = 0 ) & ( not $1 in {x} implies $2 = lq . $1 ) );

A2: for v being Element of (Z_MQ_VectSp V) ex y being Element of F_Rat st S_{2}[v,y]

A4: for v being Element of (Z_MQ_VectSp V) holds S_{2}[v,lq0 . v]
from FUNCT_2:sch 3(A2);

reconsider lq0 = lq0 as Element of Funcs ( the carrier of (Z_MQ_VectSp V), the carrier of F_Rat) by FUNCT_2:8;

set T = { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } ;

A400: { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } c= (Carrier lq) \ {x}

then A40: { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } c= Carrier lq by XBOOLE_1:1, A400;

reconsider T = { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } as finite Subset of (Z_MQ_VectSp V) by A400, XBOOLE_1:1;

for v being Element of (Z_MQ_VectSp V) st not v in T holds

lq0 . v = 0. F_Rat ;

then reconsider lq0 = lq0 as Linear_Combination of Z_MQ_VectSp V by VECTSP_6:def 1;

X5: T = Carrier lq0 ;

Carrier lq c= IQ by VECTSP_6:def 4;

then reconsider lq0 = lq0 as Linear_Combination of IQ by A40, X5, VECTSP_6:def 4, XBOOLE_1:1;

(Carrier lq) \ {x} c= T

then consider m0 being Integer, a0 being Element of F_Rat such that

X8: ( m0 <> 0 & m0 = a0 & rng (a0 * lq0) c= INT ) by P21;

consider k0, n0 being Integer such that

X9: ( n0 <> 0 & lq . x = k0 / n0 ) by RAT_1:1;

reconsider m = n0 * m0 as Integer ;

reconsider a = m as Element of F_Rat by RAT_1:def 2;

reconsider b = n0 as Element of F_Rat by RAT_1:def 2;

for y being object st y in rng (a * lq) holds

y in INT

( m <> 0 & m = a & rng (a * lq) c= INT ) by X8, X9, TARSKI:def 3; :: thesis: verum

end;( m <> 0 & m = a & rng (a * lq) c= INT ) )

assume P22: card (Carrier lq) = n + 1 ; :: thesis: ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

then Carrier lq <> {} ;

then consider x being object such that

P24: x in Carrier lq by XBOOLE_0:def 1;

reconsider x = x as Element of (Z_MQ_VectSp V) by P24;

P25: card ((Carrier lq) \ {x}) = (card (Carrier lq)) - (card {x}) by P24, CARD_2:44, ZFMISC_1:31

.= (n + 1) - 1 by P22, CARD_2:42

.= n ;

defpred S

A2: for v being Element of (Z_MQ_VectSp V) ex y being Element of F_Rat st S

proof

consider lq0 being Function of the carrier of (Z_MQ_VectSp V), the carrier of F_Rat such that
let v be Element of (Z_MQ_VectSp V); :: thesis: ex y being Element of F_Rat st S_{2}[v,y]

( v in {x} or not v in {x} ) ;

hence ex y being Element of F_Rat st S_{2}[v,y]
; :: thesis: verum

end;( v in {x} or not v in {x} ) ;

hence ex y being Element of F_Rat st S

A4: for v being Element of (Z_MQ_VectSp V) holds S

reconsider lq0 = lq0 as Element of Funcs ( the carrier of (Z_MQ_VectSp V), the carrier of F_Rat) by FUNCT_2:8;

set T = { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } ;

A400: { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } c= (Carrier lq) \ {x}

proof

(Carrier lq) \ {x} c= Carrier lq
by XBOOLE_1:36;
let v0 be object ; :: according to TARSKI:def 3 :: thesis: ( not v0 in { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } or v0 in (Carrier lq) \ {x} )

assume v0 in { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } ; :: thesis: v0 in (Carrier lq) \ {x}

then XX2: ex v1 being Element of (Z_MQ_VectSp V) st

( v1 = v0 & lq0 . v1 <> 0. F_Rat ) ;

then reconsider v = v0 as Element of (Z_MQ_VectSp V) ;

XX4: not v in {x} by A4, XX2;

lq . v <> 0. F_Rat by A4, XX2;

then v0 in Carrier lq ;

hence v0 in (Carrier lq) \ {x} by XBOOLE_0:def 5, XX4; :: thesis: verum

end;assume v0 in { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } ; :: thesis: v0 in (Carrier lq) \ {x}

then XX2: ex v1 being Element of (Z_MQ_VectSp V) st

( v1 = v0 & lq0 . v1 <> 0. F_Rat ) ;

then reconsider v = v0 as Element of (Z_MQ_VectSp V) ;

XX4: not v in {x} by A4, XX2;

lq . v <> 0. F_Rat by A4, XX2;

then v0 in Carrier lq ;

hence v0 in (Carrier lq) \ {x} by XBOOLE_0:def 5, XX4; :: thesis: verum

then A40: { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } c= Carrier lq by XBOOLE_1:1, A400;

reconsider T = { v where v is Element of (Z_MQ_VectSp V) : lq0 . v <> 0. F_Rat } as finite Subset of (Z_MQ_VectSp V) by A400, XBOOLE_1:1;

for v being Element of (Z_MQ_VectSp V) st not v in T holds

lq0 . v = 0. F_Rat ;

then reconsider lq0 = lq0 as Linear_Combination of Z_MQ_VectSp V by VECTSP_6:def 1;

X5: T = Carrier lq0 ;

Carrier lq c= IQ by VECTSP_6:def 4;

then reconsider lq0 = lq0 as Linear_Combination of IQ by A40, X5, VECTSP_6:def 4, XBOOLE_1:1;

(Carrier lq) \ {x} c= T

proof

then
card (Carrier lq0) = n
by A400, P25, XBOOLE_0:def 10;
let v0 be object ; :: according to TARSKI:def 3 :: thesis: ( not v0 in (Carrier lq) \ {x} or v0 in T )

assume YY11: v0 in (Carrier lq) \ {x} ; :: thesis: v0 in T

then YY1: ( v0 in Carrier lq & not v0 in {x} ) by XBOOLE_0:def 5;

reconsider v = v0 as Element of (Z_MQ_VectSp V) by YY11;

lq . v <> 0. F_Rat by YY1, VECTSP_6:2;

then lq0 . v <> 0. F_Rat by A4, YY1;

hence v0 in T ; :: thesis: verum

end;assume YY11: v0 in (Carrier lq) \ {x} ; :: thesis: v0 in T

then YY1: ( v0 in Carrier lq & not v0 in {x} ) by XBOOLE_0:def 5;

reconsider v = v0 as Element of (Z_MQ_VectSp V) by YY11;

lq . v <> 0. F_Rat by YY1, VECTSP_6:2;

then lq0 . v <> 0. F_Rat by A4, YY1;

hence v0 in T ; :: thesis: verum

then consider m0 being Integer, a0 being Element of F_Rat such that

X8: ( m0 <> 0 & m0 = a0 & rng (a0 * lq0) c= INT ) by P21;

consider k0, n0 being Integer such that

X9: ( n0 <> 0 & lq . x = k0 / n0 ) by RAT_1:1;

reconsider m = n0 * m0 as Integer ;

reconsider a = m as Element of F_Rat by RAT_1:def 2;

reconsider b = n0 as Element of F_Rat by RAT_1:def 2;

for y being object st y in rng (a * lq) holds

y in INT

proof

hence
ex m being Integer ex a being Element of F_Rat st
let y be object ; :: thesis: ( y in rng (a * lq) implies y in INT )

assume y in rng (a * lq) ; :: thesis: y in INT

then consider z being Element of (Z_MQ_VectSp V) such that

X2: y = (a * lq) . z by FUNCT_2:113;

end;assume y in rng (a * lq) ; :: thesis: y in INT

then consider z being Element of (Z_MQ_VectSp V) such that

X2: y = (a * lq) . z by FUNCT_2:113;

per cases
( z in {x} or not z in {x} )
;

end;

suppose B2:
z in {x}
; :: thesis: y in INT

BB2: y =
(a * lq) . x
by B2, X2, TARSKI:def 1

.= a * (lq . x) by VECTSP_6:def 9 ;

a * (lq . x) = (m0 * n0) * (k0 / n0) by X9

.= m0 * (n0 * (k0 / n0))

.= m0 * k0 by XCMPLX_1:87, X9 ;

hence y in INT by BB2, INT_1:def 2; :: thesis: verum

end;.= a * (lq . x) by VECTSP_6:def 9 ;

a * (lq . x) = (m0 * n0) * (k0 / n0) by X9

.= m0 * (n0 * (k0 / n0))

.= m0 * k0 by XCMPLX_1:87, X9 ;

hence y in INT by BB2, INT_1:def 2; :: thesis: verum

suppose
not z in {x}
; :: thesis: y in INT

then B31:
lq0 . z = lq . z
by A4;

BBB: a = b * a0 by X8;

B32: (a * lq) . z = a * (lq . z) by VECTSP_6:def 9

.= b * (a0 * (lq0 . z)) by B31, BBB

.= b * ((a0 * lq0) . z) by VECTSP_6:def 9 ;

(a0 * lq0) . z in rng (a0 * lq0) by FUNCT_2:4;

then reconsider aqz = (a0 * lq0) . z as Integer by X8;

b * ((a0 * lq0) . z) = n0 * aqz ;

hence y in INT by B32, X2, INT_1:def 2; :: thesis: verum

end;BBB: a = b * a0 by X8;

B32: (a * lq) . z = a * (lq . z) by VECTSP_6:def 9

.= b * (a0 * (lq0 . z)) by B31, BBB

.= b * ((a0 * lq0) . z) by VECTSP_6:def 9 ;

(a0 * lq0) . z in rng (a0 * lq0) by FUNCT_2:4;

then reconsider aqz = (a0 * lq0) . z as Integer by X8;

b * ((a0 * lq0) . z) = n0 * aqz ;

hence y in INT by B32, X2, INT_1:def 2; :: thesis: verum

( m <> 0 & m = a & rng (a * lq) c= INT ) by X8, X9, TARSKI:def 3; :: thesis: verum

now :: thesis: for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

hence
for lq being Linear_Combination of IQ ex m being Integer ex a being Element of F_Rat st ( m <> 0 & m = a & rng (a * lq) c= INT )

let lq be Linear_Combination of IQ; :: thesis: ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT )

card (Carrier lq) is Element of NAT ;

hence ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT ) by P3; :: thesis: verum

end;( m <> 0 & m = a & rng (a * lq) c= INT )

card (Carrier lq) is Element of NAT ;

hence ex m being Integer ex a being Element of F_Rat st

( m <> 0 & m = a & rng (a * lq) c= INT ) by P3; :: thesis: verum

( m <> 0 & m = a & rng (a * lq) c= INT ) ; :: thesis: verum