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 )

reconsider v1 = v, w1 = w as Element of (VectQuot (V,(p (*) V))) ;

thus v + w = v1 + w1

.= w1 + v1

.= w + v ; :: thesis: verum

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

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 )
let x, y be Element of (GF p); :: according to VECTSP_1:def 14 :: thesis: for b_{1} being Element of the carrier of (Z_MQ_VectSp (V,p)) holds (x + y) * b_{1} = (x * b_{1}) + (y * b_{1})

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 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; :: thesis: verum

end;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 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; :: thesis: verum

proof

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 )
let x be Element of (GF p); :: according to VECTSP_1:def 13 :: thesis: for b_{1}, b_{2} being Element of the carrier of (Z_MQ_VectSp (V,p)) holds x * (b_{1} + b_{2}) = (x * b_{1}) + (x * b_{2})

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;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

proof

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 )
let x, y be Element of (GF p); :: according to VECTSP_1:def 15 :: thesis: for b_{1} being Element of the carrier of (Z_MQ_VectSp (V,p)) holds (x * y) * b_{1} = x * (y * b_{1})

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;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

proof

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 )
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 by VECTSP_1:def 17 ; :: thesis: verum

end;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 by VECTSP_1:def 17 ; :: thesis: verum

proof

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 )
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;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

proof

thus
Z_MQ_VectSp (V,p) is right_complementable
:: thesis: Z_MQ_VectSp (V,p) is Abelian
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;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

proof

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

reconsider v1 = v, w1 = w as Element of (VectQuot (V,(p (*) V))) ;

thus v + w = v1 + w1

.= w1 + v1

.= w + v ; :: thesis: verum