let A be Ring; :: thesis: for B being comRing
for w being Element of B
for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (w,A) holds
x * p in Ann_Poly (w,A)
let B be comRing; :: thesis: for w being Element of B
for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (w,A) holds
x * p in Ann_Poly (w,A)
let w be Element of B; :: thesis: for p, x being Element of (Polynom-Ring A) st A is Subring of B & x in Ann_Poly (w,A) holds
x * p in Ann_Poly (w,A)
let p, x be Element of (Polynom-Ring A); :: thesis: ( A is Subring of B & x in Ann_Poly (w,A) implies x * p in Ann_Poly (w,A) )
set M = { p where p is Polynomial of A : Ext_eval (p,w) = 0. B } ;
reconsider p1 = p, x1 = x as Polynomial of A by POLYNOM3:def 10;
assume that
A0: A is Subring of B and
A1: x in Ann_Poly (w,A) ; :: thesis: x * p in Ann_Poly (w,A)
consider x2 being Polynomial of A such that
A2: x2 = x1 and
A3: Ext_eval (x2,w) = 0. B by A1;
Ext_eval ((x1 *' p1),w) = (Ext_eval (p1,w)) * (0. B) by A0, A2, A3, Th24
.= 0. B ;
then consider t being Polynomial of A such that
A4: t = x1 *' p1 and
A5: Ext_eval (t,w) = 0. B ;
x1 *' p1 in { p where p is Polynomial of A : Ext_eval (p,w) = 0. B } by A4, A5;
hence x * p in Ann_Poly (w,A) by POLYNOM3:def 10; :: thesis: verum