let L be complete LATTICE; :: thesis: ( PRIME L is order-generating implies ( L is distributive & L is meet-continuous ) )
set H = { (chi ((() `), 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 ((() `), the carrier of L)) where p is Element of L : p is prime } ;
now :: thesis: for x being object st x in { (chi ((() `), 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 ((() `), the carrier of L)) where p is Element of L : p is prime } implies x is Function )
assume x in { (chi ((() `), 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 ((() `), the carrier of L) & p is prime ) ;
hence x is Function ; :: thesis: verum
end;
then reconsider H = { (chi ((() `), the carrier of L)) where p is Element of L : p is prime } as non empty functional set by ;
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 A4: the carrier of () = the carrier of (InclPoset (bool H)) by YELLOW_1:4
.= bool H by YELLOW_1:1 ;
rng F c= the carrier of ()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of () )
reconsider yy = y as set by TARSKI:1;
assume y in rng F ; :: thesis: y in the carrier of ()
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 () by A4; :: thesis: verum
end;
then reconsider F = F as Function of L,() by ;
A7: F is meet-preserving
proof
let x, y be Element of L; :: according to WAYBEL_0:def 34 :: thesis:
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}),()) = F . ("/\" ({x,y},L)) )
thus ex_inf_of F .: {x,y}, BoolePoset H by YELLOW_0:17; :: thesis: "/\" ((F .: {x,y}),()) = 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 ;
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 by ;
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 ((() `), the carrier of L) = g & a is prime ) ;
then reconsider g = g as Function of L, by Th31;
g is meet-preserving by ;
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 & g . y >= Top ) by ;
then g . y = 1 by ;
then A17: p in { f where f is Element of H : f . y = 1 } by A11;
( g . x <= Top & g . x >= Top ) by ;
then g . x = 1 by ;
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 ; :: 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 ;
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 ;
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 ((() `), the carrier of L) = f1 and
A25: a is prime ;
reconsider f1 = f1 as Function of L, by ;
for x being Element of L holds
( f1 . x = {} iff x <= a ) by ;
then f1 is meet-preserving by ;
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
.= 1 by ;
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 ;
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
.= 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 V27()
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 ;
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 ;
set CH = chi ((() `), the carrier of L);
p is prime by ;
then chi ((() `), the carrier of L) in H ;
then reconsider CH = chi ((() `), 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 ;
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 ;
set CH = chi ((() `), the carrier of L);
p is prime by ;
then chi ((() `), the carrier of L) in H ;
then reconsider CH = chi ((() `), 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 ;
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:
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}),()) = F . ("\/" ({x,y},L)) )
thus ex_sup_of F .: {x,y}, BoolePoset H by YELLOW_0:17; :: thesis: "\/" ((F .: {x,y}),()) = 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 by ;
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 ((() `), the carrier of L) = g & a is prime ) ;
then reconsider g = g as Function of L, by Th31;
g is join-preserving by ;
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 ;
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 = the carrier of () 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 ;
then ( g . x = Top or g . y = Top ) by ;
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 ;
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 ;
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 ((() `), the carrier of L) = f1 and
A61: a is prime ;
reconsider f1 = f1 as Function of L, by ;
for x being Element of L holds
( f1 . x = {} iff x <= a ) by ;
then f1 is join-preserving by ;
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 & f1 . y <= Top ) by ;
A65: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by ;
(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41;
then f1 . (x "\/" y) = (f1 . x) "\/" (f1 . y) by
.= 1 by ;
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 ((() `), the carrier of L) = f1 and
A69: b is prime ;
reconsider f1 = f1 as Function of L, by ;
for x being Element of L holds
( f1 . x = {} iff x <= b ) by ;
then f1 is join-preserving by ;
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 & f1 . x <= Top ) by ;
A73: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by ;
(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41;
then f1 . (x "\/" y) = (f1 . y) "\/" (f1 . x) by
.= 1 by ;
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 ;
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
.= 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:
F is sups-preserving
proof
let X be Subset of L; :: according to WAYBEL_0:def 33 :: thesis:
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),()) = F . ("\/" (X,L)) )
thus ex_sup_of F .: X, BoolePoset H by YELLOW_0:17; :: thesis: "\/" ((F .: X),()) = 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 ;
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 ;
f in H ;
then consider p being Element of L such that
A83: f = chi ((() `), the carrier of L) and
p is prime ;
A84: now :: thesis: not f . (sup X) = 0 end;
dom f = the carrier of L by ;
then A86: f . (sup X) in rng f by FUNCT_1:def 3;
rng f c= {0,1} by ;
then ( f . (sup X) = 0 or f . (sup X) = 1 ) by ;
hence a in F . (sup X) by ; :: 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 ((() `), the carrier of L) and
p is prime ;
A90: rng f c= {0,1} by ;
A91: not sup X <= p by ;
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 ;
then f . l in rng f by FUNCT_1:def 3;
then ( f . l = 0 or f . l = 1 ) by ;
then f in { g where g is Element of H : g . l = 1 } by ;
then A94: f in F . l by A3;
F . l in F .: X by ;
then a in union (F .: X) by ;
hence a in sup (F .: X) by YELLOW_1:21; :: thesis: verum
end;
hence "\/" ((F .: X),()) = 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