let F be Field; for p being non constant Element of the carrier of (Polynom-Ring F) holds { q where q is Polynomial of F : deg q < deg p } is Preserv of poly_mult_mod p
let p be non constant Element of the carrier of (Polynom-Ring F); { q where q is Polynomial of F : deg q < deg p } is Preserv of poly_mult_mod p
set C = { q where q is Polynomial of F : deg q < deg p } ;
then
{ q where q is Polynomial of F : deg q < deg p } c= the carrier of (Polynom-Ring F)
;
then reconsider C = { q where q is Polynomial of F : deg q < deg p } as Subset of the carrier of (Polynom-Ring F) ;
set A = poly_mult_mod p;
now for x being set st x in [:C,C:] holds
(poly_mult_mod p) . x in Clet x be
set ;
( x in [:C,C:] implies (poly_mult_mod p) . x in C )assume
x in [:C,C:]
;
(poly_mult_mod p) . x in Cthen consider a,
b being
object such that A2:
a in C
and A3:
b in C
and A4:
x = [a,b]
by ZFMISC_1:def 2;
consider u being
Polynomial of
F such that A5:
(
a = u &
deg u < deg p )
by A2;
consider v being
Polynomial of
F such that A6:
(
b = v &
deg v < deg p )
by A3;
reconsider a =
a,
b =
b as
Element of
(Polynom-Ring F) by A5, A6, POLYNOM3:def 10;
A8:
deg ((u *' v) mod p) < deg p
by RING_2:29;
(poly_mult_mod p) . x =
(poly_mult_mod p) . (
u,
v)
by A5, A6, A4
.=
(u *' v) mod p
by defpmm
;
hence
(poly_mult_mod p) . x in C
by A8;
verum end;
hence
{ q where q is Polynomial of F : deg q < deg p } is Preserv of poly_mult_mod p
by REALSET1:def 1; verum