let R be domRing; for n being non empty Ordinal
for a being Function of n,R holds Zero_ (polyset a) = {a}
let n be non empty Ordinal; for a being Function of n,R holds Zero_ (polyset a) = {a}
let a be Function of n,R; Zero_ (polyset a) = {a}
thus
for o being object st o in Zero_ (polyset a) holds
o in {a}
TARSKI:def 3,XBOOLE_0:def 10 {a} c= Zero_ (polyset a)proof
let o be
object ;
( o in Zero_ (polyset a) implies o in {a} )
assume A2:
o in Zero_ (polyset a)
;
o in {a}
then consider x being
Function such that A4:
(
o = x &
dom x = n &
rng x c= [#] R )
by FUNCT_2:def 2;
assume A3:
not
o in {a}
;
contradiction
reconsider x =
x as
Function of
n,
R by A4, FUNCT_2:2;
A5:
dom a =
n
by FUNCT_2:def 1
.=
dom x
by FUNCT_2:def 1
;
x <> a
by A4, A3, TARSKI:def 1;
then consider i being
object such that A6:
(
i in dom a &
x . i <> a . i )
by A5;
reconsider i0 =
i as
Element of
n by A6;
reconsider f0 =
deg1Poly (
a,
i0) as
Polynomial of
n,
R ;
A7:
f0 in polyset a
;
A8:
eval (
f0,
x) =
(eval ((1_1 (i0,R)),x)) - (eval (((a . i0) | (n,R)),x))
by POLYNOM2:24
.=
(x . i0) - (eval (((a . i0) | (n,R)),x))
by HILB10_3:1
.=
(x . i0) - (a . i0)
by POLYNOM7:25
;
not
x in Zero_ (polyset a)
proof
assume
x in Zero_ (polyset a)
;
contradiction
then
x in { x where x is Function of n,R : for p being Polynomial of n,R st p in polyset a holds
eval (p,x) = 0. R }
by Def6;
then consider x0 being
Function of
n,
R such that A10:
(
x0 = x & ( for
f being
Polynomial of
n,
R st
f in polyset a holds
eval (
f,
x0)
= 0. R ) )
;
thus
contradiction
by RLVECT_1:21, A6, A8, A7, A10;
verum
end;
hence
contradiction
by A2, A4;
verum
end;
thus
for o being object st o in {a} holds
o in Zero_ (polyset a)
TARSKI:def 3 verumproof
let o be
object ;
( o in {a} implies o in Zero_ (polyset a) )
assume
o in {a}
;
o in Zero_ (polyset a)
then A12:
o = a
by TARSKI:def 1;
for
f being
Polynomial of
n,
R st
f in polyset a holds
eval (
f,
a)
= 0. R
proof
let f be
Polynomial of
n,
R;
( f in polyset a implies eval (f,a) = 0. R )
assume
f in polyset a
;
eval (f,a) = 0. R
then consider f0 being
Polynomial of
n,
R such that A14:
(
f0 = f & ex
i being
Element of
n st
f0 = deg1Poly (
a,
i) )
;
consider i0 being
Element of
n such that A15:
f0 = deg1Poly (
a,
i0)
by A14;
eval (
f0,
a) =
(eval ((1_1 (i0,R)),a)) - (eval (((a . i0) | (n,R)),a))
by A15, POLYNOM2:24
.=
(a . i0) - (eval (((a . i0) | (n,R)),a))
by HILB10_3:1
.=
(a . i0) - (a . i0)
by POLYNOM7:25
.=
0. R
by RLVECT_1:15
;
hence
eval (
f,
a)
= 0. R
by A14;
verum
end;
then
a in { x where x is Function of n,R : for f being Polynomial of n,R st f in polyset a holds
eval (f,x) = 0. R }
;
hence
o in Zero_ (polyset a)
by A12, Def6;
verum
end;