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 :: thesis: ( 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); :: according to VECTSP_1:def 14 :: thesis: for b₁ being Element of the carrier of (Z_MQ_VectSp (V,p)) holds (x + y) * b₁ = (x * b₁) + (y * b₁)
let v be Element of (Z_MQ_VectSp (V,p)); :: thesis: (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 NAT_D:66 ;
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; :: thesis: verum

end;

thus Z_MQ_VectSp (V,p) is vector-distributive :: thesis: ( 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); :: according to VECTSP_1:def 13 :: thesis: for b₁, b₂ being Element of the carrier of (Z_MQ_VectSp (V,p)) holds x * (b₁ + b₂) = (x * b₁) + (x * b₂)
let v, w be Element of (Z_MQ_VectSp (V,p)); :: thesis: 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 ; :: thesis: verum

end;

thus Z_MQ_VectSp (V,p) is scalar-associative :: thesis: ( 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); :: according to VECTSP_1:def 15 :: thesis: for b₁ being Element of the carrier of (Z_MQ_VectSp (V,p)) holds (x * y) * b₁ = x * (y * b₁)
let v be Element of (Z_MQ_VectSp (V,p)); :: thesis: (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; :: thesis: verum

end;

thus Z_MQ_VectSp (V,p) is scalar-unital :: thesis: ( 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 v be Element of (Z_MQ_VectSp (V,p)); :: according to VECTSP_1:def 16 :: thesis: (1. (GF p)) * v = v
reconsider v1 = v as Element of (VectQuot (V,(p (*) V))) ;
consider i being Nat such that
A13: 1. (GF p) = i mod p by EC_PF_1:13;
reconsider i = i as Element of INT.Ring by Lem1;
thus (1. (GF p)) * v = (i mod p) * v1 by Def11, A13
.= (1. INT.Ring) * v1 by A13, EC_PF_1:12
.= v ; :: thesis: verum

end;

thus Z_MQ_VectSp (V,p) is add-associative :: thesis: ( 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 u, v, w be Element of (Z_MQ_VectSp (V,p)); :: according to RLVECT_1:def 3 :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as Element of (VectQuot (V,(p (*) V))) ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum

end;

thus Z_MQ_VectSp (V,p) is right_zeroed :: thesis: ( Z_MQ_VectSp (V,p) is right_complementable & Z_MQ_VectSp (V,p) is Abelian )

proof

let u be Element of (Z_MQ_VectSp (V,p)); :: according to RLVECT_1:def 4 :: thesis: u + (0. (Z_MQ_VectSp (V,p))) = u
reconsider u1 = u as Element of (VectQuot (V,(p (*) V))) ;
thus u + (0. (Z_MQ_VectSp (V,p))) = u1 + (0. (VectQuot (V,(p (*) V))))
.= u by RLVECT_1:def 4 ; :: thesis: verum

end;

thus Z_MQ_VectSp (V,p) is right_complementable :: thesis: Z_MQ_VectSp (V,p) is Abelian

proof

let v be Element of (Z_MQ_VectSp (V,p)); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v1 = v as Element of (VectQuot (V,(p (*) V))) ;
reconsider w = - v1 as Element of (Z_MQ_VectSp (V,p)) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. (Z_MQ_VectSp (V,p))
thus v + w = v1 + (- v1)
.= 0. (VectQuot (V,(p (*) V))) by RLVECT_1:5
.= 0. (Z_MQ_VectSp (V,p)) ; :: thesis: verum

end;

let v, w be Element of (Z_MQ_VectSp (V,p)); :: according to RLVECT_1:def 2 :: thesis: 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 ; :: thesis: verum