set M = Z_MQ_VectSp (V,p);
set F = GF p;
set AD = the addF of (VectQuot (V,(p (*) V)));
set ML = lmultCoset (V,(p (*) V));
thus
Z_MQ_VectSp (V,p) is scalar-distributive
( Z_MQ_VectSp (V,p) is vector-distributive & Z_MQ_VectSp (V,p) is scalar-associative & Z_MQ_VectSp (V,p) is scalar-unital & Z_MQ_VectSp (V,p) is add-associative & Z_MQ_VectSp (V,p) is right_zeroed & Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )proof
let x,
y be
Element of
(GF p);
VECTSP_1:def 14 for b1 being Element of the carrier of (Z_MQ_VectSp (V,p)) holds (x + y) * b1 = (x * b1) + (y * b1)let v be
Element of
(Z_MQ_VectSp (V,p));
(x + y) * v = (x * v) + (y * v)
consider i being
Nat such that A1:
x = i mod p
by EC_PF_1:13;
reconsider i =
i as
Element of
INT.Ring by Lem1;
consider j being
Nat such that A2:
y = j mod p
by EC_PF_1:13;
reconsider j =
j as
Element of
INT.Ring by Lem1;
reconsider v1 =
v as
Element of
(VectQuot (V,(p (*) V))) ;
A3:
x + y =
(i + j) mod p
by A1, A2, EC_PF_1:15
.=
((i mod p) + (j mod p)) mod p
by EULER_2:6
;
A4:
x * v = (i mod p) * v1
by Def11, A1;
A5:
y * v = (j mod p) * v1
by Def11, A2;
(((i mod p) + (j mod p)) mod p) * v1 =
((i mod p) + (j mod p)) * v1
by Th2
.=
((i mod p) * v1) + ((j mod p) * v1)
by VECTSP_1:def 15
;
hence
(x + y) * v = (x * v) + (y * v)
by A3, A4, A5, Def11;
verum
end;
thus
Z_MQ_VectSp (V,p) is vector-distributive
( Z_MQ_VectSp (V,p) is scalar-associative & Z_MQ_VectSp (V,p) is scalar-unital & Z_MQ_VectSp (V,p) is add-associative & Z_MQ_VectSp (V,p) is right_zeroed & Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )proof
let x be
Element of
(GF p);
VECTSP_1:def 13 for b1, b2 being Element of the carrier of (Z_MQ_VectSp (V,p)) holds x * (b1 + b2) = (x * b1) + (x * b2)let v,
w be
Element of
(Z_MQ_VectSp (V,p));
x * (v + w) = (x * v) + (x * w)
consider i being
Nat such that A6:
x = i mod p
by EC_PF_1:13;
reconsider i =
i as
Element of
INT.Ring by Lem1;
reconsider v1 =
v,
w1 =
w as
Element of
(VectQuot (V,(p (*) V))) ;
A7:
x * w = (i mod p) * w1
by Def11, A6;
thus x * (v + w) =
(i mod p) * (v1 + w1)
by Def11, A6
.=
((i mod p) * v1) + ((i mod p) * w1)
by VECTSP_1:def 14
.=
(x * v) + (x * w)
by A6, A7, Def11
;
verum
end;
thus
Z_MQ_VectSp (V,p) is scalar-associative
( Z_MQ_VectSp (V,p) is scalar-unital & Z_MQ_VectSp (V,p) is add-associative & Z_MQ_VectSp (V,p) is right_zeroed & Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )proof
let x,
y be
Element of
(GF p);
VECTSP_1:def 15 for b1 being Element of the carrier of (Z_MQ_VectSp (V,p)) holds (x * y) * b1 = x * (y * b1)let v be
Element of
(Z_MQ_VectSp (V,p));
(x * y) * v = x * (y * v)
consider i being
Nat such that A8:
x = i mod p
by EC_PF_1:13;
reconsider i =
i as
Element of
INT.Ring by Lem1;
consider j being
Nat such that A9:
y = j mod p
by EC_PF_1:13;
reconsider j =
j as
Element of
INT.Ring by Lem1;
reconsider v1 =
v as
Element of
(VectQuot (V,(p (*) V))) ;
A10:
x * y = (i * j) mod p
by A8, A9, EC_PF_1:18;
A11:
y * v = (j mod p) * v1
by Def11, A9;
A12:
x * (y * v) = (i mod p) * ((j mod p) * v1)
by A8, A11, Def11;
((i * j) mod p) * v1 =
(i * j) * v1
by Th2
.=
i * (j * v1)
by VECTSP_1:def 16
.=
i * ((j mod p) * v1)
by Th2
.=
(i mod p) * ((j mod p) * v1)
by Th2
;
hence
(x * y) * v = x * (y * v)
by A10, A12, Def11;
verum
end;
thus
Z_MQ_VectSp (V,p) is scalar-unital
( Z_MQ_VectSp (V,p) is add-associative & Z_MQ_VectSp (V,p) is right_zeroed & Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )
thus
Z_MQ_VectSp (V,p) is add-associative
( Z_MQ_VectSp (V,p) is right_zeroed & Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )
thus
Z_MQ_VectSp (V,p) is right_zeroed
( Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )
thus
Z_MQ_VectSp (V,p) is right_complementable
Z_MQ_VectSp (V,p) is Abelian
let v, w be Element of (Z_MQ_VectSp (V,p)); RLVECT_1:def 2 v + w = w + v
reconsider v1 = v, w1 = w as Element of (VectQuot (V,(p (*) V))) ;
thus v + w =
v1 + w1
.=
w1 + v1
.=
w + v
; verum