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;

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

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

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

R1:
{ v where v is Element of V : l . v <> 0 } c= (MorphsZQ V) " (Carrier lq)
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

proof

MorphsZQ V is one-to-one
by AS, defMorph;
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;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

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

then A9:
(MorphsZQ V) " (Carrier lq) = T
by R1;
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

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

proof

hence
x in T
; :: thesis: verum
assume
l . v = 0
; :: thesis: contradiction

then a1 * d1 = 0 by RR1;

hence contradiction by R11, X3; :: thesis: verum

end;then a1 * d1 = 0 by RR1;

hence contradiction by R11, X3; :: thesis: verum

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