set M = the lmult of V;
set W = ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #);
A1:
ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is vector-distributive
A2:
ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-distributive
A3:
ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-associative
A4:
ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is scalar-unital
A5:
for a, b being Element of ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
for x, y being Element of V st x = a & b = y holds
a + b = x + y
;
( ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Abelian & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is add-associative & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable )
proof
thus
ModuleStr(# the
carrier of
V, the
addF of
V,
(0. V), the
lmult of
V #) is
Abelian
( ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is add-associative & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_zeroed & ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is right_complementable )
let a be
Element of
ModuleStr(# the
carrier of
V, the
addF of
V,
(0. V), the
lmult of
V #);
ALGSTR_0:def 16 a is right_complementable
reconsider x =
a as
Element of
V ;
reconsider b =
(comp V) . x as
Element of
ModuleStr(# the
carrier of
V, the
addF of
V,
(0. V), the
lmult of
V #) ;
take
b
;
ALGSTR_0:def 11 a + b = 0. ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
thus a + b =
x + (- x)
by VECTSP_1:def 13
.=
0. ModuleStr(# the
carrier of
V, the
addF of
V,
(0. V), the
lmult of
V #)
by RLVECT_1:5
;
verum
end;
then reconsider W = ModuleStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF by A1, A2, A3, A4;
A6:
( 0. W = 0. V & the addF of W = the addF of V || the carrier of W )
by RELSET_1:19;
the lmult of W = the lmult of V | [: the carrier of GF, the carrier of W:]
by RELSET_1:19;
then reconsider W = W as Subspace of V by A6, Def2;
take
W
; W is strict
thus
W is strict
; verum