set M = Z_MQ_VectSp (V,p);
set F = GF p;
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 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)); :: 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
.= ((i mod p) + (j mod p)) mod p by EULER_2:6 ;
A4: x * v = (i mod p) * v1 by ;
A5: y * v = (j mod p) * v1 by ;
(((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 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)); :: 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 ;
thus x * (v + w) = (i mod p) * (v1 + w1) by
.= ((i mod p) * v1) + ((i mod p) * w1) by VECTSP_1:def 14
.= (x * v) + (x * w) by ; :: 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 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)); :: 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 ;
A11: y * v = (j mod p) * v1 by ;
A12: x * (y * v) = (i mod p) * ((j mod p) * v1) by ;
((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 ; :: 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
.= () * v1 by
.= v by VECTSP_1:def 17 ; :: 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:
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