let R be Ring; for x, y being Scalar of R
for v, w being Vector of (RightModule R) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
set MLT = the multF of R;
set LS = RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #);
for x, y being Scalar of R
for v, w being Vector of RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
proof
let x,
y be
Scalar of
R;
for v, w being Vector of RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )let v,
w be
Vector of
RightModStr(# the
carrier of
R, the
addF of
R,
(0. R), the
multF of
R #);
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
reconsider v9 =
v,
w9 =
w as
Scalar of
R ;
thus (v + w) * x =
(v9 + w9) * x
.=
(v9 * x) + (w9 * x)
by VECTSP_1:def 7
.=
(v * x) + (w * x)
;
( v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (x + y) =
v9 * (x + y)
.=
(v9 * x) + (v9 * y)
by VECTSP_1:def 7
.=
(v * x) + (v * y)
;
( v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (y * x) =
v9 * (y * x)
.=
(v9 * y) * x
by GROUP_1:def 3
.=
(v * y) * x
;
v * (1_ R) = v
thus v * (1_ R) =
v9 * (1_ R)
.=
v
;
verum
end;
hence
for x, y being Scalar of R
for v, w being Vector of (RightModule R) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
; verum