let L be complete LATTICE; :: thesis: ( PRIME L is order-generating implies ( L is distributive & L is meet-continuous ) )
set H = { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ;
set p9 = the prime Element of L;
A1: chi (((downarrow the prime Element of L) `), the carrier of L) in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ;
now :: thesis: for x being object st x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } holds
x is Function
let x be object ; :: thesis: ( x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } implies x is Function )
assume x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ; :: thesis: x is Function
then ex p being Element of L st
( x = chi (((downarrow p) `), the carrier of L) & p is prime ) ;
hence x is Function ; :: thesis: verum
end;
then reconsider H = { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } as non empty functional set by A1, FUNCT_1:def 13;
deffunc H1( object ) -> set = { f where f is Element of H : f . $1 = 1 } ;
consider F being Function such that
A2: dom F = the carrier of L and
A3: for x being object st x in the carrier of L holds
F . x = H1(x) from FUNCT_1:sch 3();
 A4: the carrier of (BoolePoset H) = the carrier of (InclPoset (bool H)) by YELLOW_1:4
.= bool H by YELLOW_1:1 ;
rng F c= the carrier of (BoolePoset H)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of (BoolePoset H) )
reconsider yy = y as set by TARSKI:1;
assume y in rng F ; :: thesis: y in the carrier of (BoolePoset H)
then consider x being object such that
A5: ( x in dom F & y = F . x ) by FUNCT_1:def 3;
A6: y = { f where f is Element of H : f . x = 1 } by A2, A3, A5;
yy c= H
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in yy or p in H )
assume p in yy ; :: thesis: p in H
then ex f being Element of H st
( p = f & f . x = 1 ) by A6;
hence p in H ; :: thesis: verum
end;
hence y in the carrier of (BoolePoset H) by A4; :: thesis: verum
end;
then reconsider F = F as Function of L,(BoolePoset H) by A2, FUNCT_2:def 1, RELSET_1:4;
A7: F is meet-preserving
proof
let x, y be Element of L; :: according to WAYBEL_0:def 34 :: thesis: F preserves_inf_of {x,y}
assume ex_inf_of {x,y},L ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of F .: {x,y}, BoolePoset H & "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L)) )
thus ex_inf_of F .: {x,y}, BoolePoset H by YELLOW_0:17; :: thesis: "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L))
A8: { f where f is Element of H : f . (x "/\" y) = 1 } c= { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 }
proof
A9: ( ex_inf_of {x,y},L & x "/\" y = inf {x,y} ) by YELLOW_0:17, YELLOW_0:40;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { f where f is Element of H : f . (x "/\" y) = 1 } or p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } )
A10: 1 = Top (BoolePoset {{}}) by CARD_1:49, YELLOW_1:19;
assume p in { f where f is Element of H : f . (x "/\" y) = 1 } ; :: thesis: p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 }
then consider g being Element of H such that
A11: g = p and
A12: g . (x "/\" y) = 1 ;
g in H ;
then A13: ex a being Element of L st
( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ;
then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31;
g is meet-preserving by A13, Th33;
then A14: g preserves_inf_of {x,y} ;
dom g = the carrier of L by FUNCT_2:def 1;
then A15: {(g . x),(g . y)} = g .: {x,y} by FUNCT_1:60;
(g . x) "/\" (g . y) = inf {(g . x),(g . y)} by YELLOW_0:40;
then A16: g . (x "/\" y) = (g . x) "/\" (g . y) by A15, A14, A9;
then ( g . y <= Top (BoolePoset {{}}) & g . y >= Top (BoolePoset {{}}) ) by A12, A10, YELLOW_0:23, YELLOW_0:45;
then g . y = 1 by A10, ORDERS_2:2;
then A17: p in { f where f is Element of H : f . y = 1 } by A11;
( g . x <= Top (BoolePoset {{}}) & g . x >= Top (BoolePoset {{}}) ) by A12, A10, A16, YELLOW_0:23, YELLOW_0:45;
then g . x = 1 by A10, ORDERS_2:2;
then p in { f where f is Element of H : f . x = 1 } by A11;
hence p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } by A17, XBOOLE_0:def 4; :: thesis: verum
end;
A18: { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } c= { f where f is Element of H : f . (x "/\" y) = 1 }
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } or p in { f where f is Element of H : f . (x "/\" y) = 1 } )
A19: ( ex_inf_of {x,y},L & x "/\" y = inf {x,y} ) by YELLOW_0:17, YELLOW_0:40;
assume A20: p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } ; :: thesis: p in { f where f is Element of H : f . (x "/\" y) = 1 }
then p in { f where f is Element of H : f . x = 1 } by XBOOLE_0:def 4;
then consider f1 being Element of H such that
A21: f1 = p and
A22: f1 . x = 1 ;
p in { f where f is Element of H : f . y = 1 } by A20, XBOOLE_0:def 4;
then A23: ex f2 being Element of H st
( f2 = p & f2 . y = 1 ) ;
f1 in H ;
then consider a being Element of L such that
A24: chi (((downarrow a) `), the carrier of L) = f1 and
A25: a is prime ;
reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A24, Th31;
for x being Element of L holds
( f1 . x = {} iff x <= a ) by A24, Th32;
then f1 is meet-preserving by A25, Th25;
then A26: f1 preserves_inf_of {x,y} ;
dom f1 = the carrier of L by FUNCT_2:def 1;
then A27: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60;
(f1 . x) "/\" (f1 . y) = inf {(f1 . x),(f1 . y)} by YELLOW_0:40;
then f1 . (x "/\" y) = (f1 . x) "/\" (f1 . y) by A27, A26, A19
.= 1 by A21, A22, A23, YELLOW_5:2 ;
hence p in { f where f is Element of H : f . (x "/\" y) = 1 } by A21; :: thesis: verum
end;
F .: {x,y} = {(F . x),(F . y)} by A2, FUNCT_1:60;
hence inf (F .: {x,y}) = (F . x) "/\" (F . y) by YELLOW_0:40
.= (F . x) /\ (F . y) by YELLOW_1:17
.= { f where f is Element of H : f . x = 1 } /\ (F . y) by A3
.= { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } by A3
.= { f where f is Element of H : f . (x "/\" y) = 1 } by A18, A8
.= F . (x "/\" y) by A3
.= F . (inf {x,y}) by YELLOW_0:40 ;
:: thesis: verum
end;
assume A28: PRIME L is order-generating ; :: thesis: ( L is distributive & L is meet-continuous )
A29: F is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 )
assume that
A30: x1 in dom F and
A31: x2 in dom F and
A32: F . x1 = F . x2 ; :: thesis: x1 = x2
reconsider l2 = x2 as Element of L by A31;
reconsider l1 = x1 as Element of L by A30;
now :: thesis: not l1 <> l2
A33: F . l2 = { f where f is Element of H : f . l2 = 1 } by A3;
A34: F . l1 = { f where f is Element of H : f . l1 = 1 } by A3;
assume A35: l1 <> l2 ; :: thesis: contradiction
per cases ( not l1 <= l2 or not l2 <= l1 ) by A35, ORDERS_2:2;
suppose not l1 <= l2 ; :: thesis: contradiction
then consider p being Element of L such that
A36: p in PRIME L and
A37: l2 <= p and
A38: not l1 <= p by A28, Th17;
set CH = chi (((downarrow p) `), the carrier of L);
p is prime by A36, Def7;
then chi (((downarrow p) `), the carrier of L) in H ;
then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ;
A39: now :: thesis: not CH in F . l2
assume CH in F . l2 ; :: thesis: contradiction
then ex f being Element of H st
( f = CH & f . l2 = 1 ) by A33;
hence contradiction by A37, Th32; :: thesis: verum
end;
dom CH = the carrier of L by FUNCT_2:def 1;
then ( rng CH c= {0,1} & CH . l1 in rng CH ) by FUNCT_1:def 3, RELAT_1:def 19;
then ( CH . l1 = 0 or CH . l1 = 1 ) by TARSKI:def 2;
hence contradiction by A32, A34, A38, A39, Th32; :: thesis: verum
end;
suppose not l2 <= l1 ; :: thesis: contradiction
then consider p being Element of L such that
A40: p in PRIME L and
A41: l1 <= p and
A42: not l2 <= p by A28, Th17;
set CH = chi (((downarrow p) `), the carrier of L);
p is prime by A40, Def7;
then chi (((downarrow p) `), the carrier of L) in H ;
then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ;
A43: now :: thesis: not CH in F . l1
assume CH in F . l1 ; :: thesis: contradiction
then ex f being Element of H st
( f = CH & f . l1 = 1 ) by A34;
hence contradiction by A41, Th32; :: thesis: verum
end;
dom CH = the carrier of L by FUNCT_2:def 1;
then ( rng CH c= {0,1} & CH . l2 in rng CH ) by FUNCT_1:def 3, RELAT_1:def 19;
then ( CH . l2 = 0 or CH . l2 = 1 ) by TARSKI:def 2;
hence contradiction by A32, A33, A42, A43, Th32; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
F is join-preserving
proof
let x, y be Element of L; :: according to WAYBEL_0:def 35 :: thesis: F preserves_sup_of {x,y}
assume ex_sup_of {x,y},L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of F .: {x,y}, BoolePoset H & "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L)) )
thus ex_sup_of F .: {x,y}, BoolePoset H by YELLOW_0:17; :: thesis: "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L))
A44: { f where f is Element of H : f . (x "\/" y) = 1 } c= { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 }
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { f where f is Element of H : f . (x "\/" y) = 1 } or p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } )
A45: 1 = Top (BoolePoset {{}}) by CARD_1:49, YELLOW_1:19;
assume p in { f where f is Element of H : f . (x "\/" y) = 1 } ; :: thesis: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 }
then consider g being Element of H such that
A46: g = p and
A47: g . (x "\/" y) = 1 ;
g in H ;
then A48: ex a being Element of L st
( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ;
then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31;
g is join-preserving by A48, Th33;
then A49: g preserves_sup_of {x,y} ;
dom g = the carrier of L by FUNCT_2:def 1;
then A50: g .: {x,y} = {(g . x),(g . y)} by FUNCT_1:60;
A51: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41;
A52: (g . x) "\/" (g . y) = sup {(g . x),(g . y)} by YELLOW_0:41;
A53: now :: thesis: ( g . x = {} implies not g . y = {} )
assume ( g . x = {} & g . y = {} ) ; :: thesis: contradiction
then (g . x) "\/" (g . y) = {} \/ {} by YELLOW_1:17
.= 0 ;
hence contradiction by A47, A50, A49, A51, A52; :: thesis: verum
end;
A54: the carrier of (BoolePoset {{}}) = the carrier of (InclPoset (bool {{}})) by YELLOW_1:4
.= bool {{}} by YELLOW_1:1
.= {{},{{}}} by ZFMISC_1:24 ;
then A55: ( g . y = {} or g . y = {{}} ) by TARSKI:def 2;
( g . x = {} or g . x = {{}} ) by A54, TARSKI:def 2;
then ( g . x = Top (BoolePoset {{}}) or g . y = Top (BoolePoset {{}}) ) by A55, A53, YELLOW_1:19;
then ( p in { f where f is Element of H : f . x = 1 } or p in { f where f is Element of H : f . y = 1 } ) by A46, A45;
hence p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } by XBOOLE_0:def 3; :: thesis: verum
end;
A56: { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } c= { f where f is Element of H : f . (x "\/" y) = 1 }
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } or p in { f where f is Element of H : f . (x "\/" y) = 1 } )
assume A57: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } ; :: thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }
per cases ( p in { f where f is Element of H : f . x = 1 } or p in { f where f is Element of H : f . y = 1 } ) by A57, XBOOLE_0:def 3;
suppose p in { f where f is Element of H : f . x = 1 } ; :: thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }
then consider f1 being Element of H such that
A58: f1 = p and
A59: f1 . x = 1 ;
f1 in H ;
then consider a being Element of L such that
A60: chi (((downarrow a) `), the carrier of L) = f1 and
A61: a is prime ;
reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A60, Th31;
for x being Element of L holds
( f1 . x = {} iff x <= a ) by A60, Th32;
then f1 is join-preserving by A61, Th25;
then A62: f1 preserves_sup_of {x,y} ;
dom f1 = the carrier of L by FUNCT_2:def 1;
then A63: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60;
A64: ( 1 = Top (BoolePoset {{}}) & f1 . y <= Top (BoolePoset {{}}) ) by CARD_1:49, YELLOW_0:45, YELLOW_1:19;
A65: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41;
(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41;
then f1 . (x "\/" y) = (f1 . x) "\/" (f1 . y) by A63, A62, A65
.= 1 by A59, A64, YELLOW_0:24 ;
hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A58; :: thesis: verum
end;
suppose p in { f where f is Element of H : f . y = 1 } ; :: thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }
then consider f1 being Element of H such that
A66: f1 = p and
A67: f1 . y = 1 ;
f1 in H ;
then consider b being Element of L such that
A68: chi (((downarrow b) `), the carrier of L) = f1 and
A69: b is prime ;
reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A68, Th31;
for x being Element of L holds
( f1 . x = {} iff x <= b ) by A68, Th32;
then f1 is join-preserving by A69, Th25;
then A70: f1 preserves_sup_of {x,y} ;
dom f1 = the carrier of L by FUNCT_2:def 1;
then A71: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60;
A72: ( 1 = Top (BoolePoset {{}}) & f1 . x <= Top (BoolePoset {{}}) ) by CARD_1:49, YELLOW_0:45, YELLOW_1:19;
A73: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41;
(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41;
then f1 . (x "\/" y) = (f1 . y) "\/" (f1 . x) by A71, A70, A73
.= 1 by A67, A72, YELLOW_0:24 ;
hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A66; :: thesis: verum
end;
end;
end;
F .: {x,y} = {(F . x),(F . y)} by A2, FUNCT_1:60;
hence sup (F .: {x,y}) = (F . x) "\/" (F . y) by YELLOW_0:41
.= (F . x) \/ (F . y) by YELLOW_1:17
.= { f where f is Element of H : f . x = 1 } \/ (F . y) by A3
.= { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } by A3
.= { f where f is Element of H : f . (x "\/" y) = 1 } by A56, A44
.= F . (x "\/" y) by A3
.= F . (sup {x,y}) by YELLOW_0:41 ;
:: thesis: verum
end;
hence L is distributive by A7, A29, Th3; :: thesis: L is meet-continuous
F is sups-preserving
proof
let X be Subset of L; :: according to WAYBEL_0:def 33 :: thesis: F preserves_sup_of X
F preserves_sup_of X
proof
assume ex_sup_of X,L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of F .: X, BoolePoset H & "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L)) )
thus ex_sup_of F .: X, BoolePoset H by YELLOW_0:17; :: thesis: "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L))
A74: F . (sup X) = { g where g is Element of H : g . (sup X) = 1 } by A3;
A75: sup (F .: X) c= F . (sup X)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in sup (F .: X) or a in F . (sup X) )
assume a in sup (F .: X) ; :: thesis: a in F . (sup X)
then a in union (F .: X) by YELLOW_1:21;
then consider Y being set such that
A76: a in Y and
A77: Y in F .: X by TARSKI:def 4;
consider z being object such that
A78: z in dom F and
A79: z in X and
A80: Y = F . z by A77, FUNCT_1:def 6;
reconsider z = z as Element of L by A78;
F . z = { f where f is Element of H : f . z = 1 } by A3;
then consider f being Element of H such that
A81: a = f and
A82: f . z = 1 by A76, A80;
f in H ;
then consider p being Element of L such that
A83: f = chi (((downarrow p) `), the carrier of L) and
p is prime ;
dom f = the carrier of L by A83, FUNCT_2:def 1;
then A86: f . (sup X) in rng f by FUNCT_1:def 3;
rng f c= {0,1} by A83, RELAT_1:def 19;
then ( f . (sup X) = 0 or f . (sup X) = 1 ) by A86, TARSKI:def 2;
hence a in F . (sup X) by A74, A81, A84; :: thesis: verum
end;
F . (sup X) c= sup (F .: X)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in F . (sup X) or a in sup (F .: X) )
assume a in F . (sup X) ; :: thesis: a in sup (F .: X)
then consider f being Element of H such that
A87: a = f and
A88: f . (sup X) = 1 by A74;
f in H ;
then consider p being Element of L such that
A89: f = chi (((downarrow p) `), the carrier of L) and
p is prime ;
A90: rng f c= {0,1} by A89, RELAT_1:def 19;
A91: not sup X <= p by A88, A89, Th32;
now :: thesis: ex l being Element of L st
( l in X & not l <= p )
assume for l being Element of L st l in X holds
l <= p ; :: thesis: contradiction
then X is_<=_than p ;
hence contradiction by A91, YELLOW_0:32; :: thesis: verum
end;
then consider l being Element of L such that
A92: l in X and
A93: not l <= p ;
dom f = the carrier of L by A89, FUNCT_2:def 1;
then f . l in rng f by FUNCT_1:def 3;
then ( f . l = 0 or f . l = 1 ) by A90, TARSKI:def 2;
then f in { g where g is Element of H : g . l = 1 } by A89, A93, Th32;
then A94: f in F . l by A3;
F . l in F .: X by A2, A92, FUNCT_1:def 6;
then a in union (F .: X) by A87, A94, TARSKI:def 4;
hence a in sup (F .: X) by YELLOW_1:21; :: thesis: verum
end;
hence "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L)) by A75; :: thesis: verum
end;
hence F preserves_sup_of X ; :: thesis: verum
end;
hence L is meet-continuous by A7, A29, Th4; :: thesis: verum