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