let R be domRing; :: thesis: for n being non empty Ordinal
for F being non empty Subset of (Ideals (Polynom-Ring (n,R))) holds Zero_ (union F) = meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F }
let n be non empty Ordinal; :: thesis: for F being non empty Subset of (Ideals (Polynom-Ring (n,R))) holds Zero_ (union F) = meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F }
let F be non empty Subset of (Ideals (Polynom-Ring (n,R))); :: thesis: Zero_ (union F) = meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F }
set PR = Polynom-Ring (n,R);
set M = { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } ;
consider I being object such that
A1: I in F by XBOOLE_0:def 1;
I in Ideals (Polynom-Ring (n,R)) by A1;
then I in { J where J is Ideal of (Polynom-Ring (n,R)) : verum } by RING_2:def 3;
then consider I1 being Ideal of (Polynom-Ring (n,R)) such that
A2: I = I1 ;
Zero_ I1 in { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } by A1, A2;
then A3: { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } <> {} by XBOOLE_0:def 1;
A4: for o being object st o in Zero_ (union F) holds
o in meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F }

proof

let o be object ; :: thesis: ( o in Zero_ (union F) implies o in meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } )
assume o in Zero_ (union F) ; :: thesis: o in meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F }
then o in { x where x is Function of n,R : for p being Polynomial of n,R st p in union F holds
eval (p,x) = 0. R } by Def6;
then consider x being Function of n,R such that
A6: ( x = o & ( for p being Polynomial of n,R st p in union F holds
eval (p,x) = 0. R ) ) ;
for Z being set st Z in { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } holds
o in Z

proof

let Z be set ; :: thesis: ( Z in { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } implies o in Z )
assume Z in { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } ; :: thesis: o in Z
then consider I being Ideal of (Polynom-Ring (n,R)) such that
A8: ( Z = Zero_ I & I in F ) ;
A9: I c= union F by A8, ZFMISC_1:74;
for p1 being Polynomial of n,R st p1 in I holds
eval (p1,x) = 0. R by A6, A9;
then x in { x where x is Function of n,R : for p being Polynomial of n,R st p in I holds
eval (p,x) = 0. R } ;
hence o in Z by A8, A6, Def6; :: thesis: verum

end;

hence o in meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } by A3, SETFAM_1:def 1; :: thesis: verum

end;

for o being object st o in meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } holds
o in Zero_ (union F)

proof

let o be object ; :: thesis: ( o in meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } implies o in Zero_ (union F) )
assume A10: o in meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } ; :: thesis: o in Zero_ (union F)
Zero_ I1 in { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } by A1, A2;
then A11: meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } c= Zero_ I1 by SETFAM_1:3;
A12: meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } c= Funcs (n,([#] R)) by A11, XBOOLE_1:1;
consider x being Function such that
A13: ( o = x & dom x = n & rng x c= [#] R ) by A10, A12, FUNCT_2:def 2;
reconsider x = x as Function of n,R by A13, FUNCT_2:2;
for p being Polynomial of n,R st p in union F holds
eval (p,x) = 0. R

proof

let p be Polynomial of n,R; :: thesis: ( p in union F implies eval (p,x) = 0. R )
assume p in union F ; :: thesis: eval (p,x) = 0. R
then consider Ip being set such that
A15: ( p in Ip & Ip in F ) by TARSKI:def 4;
Ip in Ideals (Polynom-Ring (n,R)) by A15;
then Ip in { J where J is Ideal of (Polynom-Ring (n,R)) : verum } by RING_2:def 3;
then consider I being Ideal of (Polynom-Ring (n,R)) such that
A16: I = Ip ;
Zero_ I in { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } by A15, A16;
then o in Zero_ I by A3, A10, SETFAM_1:def 1;
then o in { x where x is Function of n,R : for p being Polynomial of n,R st p in I holds
eval (p,x) = 0. R } by Def6;
then consider y being Function of n,R such that
A17: ( y = o & ( for f being Polynomial of n,R st f in I holds
eval (f,y) = 0. R ) ) ;
thus eval (p,x) = 0. R by A17, A15, A16, A13; :: thesis: verum

end;

then x in { x where x is Function of n,R : for p being Polynomial of n,R st p in union F holds
eval (p,x) = 0. R } ;
hence o in Zero_ (union F) by A13, Def6; :: thesis: verum

end;

hence Zero_ (union F) = meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F } by TARSKI:2, A4; :: thesis: verum