let A, B be Ring; 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; 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); ( 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)
; 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; verum