let A be non degenerated Ring; :: thesis: for B being non degenerated comRing
for w being Element of B st A is Subring of B holds
Ann_Poly (w,A) is proper Ideal of (Polynom-Ring A)
let B be non degenerated comRing; :: thesis: for w being Element of B st A is Subring of B holds
Ann_Poly (w,A) is proper Ideal of (Polynom-Ring A)
let w be Element of B; :: thesis: ( A is Subring of B implies Ann_Poly (w,A) is proper Ideal of (Polynom-Ring A) )
assume A0: A is Subring of B ; :: thesis: Ann_Poly (w,A) is proper Ideal of (Polynom-Ring A)
A1: Ann_Poly (w,A) is add-closed by A0, Lm30;
A2: Ann_Poly (w,A) is left-ideal by A0, Th31;
A3: Ann_Poly (w,A) is right-ideal by A0, Lm32;
Ann_Poly (w,A) is proper

proof

assume not Ann_Poly (w,A) is proper ; :: thesis: contradiction
then A5: 1. (Polynom-Ring A) in Ann_Poly (w,A) ;
A6: 1_. A in Ann_Poly (w,A) by A5, POLYNOM3:37;
A7: Ext_eval ((1_. A),w) = 1. B by A0, Th18;
ex p being Polynomial of A st
( p = 1_. A & Ext_eval (p,w) = 0. B ) by A6;
hence contradiction by A7; :: thesis: verum

end;

hence Ann_Poly (w,A) is proper Ideal of (Polynom-Ring A) by A1, A2, A3; :: thesis: verum