set P = Polynom-Ring p;
set C = { q where q is Polynomial of F : deg q < deg p } ;
H0:
{ q where q is Polynomial of F : deg q < deg p } = the carrier of (Polynom-Ring p)
by defprfp;
H2:
1. (Polynom-Ring p) = 1_. F
by defprfp;
reconsider p1 = p as Polynomial of F ;
now for x, y, z being Element of (Polynom-Ring p) holds x * (y * z) = (x * y) * zlet x,
y,
z be
Element of
(Polynom-Ring p);
x * (y * z) = (x * y) * z
x in the
carrier of
(Polynom-Ring p)
;
then
x in { q where q is Polynomial of F : deg q < deg p }
by defprfp;
then consider q being
Polynomial of
F such that A1:
(
x = q &
deg q < deg p )
;
y in the
carrier of
(Polynom-Ring p)
;
then
y in { q where q is Polynomial of F : deg q < deg p }
by defprfp;
then consider r being
Polynomial of
F such that A2:
(
y = r &
deg r < deg p )
;
z in the
carrier of
(Polynom-Ring p)
;
then
z in { q where q is Polynomial of F : deg q < deg p }
by defprfp;
then consider u being
Polynomial of
F such that A3:
(
z = u &
deg u < deg p )
;
A3a:
(
[x,y] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[y,z] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] )
by H0, ZFMISC_1:def 2;
A3b:
(
[(x * y),z] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[x,(y * z)] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] )
by H0, ZFMISC_1:def 2;
A4:
x * y =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
x,
y)
by H0, defprfp
.=
(poly_mult_mod p) . (
x,
y)
by A3a, FUNCT_1:49
.=
(q *' r) mod p1
by A1, A2, defpmm
;
A5:
y * z =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
y,
z)
by H0, defprfp
.=
(poly_mult_mod p) . (
y,
z)
by A3a, FUNCT_1:49
.=
(r *' u) mod p1
by A3, A2, defpmm
;
A6:
(x * y) * z =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
(x * y),
z)
by H0, defprfp
.=
(poly_mult_mod p) . (
(x * y),
z)
by A3b, FUNCT_1:49
.=
(((q *' r) mod p1) *' u) mod p1
by A3, A4, defpmm
.=
((q *' r) *' u) mod p1
by div3
;
thus x * (y * z) =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
x,
(y * z))
by H0, defprfp
.=
(poly_mult_mod p) . (
x,
(y * z))
by A3b, FUNCT_1:49
.=
(((r *' u) mod p1) *' q) mod p1
by A1, A5, defpmm
.=
((r *' u) *' q) mod p1
by div3
.=
(x * y) * z
by A6, POLYNOM3:33
;
verum end;
hence
Polynom-Ring p is associative
by GROUP_1:def 3; ( Polynom-Ring p is well-unital & Polynom-Ring p is distributive )
now for x being Element of (Polynom-Ring p) holds
( x * (1. (Polynom-Ring p)) = x & (1. (Polynom-Ring p)) * x = x )let x be
Element of
(Polynom-Ring p);
( x * (1. (Polynom-Ring p)) = x & (1. (Polynom-Ring p)) * x = x )
x in the
carrier of
(Polynom-Ring p)
;
then
x in { q where q is Polynomial of F : deg q < deg p }
by defprfp;
then consider q being
Polynomial of
F such that A1:
(
x = q &
deg q < deg p )
;
A3a:
(
[x,(1. (Polynom-Ring p))] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[(1. (Polynom-Ring p)),x] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] )
by H0, ZFMISC_1:def 2;
thus x * (1. (Polynom-Ring p)) =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
x,
(1. (Polynom-Ring p)))
by H0, defprfp
.=
(poly_mult_mod p) . (
x,
(1. (Polynom-Ring p)))
by A3a, FUNCT_1:49
.=
(q *' (1_. F)) mod p1
by H2, A1, defpmm
.=
q mod p1
by POLYNOM3:35
.=
x
by A1, div1
;
(1. (Polynom-Ring p)) * x = xthus (1. (Polynom-Ring p)) * x =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
(1. (Polynom-Ring p)),
x)
by H0, defprfp
.=
(poly_mult_mod p) . (
(1. (Polynom-Ring p)),
x)
by A3a, FUNCT_1:49
.=
((1_. F) *' q) mod p1
by H2, A1, defpmm
.=
q mod p1
by POLYNOM3:35
.=
x
by A1, div1
;
verum end;
hence
Polynom-Ring p is well-unital
by VECTSP_1:def 6; Polynom-Ring p is distributive
now for x, y, z being Element of (Polynom-Ring p) holds
( (x * y) + (x * z) = x * (y + z) & (y * x) + (z * x) = (y + z) * x )let x,
y,
z be
Element of
(Polynom-Ring p);
( (x * y) + (x * z) = x * (y + z) & (y * x) + (z * x) = (y + z) * x )
x in the
carrier of
(Polynom-Ring p)
;
then
x in { q where q is Polynomial of F : deg q < deg p }
by defprfp;
then consider q being
Polynomial of
F such that A1:
(
x = q &
deg q < deg p )
;
y in the
carrier of
(Polynom-Ring p)
;
then
y in { q where q is Polynomial of F : deg q < deg p }
by defprfp;
then consider r being
Polynomial of
F such that A2:
(
y = r &
deg r < deg p )
;
z in the
carrier of
(Polynom-Ring p)
;
then
z in { q where q is Polynomial of F : deg q < deg p }
by defprfp;
then consider u being
Polynomial of
F such that A3:
(
z = u &
deg u < deg p )
;
reconsider q1 =
q,
r1 =
r,
u1 =
u as
Element of
(Polynom-Ring F) by POLYNOM3:def 10;
A3a:
(
[x,y] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[x,z] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[y,z] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] )
by H0, ZFMISC_1:def 2;
A3b:
(
[(x * y),(x * z)] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[x,(y * z)] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[x,(y + z)] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] )
by H0, ZFMISC_1:def 2;
A4:
y + z =
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
y,
z)
by H0, defprfp
.=
r1 + u1
by A2, A3, A3a, FUNCT_1:49
.=
r + u
by POLYNOM3:def 10
;
A5:
x * (y + z) =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
x,
(y + z))
by H0, defprfp
.=
(poly_mult_mod p) . (
x,
(y + z))
by A3b, FUNCT_1:49
.=
(q *' (r + u)) mod p1
by A1, A4, defpmm
;
A6:
x * y =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
x,
y)
by H0, defprfp
.=
(poly_mult_mod p) . (
x,
y)
by A3a, FUNCT_1:49
.=
(q *' r) mod p1
by A1, A2, defpmm
;
A7:
x * z =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
x,
z)
by H0, defprfp
.=
(poly_mult_mod p) . (
x,
z)
by A3a, FUNCT_1:49
.=
(q *' u) mod p1
by A1, A3, defpmm
;
reconsider s =
(q *' r) mod p1 as
Element of
(Polynom-Ring F) by POLYNOM3:def 10;
reconsider t =
(q *' u) mod p1 as
Element of
(Polynom-Ring F) by POLYNOM3:def 10;
thus (x * y) + (x * z) =
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
(x * y),
(x * z))
by H0, defprfp
.=
s + t
by A6, A7, A3b, FUNCT_1:49
.=
((q *' r) mod p1) + ((q *' u) mod p1)
by POLYNOM3:def 10
.=
((q *' r) + (q *' u)) mod p1
by div4
.=
x * (y + z)
by A5, POLYNOM3:31
;
(y * x) + (z * x) = (y + z) * xA3a:
(
[y,x] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[z,x] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[y,z] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] )
by H0, ZFMISC_1:def 2;
A3b:
(
[(y * x),(z * x)] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[x,(y * z)] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] &
[(y + z),x] in [: { q where q is Polynomial of F : deg q < deg p } , { q where q is Polynomial of F : deg q < deg p } :] )
by H0, ZFMISC_1:def 2;
A4:
y + z =
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
y,
z)
by H0, defprfp
.=
r1 + u1
by A2, A3, A3a, FUNCT_1:49
.=
r + u
by POLYNOM3:def 10
;
A5:
(y + z) * x =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
(y + z),
x)
by H0, defprfp
.=
(poly_mult_mod p) . (
(y + z),
x)
by A3b, FUNCT_1:49
.=
((r + u) *' q) mod p1
by A1, A4, defpmm
;
A6:
y * x =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
y,
x)
by H0, defprfp
.=
(poly_mult_mod p) . (
y,
x)
by A3a, FUNCT_1:49
.=
(r *' q) mod p1
by A1, A2, defpmm
;
A7:
z * x =
((poly_mult_mod p) || { q where q is Polynomial of F : deg q < deg p } ) . (
z,
x)
by H0, defprfp
.=
(poly_mult_mod p) . (
z,
x)
by A3a, FUNCT_1:49
.=
(u *' q) mod p1
by A1, A3, defpmm
;
reconsider s =
(r *' q) mod p1 as
Element of
(Polynom-Ring F) by POLYNOM3:def 10;
reconsider t =
(u *' q) mod p1 as
Element of
(Polynom-Ring F) by POLYNOM3:def 10;
thus (y * x) + (z * x) =
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
(y * x),
(z * x))
by H0, defprfp
.=
s + t
by A6, A7, A3b, FUNCT_1:49
.=
((q *' r) mod p1) + ((q *' u) mod p1)
by POLYNOM3:def 10
.=
((q *' r) + (q *' u)) mod p1
by div4
.=
(y + z) * x
by A5, POLYNOM3:31
;
verum end;
hence
Polynom-Ring p is distributive
by VECTSP_1:def 7; verum