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 ; :: thesis: ( 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)):] ; :: thesis: ((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; :: thesis: 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
proof
let i be Element of INT.Ring; :: thesis: 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
let j be Element of F_Rat; :: thesis: for x being Vector of ZS
for v being Vector of Z st i = j & x = v holds
i * x = j * v
let x be Vector of ZS; :: thesis: for v being Vector of Z st i = j & x = v holds
i * x = j * v
let v be Vector of Z; :: thesis: ( i = j & x = v implies i * x = j * v )
assume L0: ( i = j & x = v ) ; :: thesis: i * x = j * v
thus i * x = (lmultCoset V) . [i,x] by FUNCT_1:49
.= j * v by L0, Z1 ; :: thesis: verum
end;
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)
proof
let x be Element of INT.Ring; :: thesis: for v, w being Element of ZS holds x * (v + w) = (x * v) + (x * w)
let v, w be Element of ZS; :: thesis: x * (v + w) = (x * v) + (x * w)
reconsider y = x as Element of F_Rat by NUMBERS:14;
reconsider s = v, t = w as Vector of Z by Z1;
P2: ( x * v = y * s & x * w = y * t ) by LM3;
thus x * (v + w) = y * (s + t) by Z1, LM3
.= (y * s) + (y * t) by VECTSP_1:def 14
.= (x * v) + (x * w) by P2, Z1 ; :: thesis: verum
end;
P2: for x, y being Element of INT.Ring
for v being Element of ZS holds (x + y) * v = (x * v) + (y * v)
proof
let x, y be Element of INT.Ring; :: thesis: for v being Element of ZS holds (x + y) * v = (x * v) + (y * v)
let v be Element of ZS; :: thesis: (x + y) * v = (x * v) + (y * v)
reconsider p = x, q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p, q1 = q as Rational ;
reconsider s = v as Vector of Z by Z1;
P2: y * v = q * s by LM3;
thus (x + y) * v = (p + q) * s by LM3
.= (p * s) + (q * s) by VECTSP_1:def 15
.= (x * v) + (y * v) by P2, Z1, LM3 ; :: thesis: verum
end;
P3: for x, y being Element of INT.Ring
for v being Element of ZS holds (x * y) * v = x * (y * v)
proof
let x, y be Element of INT.Ring; :: thesis: for v being Element of ZS holds (x * y) * v = x * (y * v)
let v be Element of ZS; :: thesis: (x * y) * v = x * (y * v)
reconsider p = x, q = y as Element of F_Rat by NUMBERS:14;
reconsider p1 = p, q1 = q as Rational ;
reconsider s = v as Vector of Z by Z1;
P1: y * v = q * s by LM3;
thus (x * y) * v = (p * q) * s by LM3
.= p * (q * s) by VECTSP_1:def 16
.= x * (y * v) by P1, LM3 ; :: thesis: verum
end;
P4: for v being Element of ZS holds (1. INT.Ring) * v = v
proof
let v be Element of ZS; :: thesis: (1. INT.Ring) * v = v
reconsider s = v as Vector of Z by Z1;
thus (1. INT.Ring) * v = (1. F_Rat) * s by LM3
.= v by VECTSP_1:def 17 ; :: thesis: verum
end;
P5: for v being Element of ZS holds v is right_complementable
proof
let v be Element of ZS; :: thesis: v is right_complementable
reconsider s = v as Vector of Z by Z1;
reconsider i1 = 1. F_Rat as Rational ;
P5: - s = (- (1. F_Rat)) * s by VECTSP_1:14;
v + ((- (1. INT.Ring)) * v) = s - s by P5, Z1, LM3
.= 0. ZS by Z2, RLVECT_1:15 ;
hence v is right_complementable ; :: thesis: verum
end;
P6: for v, w being Element of ZS holds v + w = w + v
proof
let v, w be Element of ZS; :: thesis: v + w = w + v
reconsider s = v, t = w as Vector of Z by Z1;
thus v + w = s + t by Z1
.= w + v by LM2 ; :: thesis: verum
end;
P7: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
proof
let u, v, w be Element of ZS; :: thesis: (u + v) + w = u + (v + w)
reconsider z = u, s = v, t = w as Vector of Z by Z1;
thus (u + v) + w = (z + s) + t by Z1
.= z + (s + t) by RLVECT_1:def 3
.= u + (v + w) by Z1 ; :: thesis: verum
end;
for v being Element of ZS holds v + (0. ZS) = v
proof
let v be Element of ZS; :: thesis: v + (0. ZS) = v
reconsider s = v as Vector of Z by Z1;
thus v + (0. ZS) = s + (0. Z) by Z1
.= v ; :: thesis: verum
end;
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; :: thesis: verum
end;
then reconsider ZS = ZS as strict Z_Module ;
take ZS ; :: thesis: ( 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)):] ) ; :: thesis: verum