set M = the rmult of V;
set W = RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #);
A1:
RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is RightMod-like
proof
let a,
b be
Scalar of
R;
VECTSP_2:def 8 for b1, b2 being Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) holds
( (b1 + b2) * a = (b1 * a) + (b2 * a) & b1 * (a + b) = (b1 * a) + (b1 * b) & b1 * (b * a) = (b1 * b) * a & b1 * (1_ R) = b1 )let v,
w be
Vector of
RightModStr(# the
carrier of
V, the
addF of
V,
(0. V), the
rmult of
V #);
( (v + w) * a = (v * a) + (w * a) & v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v )
reconsider x =
v,
y =
w as
Vector of
V ;
thus (v + w) * a =
(x + y) * a
.=
(x * a) + (y * a)
by VECTSP_2:def 9
.=
(v * a) + (w * a)
;
( v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v )
thus v * (a + b) =
x * (a + b)
.=
(x * a) + (x * b)
by VECTSP_2:def 9
.=
(v * a) + (v * b)
;
( v * (b * a) = (v * b) * a & v * (1_ R) = v )
thus v * (b * a) =
x * (b * a)
.=
(x * b) * a
by VECTSP_2:def 9
.=
(v * b) * a
;
v * (1_ R) = v
thus v * (1_ R) =
x * (1_ R)
.=
v
by VECTSP_2:def 9
;
verum
end;
A2:
for a, b being Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
for x, y being Vector of V st x = a & b = y holds
a + b = x + y
;
( RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Abelian & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_complementable )
proof
thus
RightModStr(# the
carrier of
V, the
addF of
V,
(0. V), the
rmult of
V #) is
Abelian
( RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_complementable )
let a be
Element of
RightModStr(# the
carrier of
V, the
addF of
V,
(0. V), the
rmult of
V #);
ALGSTR_0:def 16 a is right_complementable
reconsider x =
a as
Vector of
V ;
reconsider b =
(comp V) . x as
Element of
RightModStr(# the
carrier of
V, the
addF of
V,
(0. V), the
rmult of
V #) ;
take
b
;
ALGSTR_0:def 11 a + b = 0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
thus a + b =
x + (- x)
by VECTSP_1:def 13
.=
0. RightModStr(# the
carrier of
V, the
addF of
V,
(0. V), the
rmult of
V #)
by RLVECT_1:5
;
verum
end;
then reconsider W = RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) as RightMod of R by A1;
A3:
( 0. W = 0. V & the addF of W = the addF of V || the carrier of W )
by RELSET_1:19;
the rmult of W = the rmult of V | [: the carrier of W, the carrier of R:]
by RELSET_1:19;
then reconsider W = W as Submodule of V by A3, Def2;
take
W
; W is strict
thus
W is strict
; verum