let V be Z_Module; :: thesis: for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
let IQ be Subset of (Z_MQ_VectSp V); :: thesis: for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
let lq be Linear_Combination of IQ; :: thesis: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I implies ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l ) )
assume AS: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I ) ; :: thesis: ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
consider m being Integer, a being Element of F_Rat such that
X3: ( m <> 0 & m = a & rng (a * lq) c= INT ) by ThEQRZMV3A;
reconsider mm = m as Element of INT.Ring by INT_1:def 2;
P81: rng ((a * lq) * (MorphsZQ V)) c= rng (a * lq) by RELAT_1:26;
dom ((a * lq) * (MorphsZQ V)) = the carrier of V by FUNCT_2:def 1;
then (a * lq) * (MorphsZQ V) is Function of the carrier of V,INT by P81, X3, FUNCT_2:2, XBOOLE_1:1;
then reconsider l = (a * lq) * (MorphsZQ V) 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 } ;
set F = MorphsZQ V;
B2: 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
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;
R1: { v where v is Element of V : l . v <> 0 } c= (MorphsZQ V) " (Carrier lq)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of V : l . v <> 0 } or x in (MorphsZQ V) " (Carrier lq) )
assume x in { v where v is Element of V : l . v <> 0 } ; :: thesis: x in (MorphsZQ V) " (Carrier lq)
then consider v being Element of V such that
R11: ( x = v & l . v <> 0 ) ;
RRR: dom (MorphsZQ V) = the carrier of V by FUNCT_2:def 1;
V1: l . v = (a * lq) . ((MorphsZQ V) . v) by FUNCT_1:13, RRR
.= a * (lq . ((MorphsZQ V) . v)) by VECTSP_6:def 9 ;
lq . ((MorphsZQ V) . v) <> 0. F_Rat by V1, R11;
then (MorphsZQ V) . v in Carrier lq ;
hence x in (MorphsZQ V) " (Carrier lq) by R11, FUNCT_2:38; :: thesis: verum
end;
MorphsZQ V is one-to-one by AS, defMorph;
then (MorphsZQ V) " (Carrier lq) = ((MorphsZQ V) ") .: (Carrier lq) by FUNCT_1:85;
then reconsider T = { v where v is Element of V : l . v <> 0 } as finite Subset of V by B2, R1, 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;
(MorphsZQ V) " (Carrier lq) c= T
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (MorphsZQ V) " (Carrier lq) or x in T )
assume S21: x in (MorphsZQ V) " (Carrier lq) ; :: thesis: x in T
then ( x in the carrier of V & (MorphsZQ V) . x in Carrier lq ) by FUNCT_2:38;
then consider w being Element of (Z_MQ_VectSp V) such that
R11: ( (MorphsZQ V) . x = w & lq . w <> 0. F_Rat ) ;
reconsider v = x as Element of V by S21;
RRR: dom (MorphsZQ V) = the carrier of V by FUNCT_2:def 1;
RR1: l . v = (a * lq) . ((MorphsZQ V) . v) by FUNCT_1:13, RRR
.= a * (lq . w) by R11, VECTSP_6:def 9 ;
reconsider a1 = a, d1 = lq . w as Rational ;
l . v <> 0 by RR1, R11, X3;
hence x in T ; :: thesis: verum
end;
then A9: (MorphsZQ V) " (Carrier lq) = T by R1;
A7: T = Carrier l ;
AA1: (MorphsZQ V) " (Carrier lq) c= (MorphsZQ V) " ((MorphsZQ V) .: I) by AS, RELAT_1:143, VECTSP_6:def 4;
dom (MorphsZQ V) = the carrier of V by FUNCT_2:def 1;
then ( MorphsZQ V is one-to-one & I c= dom (MorphsZQ V) ) by AS, defMorph;
then T c= I by A9, AA1, FUNCT_1:94;
then reconsider l1 = l as Linear_Combination of I by A7, VECTSP_6:def 4;
take mm ; :: thesis: ex a being Element of F_Rat ex l being Linear_Combination of I st
( mm <> 0. INT.Ring & mm = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
take a ; :: thesis: ex l being Linear_Combination of I st
( mm <> 0. INT.Ring & mm = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
take l1 ; :: thesis: ( mm <> 0. INT.Ring & mm = a & l1 = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l1 )
thus ( mm <> 0. INT.Ring & mm = a & l1 = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l1 ) by A9, X3; :: thesis: verum