let K be Ring; for V being LeftMod of K
for W being Subspace of V holds V / W is strict LeftMod of K
let V be LeftMod of K; for W being Subspace of V holds V / W is strict LeftMod of K
let W be Subspace of V; V / W is strict LeftMod of K
now let x,
y be
Scalar of
K;
for v, w being Vector of (V / W) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )let v,
w be
Vector of
(V / W);
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )consider a being
Vector of
V such that A1:
v = a / W
by Th28;
consider b being
Vector of
V such that A2:
w = b / W
by Th28;
A3:
(x * a) / W = x * v
by A1, Th30;
A4:
(x * b) / W = x * w
by A2, Th30;
A5:
(y * a) / W = y * v
by A1, Th30;
thus x * (v + w) =
x * ((a + b) / W)
by A1, A2, Th30
.=
(x * (a + b)) / W
by Th30
.=
((x * a) + (x * b)) / W
by VECTSP_1:def 26
.=
(x * v) + (x * w)
by A3, A4, Th30
;
( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )thus (x + y) * v =
((x + y) * a) / W
by A1, Th30
.=
((x * a) + (y * a)) / W
by VECTSP_1:def 27
.=
(x * v) + (y * v)
by A3, A5, Th30
;
( (x * y) * v = x * (y * v) & (1_ K) * v = v )thus (x * y) * v =
((x * y) * a) / W
by A1, Th30
.=
(x * (y * a)) / W
by VECTSP_1:def 28
.=
x * ((y * a) / W)
by Th30
.=
x * (y * v)
by A1, Th30
;
(1_ K) * v = vthus (1_ K) * v =
((1_ K) * a) / W
by A1, Th30
.=
v
by A1, VECTSP_1:def 29
;
verum end;
hence
V / W is strict LeftMod of K
by Lm2, VECTSP_1:def 26, VECTSP_1:def 27, VECTSP_1:def 28, VECTSP_1:def 29; verum