let L be distributive complete LATTICE; :: thesis: ( L opp is meet-continuous implies for p being Element of L st p is completely-irreducible holds
the carrier of L \ (downarrow p) is Open Filter of L )
assume A1: L opp is meet-continuous ; :: thesis: for p being Element of L st p is completely-irreducible holds
the carrier of L \ (downarrow p) is Open Filter of L
let p be Element of L; :: thesis: ( p is completely-irreducible implies the carrier of L \ (downarrow p) is Open Filter of L )
assume A2: p is completely-irreducible ; :: thesis: the carrier of L \ (downarrow p) is Open Filter of L
then consider q being Element of L such that
A3: p < q and
A4: for s being Element of L st p < s holds
q <= s and
uparrow p = {p} \/ (uparrow q) by Th20;
defpred S1[ Element of L] means ( $1 <= q & not $1 <= p );
reconsider F = { t where t is Element of L : S1[t] } as Subset of L from DOMAIN_1:sch 7();
 not q <= p by A3, ORDERS_2:6;
then A5: q in F ;
A6: now :: thesis: for x, y being Element of L st x in F & y in F holds
ex z being Element of the carrier of L st
( z in F & z <= x & z <= y )
let x, y be Element of L; :: thesis: ( x in F & y in F implies ex z being Element of the carrier of L st
( z in F & z <= x & z <= y ) )
assume that
A7: x in F and
A8: y in F ; :: thesis: ex z being Element of the carrier of L st
( z in F & z <= x & z <= y )
A9: ex x1 being Element of L st
( x1 = x & x1 <= q & not x1 <= p ) by A7;
take z = x "/\" y; :: thesis: ( z in F & z <= x & z <= y )
A10: z <= x by YELLOW_0:23;
A11: ex y1 being Element of L st
( y1 = y & y1 <= q & not y1 <= p ) by A8;
A12: not z <= p
proof
A13: now :: thesis: for d being Element of L st d >= y & d >= p holds
q <= d
let d be Element of L; :: thesis: ( d >= y & d >= p implies q <= d )
assume ( d >= y & d >= p ) ; :: thesis: q <= d
then d > p by A11, ORDERS_2:def 6;
hence q <= d by A4; :: thesis: verum
end;
assume A14: z <= p ; :: thesis: contradiction
A15: q >= p by A3, ORDERS_2:def 6;
x = x "/\" q by A9, YELLOW_0:25
.= x "/\" (y "\/" p) by A11, A15, A13, YELLOW_0:22
.= z "\/" (x "/\" p) by WAYBEL_1:def 3
.= (x "\/" z) "/\" (z "\/" p) by WAYBEL_1:5
.= x "/\" (p "\/" z) by A10, YELLOW_0:24
.= x "/\" p by A14, YELLOW_0:24 ;
hence contradiction by A9, YELLOW_0:25; :: thesis: verum
end;
z <= q by A9, A10, ORDERS_2:3;
hence z in F by A12; :: thesis: ( z <= x & z <= y )
thus z <= x by YELLOW_0:23; :: thesis: z <= y
thus z <= y by YELLOW_0:23; :: thesis: verum
end;
p is irreducible by A2, Th23;
then A16: p is prime by WAYBEL_6:27;
not Top L in Irr L by Th21;
then p <> Top L by A2, Def4;
then (downarrow p) ` is Filter of L by A16, WAYBEL_6:26;
then reconsider V = the carrier of L \ (downarrow p) as Filter of L by SUBSET_1:def 4;
reconsider F = F as non empty filtered Subset of L by A5, A6, WAYBEL_0:def 2;
reconsider F1 = F as non empty directed Subset of (L opp) by YELLOW_7:27;
now :: thesis: for x being Element of L st x in V holds
ex y being Element of the carrier of L st
( y in V & y << x )
let x be Element of L; :: thesis: ( x in V implies ex y being Element of the carrier of L st
( y in V & y << x ) )
assume A17: x in V ; :: thesis: ex y being Element of the carrier of L st
( y in V & y << x )
take y = inf F; :: thesis: ( y in V & y << x )
thus y in V :: thesis: y << x
proof
now :: thesis: for r being Element of L st r in {p} "\/" F holds
q <= r
let r be Element of L; :: thesis: ( r in {p} "\/" F implies q <= r )
assume r in {p} "\/" F ; :: thesis: q <= r
then r in { (p "\/" v) where v is Element of L : v in F } by YELLOW_4:15;
then consider v being Element of L such that
A18: r = p "\/" v and
A19: v in F ;
ex v1 being Element of L st
( v = v1 & v1 <= q & not v1 <= p ) by A19;
then A20: p <> r by A18, YELLOW_0:24;
p <= r by A18, YELLOW_0:22;
then p < r by A20, ORDERS_2:def 6;
hence q <= r by A4; :: thesis: verum
end;
then A21: q is_<=_than {p} "\/" F by LATTICE3:def 8;
A22: ex_inf_of {(p ~)} "/\" F1,L by YELLOW_0:17;
ex_inf_of F,L by YELLOW_0:17;
then A23: inf F = sup F1 by YELLOW_7:13;
A24: {(p ~)} = {p} by LATTICE3:def 6;
assume not y in V ; :: thesis: contradiction
then y in downarrow p by XBOOLE_0:def 5;
then y <= p by WAYBEL_0:17;
then p = p "\/" y by YELLOW_0:24
.= (p ~) "/\" ((inf F) ~) by YELLOW_7:23
.= (p ~) "/\" (sup F1) by A23, LATTICE3:def 6
.= sup ({(p ~)} "/\" F1) by A1, WAYBEL_2:def 6
.= "/\" (({(p ~)} "/\" F1),L) by A22, YELLOW_7:13
.= "/\" (({p} "\/" F),L) by A24, Th5 ;
then q <= p by A21, YELLOW_0:33;
hence contradiction by A3, ORDERS_2:6; :: thesis: verum
end;
then not y in downarrow p by XBOOLE_0:def 5;
then A25: not y <= p by WAYBEL_0:17;
now :: thesis: for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & y <= d )
let D be non empty directed Subset of L; :: thesis: ( y <= sup D implies ex d being Element of L st
( d in D & y <= d ) )
assume A26: y <= sup D ; :: thesis: ex d being Element of L st
( d in D & y <= d )
not D \ (downarrow p) is empty then consider d being object such that
A27: d in D \ (downarrow p) ;
reconsider d = d as Element of L by A27;
take d = d; :: thesis: ( d in D & y <= d )
thus d in D by A27, XBOOLE_0:def 5; :: thesis: y <= d
not d in downarrow p by A27, XBOOLE_0:def 5;
then not d <= p by WAYBEL_0:17;
then ( d "/\" q <= q & not d "/\" q <= p ) by A3, A4, Th28, YELLOW_0:23;
then ( y is_<=_than F & d "/\" q in F ) by YELLOW_0:33;
then ( d "/\" q <= d & y <= d "/\" q ) by LATTICE3:def 8, YELLOW_0:23;
hence y <= d by ORDERS_2:3; :: thesis: verum
end;
then A28: y << y by WAYBEL_3:def 1;
not x in downarrow p by A17, XBOOLE_0:def 5;
then not x <= p by WAYBEL_0:17;
then ( x "/\" q <= q & not x "/\" q <= p ) by A3, A4, Th28, YELLOW_0:23;
then ( y is_<=_than F & x "/\" q in F ) by YELLOW_0:33;
then ( x "/\" q <= x & y <= x "/\" q ) by LATTICE3:def 8, YELLOW_0:23;
then y <= x by ORDERS_2:3;
hence y << x by A28, WAYBEL_3:2; :: thesis: verum
end;
hence the carrier of L \ (downarrow p) is Open Filter of L by WAYBEL_6:def 1; :: thesis: verum