definition
let V be
Z_Module;
let W be
Submodule of
V;
existence
ex b1 being BinOp of (CosetSet (V,W)) st
for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
b1 . (A,B) = (a + b) + W
uniqueness
for b1, b2 being BinOp of (CosetSet (V,W)) st ( for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
b1 . (A,B) = (a + b) + W ) & ( for A, B being Element of CosetSet (V,W)
for a, b being VECTOR of V st A = a + W & B = b + W holds
b2 . (A,B) = (a + b) + W ) holds
b1 = b2
end;
definition
let V be
Z_Module;
let W be
Submodule of
V;
existence
ex b1 being Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) st
for z being Element of INT.Ring
for A being Element of CosetSet (V,W)
for a being VECTOR of V st A = a + W holds
b1 . (z,A) = (z * a) + W
uniqueness
for b1, b2 being Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) st ( for z being Element of INT.Ring
for A being Element of CosetSet (V,W)
for a being VECTOR of V st A = a + W holds
b1 . (z,A) = (z * a) + W ) & ( for z being Element of INT.Ring
for A being Element of CosetSet (V,W)
for a being VECTOR of V st A = a + W holds
b2 . (z,A) = (z * a) + W ) holds
b1 = b2
end;
definition
let V be
Z_Module;
let W be
Submodule of
V;
existence
ex b1 being strict Z_Module st
( the carrier of b1 = CosetSet (V,W) & the addF of b1 = addCoset (V,W) & 0. b1 = zeroCoset (V,W) & the lmult of b1 = lmultCoset (V,W) )
uniqueness
for b1, b2 being strict Z_Module st the carrier of b1 = CosetSet (V,W) & the addF of b1 = addCoset (V,W) & 0. b1 = zeroCoset (V,W) & the lmult of b1 = lmultCoset (V,W) & the carrier of b2 = CosetSet (V,W) & the addF of b2 = addCoset (V,W) & 0. b2 = zeroCoset (V,W) & the lmult of b2 = lmultCoset (V,W) holds
b1 = b2
;
end;
Lem1:
for i being Integer holds i in the carrier of INT.Ring
definition
let p be
prime Element of
INT.Ring;
let V be
Z_Module;
existence
ex b1 being Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) st
for a being Element of (GF p)
for i being Element of INT.Ring
for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds
b1 . (a,x) = (i mod p) * x
uniqueness
for b1, b2 being Function of [: the carrier of (GF p), the carrier of (Z_ModuleQuot (V,(p (*) V))):], the carrier of (Z_ModuleQuot (V,(p (*) V))) st ( for a being Element of (GF p)
for i being Element of INT.Ring
for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds
b1 . (a,x) = (i mod p) * x ) & ( for a being Element of (GF p)
for i being Element of INT.Ring
for x being Element of (Z_ModuleQuot (V,(p (*) V))) st a = i mod p holds
b2 . (a,x) = (i mod p) * x ) holds
b1 = b2
end;
Lm3:
for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W2 & W1 is Submodule of W3 holds
W1 is Submodule of W2 /\ W3
Lm4:
for V being Z_Module
for W1, W2, W3 being Submodule of V st W1 is Submodule of W3 & W2 is Submodule of W3 holds
W1 + W2 is Submodule of W3