let V be divisible Z_Module; for W being Submodule of V holds VectQuot (V,W) is divisible
let W be Submodule of V; VectQuot (V,W) is divisible
set VW = VectQuot (V,W);
X0:
the carrier of (VectQuot (V,W)) = CosetSet (V,W)
by VECTSP10:def 6;
for vw being Vector of (VectQuot (V,W)) holds vw is divisible
proof
let vw be
Vector of
(VectQuot (V,W));
vw is divisible
for
a being
Element of
INT.Ring st
a <> 0 holds
ex
u being
Vector of
(VectQuot (V,W)) st
a * u = vw
proof
let a be
Element of
INT.Ring;
( a <> 0 implies ex u being Vector of (VectQuot (V,W)) st a * u = vw )
assume AS:
a <> 0
;
ex u being Vector of (VectQuot (V,W)) st a * u = vw
vw in CosetSet (
V,
W)
by X0;
then consider A being
Coset of
W such that X1:
vw = A
;
consider v being
Vector of
V such that X2:
A = v + W
by VECTSP_4:def 6;
v is
divisible
by defDivisibleModule;
then consider u0 being
Vector of
V such that X3:
a * u0 = v
by AS;
u0 + W is
Coset of
W
by VECTSP_4:def 6;
then
u0 + W in CosetSet (
V,
W)
;
then reconsider B =
u0 + W as
Element of
CosetSet (
V,
W) ;
reconsider u =
B as
Vector of
(VectQuot (V,W)) by VECTSP10:def 6;
take
u
;
a * u = vw
thus a * u =
(lmultCoset (V,W)) . (
a,
B)
by VECTSP10:def 6
.=
vw
by X1, X2, X3, VECTSP10:def 5
;
verum
end;
hence
vw is
divisible
;
verum
end;
hence
VectQuot (V,W) is divisible
; verum