let R be Ring; :: thesis: 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 GF = addLoopStr(# the carrier of R,the addF of R,(0. R) #);
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;
:: thesis: 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 #);
:: thesis: ( (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 v' =
v,
w' =
w as
Scalar of
R ;
thus (v + w) * x =
(v' + w') * x
.=
(v' * x) + (w' * x)
by VECTSP_1:def 18
.=
(v * x) + (w * x)
;
:: thesis: ( v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (x + y) =
v' * (x + y)
.=
(v' * x) + (v' * y)
by VECTSP_1:def 18
.=
(v * x) + (v * y)
;
:: thesis: ( v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (y * x) =
v' * (y * x)
.=
(v' * y) * x
by GROUP_1:def 4
.=
(v * y) * x
;
:: thesis: v * (1_ R) = v
thus v * (1_ R) =
v' * (1_ R)
.=
v
by VECTSP_1:def 13
;
:: thesis: 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 )
; :: thesis: verum