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 for x, y being 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 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 Th20;
consider b being
Vector of
V such that A2:
w = b / W
by Th20;
A3:
(x * a) / W = x * v
by A1, Th22;
A4:
(x * b) / W = x * w
by A2, Th22;
A5:
(y * a) / W = y * v
by A1, Th22;
thus x * (v + w) =
x * ((a + b) / W)
by A1, A2, Th22
.=
(x * (a + b)) / W
by Th22
.=
((x * a) + (x * b)) / W
by VECTSP_1:def 14
.=
(x * v) + (x * w)
by A3, A4, Th22
;
( (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, Th22
.=
((x * a) + (y * a)) / W
by VECTSP_1:def 15
.=
(x * v) + (y * v)
by A3, A5, Th22
;
( (x * y) * v = x * (y * v) & (1_ K) * v = v )thus (x * y) * v =
((x * y) * a) / W
by A1, Th22
.=
(x * (y * a)) / W
by VECTSP_1:def 16
.=
x * ((y * a) / W)
by Th22
.=
x * (y * v)
by A1, Th22
;
(1_ K) * v = vthus (1_ K) * v =
((1_ K) * a) / W
by A1, Th22
.=
v
by A1
;
verum end;
hence
V / W is strict LeftMod of K
by Lm2, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17; verum