let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds ker (poly_mod p) = {p} -Ideal
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ker (poly_mod p) = {p} -Ideal
set R = Polynom-Ring F;
set S = Polynom-Ring p;
set f = poly_mod p;
reconsider p1 = p as Element of (Polynom-Ring F) ;

A: now :: thesis: for x being object st x in ker (poly_mod p) holds
x in {p} -Ideal

let x be object ; :: thesis: ( x in ker (poly_mod p) implies x in {p} -Ideal )
assume A0: x in ker (poly_mod p) ; :: thesis: x in {p} -Ideal
then x in { v where v is Element of (Polynom-Ring F) : (poly_mod p) . v = 0. (Polynom-Ring p) } by VECTSP10:def 9;
then consider y being Element of (Polynom-Ring F) such that
A1: ( y = x & (poly_mod p) . y = 0. (Polynom-Ring p) ) ;
reconsider q = x as Element of the carrier of (Polynom-Ring F) by A0;
reconsider q1 = x as Element of (Polynom-Ring F) by A0;
A2: q - ((q div p) *' p) = q mod p
.= 0. (Polynom-Ring p) by A1, dpm
.= 0_. F by defprfp ;
reconsider qp = q div p as Element of (Polynom-Ring F) by POLYNOM3:def 10;
qp * p1 = (q div p) *' p by POLYNOM3:def 10;
then A3: - (qp * p1) = - ((q div p) *' p) by lemminuspoly;
q1 - (qp * p1) = q + (- ((q div p) *' p)) by A3, POLYNOM3:def 10
.= 0. (Polynom-Ring F) by A2, POLYNOM3:def 10 ;
then qp * p1 = q1 by RLVECT_1:21;
then q in { (p * r) where r is Element of (Polynom-Ring F) : verum } ;
hence x in {p} -Ideal by IDEAL_1:64; :: thesis: verum

end;

now :: thesis: for x being object st x in {p} -Ideal holds
x in ker (poly_mod p)

let x be object ; :: thesis: ( x in {p} -Ideal implies x in ker (poly_mod p) )
assume x in {p} -Ideal ; :: thesis: x in ker (poly_mod p)
then x in { (p * r) where r is Element of (Polynom-Ring F) : verum } by IDEAL_1:64;
then consider y being Element of (Polynom-Ring F) such that
A1: x = p * y ;
reconsider q = y as Element of the carrier of (Polynom-Ring F) ;
p * y = p *' q by POLYNOM3:def 10;
then (poly_mod p) . x = (p *' q) mod p by A1, dpm
.= 0_. F by T2, div2
.= 0. (Polynom-Ring p) by defprfp ;
then x in { v where v is Element of (Polynom-Ring F) : (poly_mod p) . v = 0. (Polynom-Ring p) } by A1;
hence x in ker (poly_mod p) by VECTSP10:def 9; :: thesis: verum

end;

hence ker (poly_mod p) = {p} -Ideal by A, TARSKI:2; :: thesis: verum