let R be domRing; for n being non empty Ordinal
for S being Subset of (Polynom-Ring (n,R)) holds S c= Ideal_ (Zero_ S)
let n be non empty Ordinal; for S being Subset of (Polynom-Ring (n,R)) holds S c= Ideal_ (Zero_ S)
let S be Subset of (Polynom-Ring (n,R)); S c= Ideal_ (Zero_ S)
for o being object st o in S holds
o in Ideal_ (Zero_ S)
proof
let o be
object ;
( o in S implies o in Ideal_ (Zero_ S) )
assume A1:
o in S
;
o in Ideal_ (Zero_ S)
then A2:
S <> {}
by XBOOLE_0:def 1;
reconsider p =
o as
Polynomial of
n,
R by A1, POLYNOM1:def 11;
assume
not
o in Ideal_ (Zero_ S)
;
contradiction
then
not
Zero_ S c= Zero_ p
;
then consider z being
object such that A4:
z in Zero_ S
and A5:
not
z in Zero_ p
;
z in { x where x is Function of n,R : for f being Polynomial of n,R st f in S holds
eval (f,x) = 0. R }
by A2, A4, Def6;
then consider x being
Function of
n,
R such that A6:
x = z
and A7:
for
f being
Polynomial of
n,
R st
f in S holds
eval (
f,
x)
= 0. R
;
eval (
p,
x)
= 0. R
by A1, A7;
hence
contradiction
by A5, A6;
verum
end;
hence
S c= Ideal_ (Zero_ S)
; verum