let V be Z_Module; :: thesis: for I being Subset of V
for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
let I be Subset of V; :: thesis: for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
let l be Linear_Combination of I; :: thesis: for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
let IQ be Subset of (Z_MQ_VectSp V); :: thesis: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I implies ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) ) )
assume AS0: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I ) ; :: thesis: ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
reconsider I0 = Carrier l as finite Subset of V ;
K2: ( (MorphsZQ V) .: I0 c= IQ & (MorphsZQ V) .: I0 is finite ) by AS0, RELAT_1:123, VECTSP_6:def 4;
reconsider IQ0 = (MorphsZQ V) .: I0 as finite Subset of (Z_MQ_VectSp V) ;
defpred S1[ object , object ] means ( ( $1 in IQ0 & ex v being Element of V st
( v in I0 & $1 = (MorphsZQ V) . v & $2 = l . v ) ) or ( not $1 in IQ0 & $2 = 0. F_Rat ) );
A2: for x being object st x in the carrier of (Z_MQ_VectSp V) holds
ex y being object st
( y in RAT & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of (Z_MQ_VectSp V) implies ex y being object st
( y in RAT & S1[x,y] ) )
assume x in the carrier of (Z_MQ_VectSp V) ; :: thesis: ex y being object st
( y in RAT & S1[x,y] )
then reconsider x = x as Element of (Z_MQ_VectSp V) ;
per cases ( x in IQ0 or not x in IQ0 ) ;
suppose A3: x in IQ0 ; :: thesis: ex y being object st
( y in RAT & S1[x,y] )
then consider v being object such that
A4: ( v in the carrier of V & v in I0 & x = (MorphsZQ V) . v ) by FUNCT_2:64;
reconsider v = v as Element of V by A4;
l . v in RAT by NUMBERS:14, TARSKI:def 3;
hence ex y being object st
( y in RAT & S1[x,y] ) by A3, A4; :: thesis: verum
end;
suppose not x in IQ0 ; :: thesis: ex y being object st
( y in RAT & S1[x,y] )
hence ex y being object st
( y in RAT & S1[x,y] ) ; :: thesis: verum
end;
end;
end;
consider lq being Function of the carrier of (Z_MQ_VectSp V),RAT such that
A5: for x being object st x in the carrier of (Z_MQ_VectSp V) holds
S1[x,lq . x] from FUNCT_2:sch 1(A2);
 A6: for x being Element of (Z_MQ_VectSp V) st not x in IQ0 holds
lq . x = 0. F_Rat by A5;
lq is Element of Funcs ( the carrier of (Z_MQ_VectSp V),RAT) by FUNCT_2:8;
then reconsider lq = lq as Linear_Combination of Z_MQ_VectSp V by A6, VECTSP_6:def 1;
A11: Carrier lq c= IQ0
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier lq or x in IQ0 )
assume that
A7: x in Carrier lq and
A8: not x in IQ0 ; :: thesis: contradiction
consider z being Element of (Z_MQ_VectSp V) such that
A9: x = z and
A10: lq . z <> 0. F_Rat by A7;
thus contradiction by A5, A8, A9, A10; :: thesis: verum
end;
then reconsider lq = lq as Linear_Combination of IQ by K2, VECTSP_6:def 4, XBOOLE_1:1;
A12: dom l = the carrier of V by FUNCT_2:def 1;
A13: dom (lq * (MorphsZQ V)) = the carrier of V by FUNCT_2:def 1;
take lq ; :: thesis: ( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
F1: MorphsZQ V is one-to-one by defMorph, AS0;
for x being object st x in dom l holds
l . x = (lq * (MorphsZQ V)) . x
proof
let x be object ; :: thesis: ( x in dom l implies l . x = (lq * (MorphsZQ V)) . x )
assume x in dom l ; :: thesis: l . x = (lq * (MorphsZQ V)) . x
then reconsider v = x as Element of V ;
reconsider w = (MorphsZQ V) . v as Element of (Z_MQ_VectSp V) ;
per cases ( v in I0 or not v in I0 ) ;
suppose v in I0 ; :: thesis: l . x = (lq * (MorphsZQ V)) . x
then w in IQ0 by FUNCT_2:35;
then consider v0 being Element of V such that
A16: ( v0 in I0 & w = (MorphsZQ V) . v0 & lq . w = l . v0 ) by A5;
v0 = v by A16, FUNCT_2:19, F1;
hence l . x = (lq * (MorphsZQ V)) . x by A13, A16, FUNCT_1:12; :: thesis: verum
end;
suppose A18: not v in I0 ; :: thesis: l . x = (lq * (MorphsZQ V)) . x
then A19: l . v = 0. F_Rat ;
not w in IQ0
proof
assume w in IQ0 ; :: thesis: contradiction
then consider v0 being Element of V such that
A16: ( v0 in I0 & w = (MorphsZQ V) . v0 & lq . w = l . v0 ) by A5;
thus contradiction by A16, A18, F1, FUNCT_2:19; :: thesis: verum
end;
then lq . w = 0. F_Rat by A5;
hence l . x = (lq * (MorphsZQ V)) . x by A13, A19, FUNCT_1:12; :: thesis: verum
end;
end;
end;
hence U1: l = lq * (MorphsZQ V) by FUNCT_1:2, A12, A13; :: thesis: Carrier lq = (MorphsZQ V) .: (Carrier l)
IQ0 c= Carrier lq
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in IQ0 or x in Carrier lq )
assume x in IQ0 ; :: thesis: x in Carrier lq
then consider v being object such that
A4: ( v in the carrier of V & v in I0 & x = (MorphsZQ V) . v ) by FUNCT_2:64;
reconsider v = v as Element of V by A4;
x = (MorphsZQ V) . v by A4;
then reconsider y = x as Element of (Z_MQ_VectSp V) ;
X1: lq . y = l . v by A4, A13, U1, FUNCT_1:12;
l . v <> 0 by ZMODUL02:8, A4;
hence x in Carrier lq by X1; :: thesis: verum
end;
hence Carrier lq = (MorphsZQ V) .: (Carrier l) by A11; :: thesis: verum