let V be torsion-free Z_Module; :: thesis: EMbedding V is Submodule of DivisibleMod V
set EV = EMbedding V;
set DV = DivisibleMod V;
for x being object st x in the carrier of (EMbedding V) holds
x in the carrier of (DivisibleMod V)
proof
let x be object ; :: thesis: ( x in the carrier of (EMbedding V) implies x in the carrier of (DivisibleMod V) )
assume B1: x in the carrier of (EMbedding V) ; :: thesis: x in the carrier of (DivisibleMod V)
x in rng (MorphsZQ V) by B1, defEmbedding;
then consider y being object such that
B2: ( y in the carrier of V & (MorphsZQ V) . y = x ) by FUNCT_2:11;
reconsider y = y as Vector of V by B2;
B3: Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) by ZMODUL04:def 5;
x in Class (EQRZM V) by B2, B3, FUNCT_2:5;
hence x in the carrier of (DivisibleMod V) by defDivisibleMod; :: thesis: verum
end;
then A1: the carrier of (EMbedding V) c= the carrier of (DivisibleMod V) ;
A2: 0. (EMbedding V) = zeroCoset V by defEmbedding
.= 0. (DivisibleMod V) by defDivisibleMod ;
A3: the addF of (EMbedding V) = (addCoset V) || (rng (MorphsZQ V)) by defEmbedding
.= the addF of (DivisibleMod V) || (rng (MorphsZQ V)) by defDivisibleMod
.= the addF of (DivisibleMod V) || the carrier of (EMbedding V) by defEmbedding ;
the lmult of (EMbedding V) = the lmult of (DivisibleMod V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):]
proof
the carrier of (EMbedding V) c= Class (EQRZM V) by A1, defDivisibleMod;
then B1: rng (MorphsZQ V) c= Class (EQRZM V) by defEmbedding;
thus the lmult of (EMbedding V) = (lmultCoset V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):] by defEmbedding
.= ((lmultCoset V) | [: the carrier of INT.Ring,(Class (EQRZM V)):]) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):] by B1, RELAT_1:74, ZFMISC_1:96
.= the lmult of (DivisibleMod V) | [: the carrier of INT.Ring,(rng (MorphsZQ V)):] by defDivisibleMod ; :: thesis: verum
end;
then the lmult of (EMbedding V) = the lmult of (DivisibleMod V) | [: the carrier of INT.Ring, the carrier of (EMbedding V):] by defEmbedding;
hence EMbedding V is Submodule of DivisibleMod V by A1, A2, A3, VECTSP_4:def 2; :: thesis: verum