let V be torsion-free Z_Module; :: thesis: for r being Element of F_Rat holds EMbedding (r,V) is Submodule of DivisibleMod V
let r be Element of F_Rat; :: thesis: EMbedding (r,V) is Submodule of DivisibleMod V
set Z = EMbedding (r,V);
set D = DivisibleMod V;
for x being object st x in the carrier of (EMbedding (r,V)) holds
x in the carrier of (DivisibleMod V)
proof
let x be object ; :: thesis: ( x in the carrier of (EMbedding (r,V)) implies x in the carrier of (DivisibleMod V) )
assume B1: x in the carrier of (EMbedding (r,V)) ; :: thesis: x in the carrier of (DivisibleMod V)
x is Vector of (Z_MQ_VectSp V) by B1, rSB01;
then x is Vector of (DivisibleMod V) by ThDivisibleX1;
hence x in the carrier of (DivisibleMod V) ; :: thesis: verum
end;
then A1: the carrier of (EMbedding (r,V)) c= the carrier of (DivisibleMod V) ;
A2: the addF of (EMbedding (r,V)) = (addCoset V) || (r * (rng (MorphsZQ V))) by defriV
.= (addCoset V) || the carrier of (EMbedding (r,V)) by defriV
.= the addF of (DivisibleMod V) || the carrier of (EMbedding (r,V)) by defDivisibleMod ;
A3: 0. (EMbedding (r,V)) = zeroCoset V by defriV
.= 0. (DivisibleMod V) by defDivisibleMod ;
A4: [: the carrier of INT.Ring, the carrier of (EMbedding (r,V)):] c= [: the carrier of INT.Ring, the carrier of (DivisibleMod V):] by A1, ZFMISC_1:96;
the lmult of (DivisibleMod V) | [: the carrier of INT.Ring, the carrier of (EMbedding (r,V)):] = ((lmultCoset V) | [: the carrier of INT.Ring,(Class (EQRZM V)):]) | [: the carrier of INT.Ring, the carrier of (EMbedding (r,V)):] by defDivisibleMod
.= ((lmultCoset V) | [: the carrier of INT.Ring, the carrier of (DivisibleMod V):]) | [:INT, the carrier of (EMbedding (r,V)):] by defDivisibleMod
.= (lmultCoset V) | [: the carrier of INT.Ring, the carrier of (EMbedding (r,V)):] by A4, FUNCT_1:51
.= (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] by defriV
.= the lmult of (EMbedding (r,V)) by defriV ;
hence EMbedding (r,V) is Submodule of DivisibleMod V by A1, A2, A3, VECTSP_4:def 2; :: thesis: verum