let L be distributive Lattice; for I being Ideal of L
for F being Filter of L st I misses F holds
ex P being Ideal of L st
( P is prime & I c= P & P misses F )
let I be Ideal of L; for F being Filter of L st I misses F holds
ex P being Ideal of L st
( P is prime & I c= P & P misses F )
let F be Filter of L; ( I misses F implies ex P being Ideal of L st
( P is prime & I c= P & P misses F ) )
assume A1:
I misses F
; ex P being Ideal of L st
( P is prime & I c= P & P misses F )
set X = { i where i is Ideal of L : ( I c= i & i misses F ) } ;
z1:
I in { i where i is Ideal of L : ( I c= i & i misses F ) }
by A1;
for Z being set st Z <> {} & Z c= { i where i is Ideal of L : ( I c= i & i misses F ) } & Z is c=-linear holds
union Z in { i where i is Ideal of L : ( I c= i & i misses F ) }
then consider Y being set such that
J0:
( Y in { i where i is Ideal of L : ( I c= i & i misses F ) } & ( for Z being set st Z in { i where i is Ideal of L : ( I c= i & i misses F ) } & Z <> Y holds
not Y c= Z ) )
by ORDERS_1:67, z1;
consider i being Ideal of L such that
KK:
( Y = i & I c= i & i misses F )
by J0;
take
i
; ( i is prime & I c= i & i misses F )
i is prime
proof
assume
not
i is
prime
;
contradiction
then consider a,
b being
Element of
L such that G3:
(
a "/\" b in i & not
a in i & not
b in i )
by Lem2;
set Ia =
i "\/" (.a.>;
i c= i "\/" (.a.>
by FILTER_2:50;
then J1:
I c= i "\/" (.a.>
by KK;
i "\/" (.a.> meets F
then consider p1 being
object such that HH:
(
p1 in i "\/" (.a.> &
p1 in F )
by XBOOLE_0:3;
reconsider p1 =
p1 as
Element of
L by HH;
consider p,
q being
Element of
L such that h1:
(
p1 = p "\/" q &
p in i &
q in (.a.> )
by HH;
p "\/" q [= p "\/" a
by FILTER_0:1, FILTER_2:28, h1;
then
p "\/" a in F
by FILTER_0:9, HH, h1;
then consider p being
Element of
L such that G1:
(
p in i &
p "\/" a in F )
by h1;
set Ib =
i "\/" (.b.>;
i c= i "\/" (.b.>
by FILTER_2:50;
then J1:
I c= i "\/" (.b.>
by KK;
i "\/" (.b.> meets F
then consider p1 being
object such that HH:
(
p1 in i "\/" (.b.> &
p1 in F )
by XBOOLE_0:3;
reconsider p1 =
p1 as
Element of
L by HH;
consider P,
Q being
Element of
L such that h1:
(
p1 = P "\/" Q &
P in i &
Q in (.b.> )
by HH;
P "\/" Q [= P "\/" b
by FILTER_0:1, FILTER_2:28, h1;
then
P "\/" b in F
by FILTER_0:9, HH, h1;
then consider q being
Element of
L such that G2:
(
q in i &
q "\/" b in F )
by h1;
set y =
(p "\/" a) "/\" (q "\/" b);
Z1:
(p "\/" a) "/\" (q "\/" b) in F
by G1, G2, FILTER_0:8;
ZZ:
(p "\/" a) "/\" (q "\/" b) =
((p "\/" a) "/\" q) "\/" ((p "\/" a) "/\" b)
by LATTICES:def 11
.=
((p "/\" q) "\/" (a "/\" q)) "\/" ((p "\/" a) "/\" b)
by LATTICES:def 11
.=
((p "/\" q) "\/" (a "/\" q)) "\/" ((p "/\" b) "\/" (a "/\" b))
by LATTICES:def 11
.=
(((p "/\" q) "\/" (a "/\" q)) "\/" (p "/\" b)) "\/" (a "/\" b)
by LATTICES:def 5
.=
(((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q)) "\/" (a "/\" b)
by LATTICES:def 5
;
set x =
(((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q)) "\/" (a "/\" b);
G4:
p "/\" q in i
by G2, FILTER_2:22;
G5:
p "/\" b in i
by G1, FILTER_2:22;
G6:
a "/\" q in i
by G2, FILTER_2:22;
(p "/\" q) "\/" (p "/\" b) in i
by G4, G5, FILTER_2:21;
then
((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q) in i
by G6, FILTER_2:21;
then
(((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q)) "\/" (a "/\" b) in i
by FILTER_2:21, G3;
hence
contradiction
by KK, XBOOLE_0:3, Z1, ZZ;
verum
end;
hence
( i is prime & I c= i & i misses F )
by KK; verum