let K, L be Field; for w being Element of L st K is Subring of L holds
Ann_Poly (w,K) is quasi-prime
let w be Element of L; ( K is Subring of L implies Ann_Poly (w,K) is quasi-prime )
assume A0:
K is Subring of L
; Ann_Poly (w,K) is quasi-prime
set M = { p where p is Polynomial of K : Ext_eval (p,w) = 0. L } ;
for p, q being Element of (Polynom-Ring K) holds
( not p * q in Ann_Poly (w,K) or p in Ann_Poly (w,K) or q in Ann_Poly (w,K) )
proof
let p,
q be
Element of
(Polynom-Ring K);
( not p * q in Ann_Poly (w,K) or p in Ann_Poly (w,K) or q in Ann_Poly (w,K) )
assume A1:
p * q in Ann_Poly (
w,
K)
;
( p in Ann_Poly (w,K) or q in Ann_Poly (w,K) )
reconsider p1 =
p,
q1 =
q as
Polynomial of
K by POLYNOM3:def 10;
p1 *' q1 in Ann_Poly (
w,
K)
by A1, POLYNOM3:def 10;
then consider t being
Polynomial of
K such that A5:
t = p1 *' q1
and A6:
Ext_eval (
t,
w)
= 0. L
;
(Ext_eval (p1,w)) * (Ext_eval (q1,w)) = 0. L
by A0, Th24, A6, A5;
end;
hence
Ann_Poly (w,K) is quasi-prime
by RING_1:def 1; verum