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