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 S1[ 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: S1[ 0 ]
proof
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;
now :: thesis: for y being object st y in rng (a * lq) holds
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;
hence ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT ) by TARSKI:def 3; :: thesis: verum
end;
P2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume P21: S1[n] ; :: thesis: S1[n + 1]
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 )
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 S2[ 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 S2[v,y]
proof
let v be Element of (Z_MQ_VectSp V); :: thesis: ex y being Element of F_Rat st S2[v,y]
( v in {x} or not v in {x} ) ;
hence ex y being Element of F_Rat st S2[v,y] ; :: thesis: verum
end;
consider lq0 being Function of the carrier of (Z_MQ_VectSp V), the carrier of F_Rat such that
A4: for v being Element of (Z_MQ_VectSp V) holds S2[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}
proof
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;
(Carrier lq) \ {x} c= Carrier lq by XBOOLE_1:36;
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
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;
then card (Carrier lq0) = n by A400, P25, XBOOLE_0:def 10;
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
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;
per cases ( z in {x} or not z in {x} ) ;
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;
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;
end;
end;
hence ex m being Integer ex a being Element of F_Rat st
( m <> 0 & m = a & rng (a * lq) c= INT ) by X8, X9, TARSKI:def 3; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
P3: for n being Nat holds S1[n] from NAT_1:sch 2(P1, P2);
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 )
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;
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 ) ; :: thesis: verum