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;
H1:
0. (Polynom-Ring p) = 0_. F
by defprfp;
now for x, y being Element of (Polynom-Ring p) holds x + y = y + xlet x,
y be
Element of
(Polynom-Ring p);
x + y = y + 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 )
;
reconsider q =
q,
r =
r as
Element of
(Polynom-Ring F) by POLYNOM3:def 10;
A3:
(
[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,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 + y =
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
x,
y)
by H0, defprfp
.=
q + r
by A1, A2, A3, FUNCT_1:49
.=
the
addF of
(Polynom-Ring F) . (
y,
x)
by A1, A2, ALGSTR_0:def 1
.=
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
y,
x)
by A3, FUNCT_1:49
.=
y + x
by H0, defprfp
;
verum end;
hence
Polynom-Ring p is Abelian
by RLVECT_1:def 2; ( Polynom-Ring p is add-associative & Polynom-Ring p is right_zeroed & Polynom-Ring p is right_complementable )
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;
reconsider q =
q,
r =
r,
u =
u as
Element of
(Polynom-Ring F) by POLYNOM3:def 10;
A4:
x + y =
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
x,
y)
by H0, defprfp
.=
q + r
by A1, A2, A3a, FUNCT_1:49
;
A5:
y + z =
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
y,
z)
by H0, defprfp
.=
r + u
by A3, A2, A3a, FUNCT_1:49
;
A6:
(x + y) + z =
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
(x + y),
z)
by H0, defprfp
.=
(q + r) + u
by A3, A4, A3b, FUNCT_1:49
.=
q + (r + u)
by RLVECT_1:def 3
;
thus x + (y + z) =
( the addF of (Polynom-Ring F) || { q where q is Polynomial of F : deg q < deg p } ) . (
x,
(y + z))
by H0, defprfp
.=
(x + y) + z
by A6, A5, A1, A3b, FUNCT_1:49
;
verum end;
hence
Polynom-Ring p is add-associative
by RLVECT_1:def 3; ( Polynom-Ring p is right_zeroed & Polynom-Ring p is right_complementable )
hence
Polynom-Ring p is right_zeroed
by RLVECT_1:def 4; Polynom-Ring p is right_complementable
hence
Polynom-Ring p is right_complementable
; verum