let R be domRing; for n being non empty Ordinal
for I, J being Ideal of (Polynom-Ring (n,R)) holds Zero_ (I /\ J) = (Zero_ I) \/ (Zero_ J)
let n be non empty Ordinal; for I, J being Ideal of (Polynom-Ring (n,R)) holds Zero_ (I /\ J) = (Zero_ I) \/ (Zero_ J)
let I, J be Ideal of (Polynom-Ring (n,R)); Zero_ (I /\ J) = (Zero_ I) \/ (Zero_ J)
A1:
( Zero_ I c= Zero_ (I /\ J) & Zero_ J c= Zero_ (I /\ J) )
by Th16, XBOOLE_1:17;
for o being object st o in Zero_ (I /\ J) holds
o in (Zero_ I) \/ (Zero_ J)
proof
let o be
object ;
( o in Zero_ (I /\ J) implies o in (Zero_ I) \/ (Zero_ J) )
assume
o in Zero_ (I /\ J)
;
o in (Zero_ I) \/ (Zero_ J)
then
o in { x where x is Function of n,R : for p being Polynomial of n,R st p in I /\ J holds
eval (p,x) = 0. R }
by Def6;
then consider x1 being
Function of
n,
R such that A3:
(
o = x1 & ( for
p being
Polynomial of
n,
R st
p in I /\ J holds
eval (
p,
x1)
= 0. R ) )
;
x1 in (Zero_ I) \/ (Zero_ J)
proof
assume
not
x1 in (Zero_ I) \/ (Zero_ J)
;
contradiction
then A5:
( not
x1 in Zero_ I & not
x1 in Zero_ J )
by XBOOLE_0:def 3;
not
x1 in { z where z is Function of n,R : for f being Polynomial of n,R st f in I holds
eval (f,z) = 0. R }
by A5, Def6;
then consider f1 being
Polynomial of
n,
R such that A6:
(
f1 in I &
eval (
f1,
x1)
<> 0. R )
;
not
x1 in { z where z is Function of n,R : for f being Polynomial of n,R st f in J holds
eval (f,z) = 0. R }
by A5, Def6;
then consider f2 being
Polynomial of
n,
R such that A7:
(
f2 in J &
eval (
f2,
x1)
<> 0. R )
;
A8:
eval (
(f1 *' f2),
x1)
= (eval (f1,x1)) * (eval (f2,x1))
by POLYNOM2:25;
reconsider F1 =
f1,
F2 =
f2 as
Element of
(Polynom-Ring (n,R)) by POLYNOM1:def 11;
A9:
F1 * F2 = f1 *' f2
by POLYNOM1:def 11;
A10:
(
F1 * F2 in I &
F1 * F2 in J )
by A6, A7, IDEAL_1:def 2;
f1 *' f2 in I /\ J
by A9, A10;
hence
contradiction
by A3, A8, A6, A7, VECTSP_2:def 1;
verum
end;
hence
o in (Zero_ I) \/ (Zero_ J)
by A3;
verum
end;
then
Zero_ (I /\ J) c= (Zero_ I) \/ (Zero_ J)
;
hence
Zero_ (I /\ J) = (Zero_ I) \/ (Zero_ J)
by A1, XBOOLE_1:8; verum