let V be torsion-free Z_Module; :: thesis: ( ( for v, w being Vector of (Z_MQ_VectSp V) st v in EMbedding V & w in EMbedding V holds
v + w in EMbedding V ) & ( for j being Element of F_Rat
for v being Vector of (Z_MQ_VectSp V) st j in INT & v in EMbedding V holds
j * v in EMbedding V ) )
set EZV = Z_MQ_VectSp V;
set ZS = EMbedding V;
set Cl = the carrier of (EMbedding V);
set Add = (addCoset V) || the carrier of (EMbedding V);
set Mlt = (lmultCoset V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):];
thus for v, w being Vector of (Z_MQ_VectSp V) st v in EMbedding V & w in EMbedding V holds
v + w in EMbedding V :: thesis: for j being Element of F_Rat
for v being Vector of (Z_MQ_VectSp V) st j in INT & v in EMbedding V holds
j * v in EMbedding V
proof
let v, w be Vector of (Z_MQ_VectSp V); :: thesis: ( v in EMbedding V & w in EMbedding V implies v + w in EMbedding V )
assume B1: ( v in EMbedding V & w in EMbedding V ) ; :: thesis: v + w in EMbedding V
reconsider v1 = v, w1 = w as Vector of (EMbedding V) by B1;
v + w = v1 + w1 by SB01;
hence v + w in EMbedding V ; :: thesis: verum
end;
thus for j being Element of F_Rat
for v being Vector of (Z_MQ_VectSp V) st j in INT & v in EMbedding V holds
j * v in EMbedding V :: thesis: verum
proof
let j be Element of F_Rat; :: thesis: for v being Vector of (Z_MQ_VectSp V) st j in INT & v in EMbedding V holds
j * v in EMbedding V
let v be Vector of (Z_MQ_VectSp V); :: thesis: ( j in INT & v in EMbedding V implies j * v in EMbedding V )
assume B1: ( j in INT & v in EMbedding V ) ; :: thesis: j * v in EMbedding V
then reconsider v1 = v as Vector of (EMbedding V) ;
reconsider i = j as Element of INT.Ring by B1;
j * v = i * v1 by SB01;
hence j * v in EMbedding V ; :: thesis: verum
end;