set Z = Z_MQ_VectSp V;
reconsider Z = Z_MQ_VectSp V as VectSp of F_Rat ;
set Mlt = (lmultCoset V) | [:INT,(Class (EQRZM V)):];
dom (lmultCoset V) = [: the carrier of F_Rat,(Class (EQRZM V)):]
by FUNCT_2:def 1;
then Y3:
dom ((lmultCoset V) | [:INT,(Class (EQRZM V)):]) = [:INT,(Class (EQRZM V)):]
by NUMBERS:14, RELAT_1:62, ZFMISC_1:96;
Z1:
Z = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #)
by ZMODUL04:def 5;
Z2:
0. Z = zeroCoset V
by Z1;
for x being object st x in [:INT,(Class (EQRZM V)):] holds
((lmultCoset V) | [:INT,(Class (EQRZM V)):]) . x in Class (EQRZM V)
proof
let x be
object ;
( x in [:INT,(Class (EQRZM V)):] implies ((lmultCoset V) | [:INT,(Class (EQRZM V)):]) . x in Class (EQRZM V) )
assume X40:
x in [:INT,(Class (EQRZM V)):]
;
((lmultCoset V) | [:INT,(Class (EQRZM V)):]) . x in Class (EQRZM V)
then consider i,
w being
object such that X41:
(
i in INT &
w in Class (EQRZM V) &
x = [i,w] )
by ZFMISC_1:def 2;
reconsider i =
i as
Element of
INT by X41;
reconsider j =
i as
Element of
F_Rat by NUMBERS:14;
reconsider b =
w as
Element of
Z by X41, Z1;
X46:
((lmultCoset V) | [:INT,(Class (EQRZM V)):]) . x = (lmultCoset V) . (
j,
w)
by X40, X41, FUNCT_1:49;
[j,w] in [: the carrier of F_Rat,(Class (EQRZM V)):]
by X41, ZFMISC_1:87;
hence
((lmultCoset V) | [:INT,(Class (EQRZM V)):]) . x in Class (EQRZM V)
by X46, FUNCT_2:5;
verum
end;
then reconsider Mlt = (lmultCoset V) | [:INT,(Class (EQRZM V)):] as Function of [: the carrier of INT.Ring,(Class (EQRZM V)):],(Class (EQRZM V)) by Y3, FUNCT_2:3;
set ZS = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),Mlt #);
reconsider ZS = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),Mlt #) as non empty ModuleStr over INT.Ring ;
LM2:
for x, y being Vector of ZS
for v, w being Vector of Z st x = v & y = w holds
x + y = v + w
by Z1;
LM3:
for i being Element of INT.Ring
for j being Element of F_Rat
for x being Vector of ZS
for v being Vector of Z st i = j & x = v holds
i * x = j * v
ZS is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over INT.Ring
proof
P1:
for
x being
Element of
INT.Ring for
v,
w being
Element of
ZS holds
x * (v + w) = (x * v) + (x * w)
P2:
for
x,
y being
Element of
INT.Ring for
v being
Element of
ZS holds
(x + y) * v = (x * v) + (y * v)
P3:
for
x,
y being
Element of
INT.Ring for
v being
Element of
ZS holds
(x * y) * v = x * (y * v)
P4:
for
v being
Element of
ZS holds
(1. INT.Ring) * v = v
P5:
for
v being
Element of
ZS holds
v is
right_complementable
P6:
for
v,
w being
Element of
ZS holds
v + w = w + v
P7:
for
u,
v,
w being
Element of
ZS holds
(u + v) + w = u + (v + w)
for
v being
Element of
ZS holds
v + (0. ZS) = v
hence
ZS is non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over
INT.Ring
by P1, P2, P3, P4, P5, P6, P7, ALGSTR_0:def 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;
verum
end;
then reconsider ZS = ZS as strict Z_Module ;
take
ZS
; ( the carrier of ZS = Class (EQRZM V) & the ZeroF of ZS = zeroCoset V & the addF of ZS = addCoset V & the lmult of ZS = (lmultCoset V) | [:INT,(Class (EQRZM V)):] )
thus
( the carrier of ZS = Class (EQRZM V) & the ZeroF of ZS = zeroCoset V & the addF of ZS = addCoset V & the lmult of ZS = (lmultCoset V) | [:INT,(Class (EQRZM V)):] )
; verum