let K be Field; for f, g being Element of (Polynom-Ring K) st f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal holds
{f,g} -Ideal = the carrier of (Polynom-Ring K)
let f, g be Element of (Polynom-Ring K); ( f <> 0. (Polynom-Ring K) & {f} -Ideal is prime & not g in {f} -Ideal implies {f,g} -Ideal = the carrier of (Polynom-Ring K) )
assume that
A1:
f <> 0. (Polynom-Ring K)
and
A2:
{f} -Ideal is prime
and
A4:
not g in {f} -Ideal
; {f,g} -Ideal = the carrier of (Polynom-Ring K)
assume A5:
{f,g} -Ideal <> the carrier of (Polynom-Ring K)
; contradiction
Polynom-Ring K is PID
;
then consider h being Element of (Polynom-Ring K) such that
A7:
{f,g} -Ideal = {h} -Ideal
by IDEAL_1:def 27;
A8:
( {f} -Ideal c= {h} -Ideal & {g} -Ideal c= {h} -Ideal )
by A7, IDEAL_1:69;
consider s being Element of (Polynom-Ring K) such that
A9:
f = h * s
by RING_2:19, A8, GCD_1:def 1;
consider t being Element of (Polynom-Ring K) such that
A11:
g = h * t
by RING_2:19, A8, GCD_1:def 1;
f is non zero Element of (Polynom-Ring K)
by A1, STRUCT_0:def 12;
then A13:
f is prime
by A2, RING_2:24;