set W = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #);
A1:
RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is RightMod-like
proof
let x,
y be
Element of
R;
VECTSP_2:def 8 for b1, b2 being Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) holds
( (b1 + b2) * x = (b1 * x) + (b2 * x) & b1 * (x + y) = (b1 * x) + (b1 * y) & b1 * (y * x) = (b1 * y) * x & b1 * (1_ R) = b1 )let v,
w be
Element of
RightModStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
rmult of
V #);
( (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
Vector of
V ;
thus (v + w) * x =
(v9 + w9) * x
.=
(v9 * x) + (w9 * x)
by VECTSP_2:def 9
.=
(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_2:def 9
.=
(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 VECTSP_2:def 9
.=
(v * y) * x
;
v * (1_ R) = v
thus v * (1_ R) =
v9 * (1_ R)
.=
v
by VECTSP_2:def 9
;
verum
end;
A2:
for a being Scalar of R
for v, w being Vector of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
for v9, w9 being Vector of V st v = v9 & w = w9 holds
( v + w = v9 + w9 & v * a = v9 * a )
;
( RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Abelian & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_complementable )
proof
thus
RightModStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
rmult of
V #) is
Abelian
( RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_complementable )
let x be
Element of
RightModStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
rmult of
V #);
ALGSTR_0:def 16 x is right_complementable
reconsider x9 =
x as
Vector of
V ;
consider b being
Vector of
V such that A3:
x9 + b = 0. V
by ALGSTR_0:def 11;
reconsider b9 =
b as
Element of
RightModStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
rmult of
V #) ;
take
b9
;
ALGSTR_0:def 11 x + b9 = 0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
thus
x + b9 = 0. RightModStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
rmult of
V #)
by A3;
verum
end;
then reconsider W = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) as RightMod of R by A1;
A4:
the rmult of W = the rmult of V | [: the carrier of W, the carrier of R:]
by RELSET_1:19;
( 0. W = 0. V & the addF of W = the addF of V | [: the carrier of W, the carrier of W:] )
by RELSET_1:19;
hence
RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is strict Submodule of V
by A4, Def2; verum