let L be complete LATTICE; :: thesis: ( PRIME L is order-generating implies ( L is distributive & L is meet-continuous ) )
assume A1:
PRIME L is order-generating
; :: thesis: ( 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 } ;
consider p' being prime Element of L;
A2:
chi ((downarrow p') ` ),the carrier of L in { (chi ((downarrow p) ` ),the carrier of L) where p is Element of L : p is prime }
;
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 A2, FUNCT_1:def 19;
A3: the carrier of (BoolePoset H) =
the carrier of (InclPoset (bool H))
by YELLOW_1:4
.=
bool H
by YELLOW_1:1
;
deffunc H1( set ) -> set = { f where f is Element of H : f . $1 = 1 } ;
consider F being Function such that
A4:
dom F = the carrier of L
and
A5:
for x being set st x in the carrier of L holds
F . x = H1(x)
from FUNCT_1:sch 3();
rng F c= the carrier of (BoolePoset H)
then reconsider F = F as Function of L,(BoolePoset H) by A4, FUNCT_2:def 1, RELSET_1:11;
A8:
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)
A9:
F .: {x,y} = {(F . x),(F . y)}
by A4, FUNCT_1:118;
A10:
{ 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
set ;
:: 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
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 A11:
(
p in { f where f is Element of H : f . x = 1 } &
p in { f where f is Element of H : f . y = 1 } )
by XBOOLE_0:def 4;
then consider f1 being
Element of
H such that A12:
(
f1 = p &
f1 . x = 1 )
;
consider f2 being
Element of
H such that A13:
(
f2 = p &
f2 . y = 1 )
by A11;
f1 in H
;
then consider a being
Element of
L such that A14:
(
chi ((downarrow a) ` ),the
carrier of
L = f1 &
a is
prime )
;
reconsider f1 =
f1 as
Function of
L,
(BoolePoset {{} }) by A14, Th31;
dom f1 = the
carrier of
L
by FUNCT_2:def 1;
then A15:
{(f1 . x),(f1 . y)} = f1 .: {x,y}
by FUNCT_1:118;
for
x being
Element of
L holds
(
f1 . x = {} iff
x <= a )
by A14, Th32;
then
f1 is
meet-preserving
by A14, Th25;
then
(
f1 preserves_inf_of {x,y} &
ex_inf_of {x,y},
L &
x "/\" y = inf {x,y} &
(f1 . x) "/\" (f1 . y) = inf {(f1 . x),(f1 . y)} )
by WAYBEL_0:def 34, YELLOW_0:17, YELLOW_0:40;
then f1 . (x "/\" y) =
(f1 . x) "/\" (f1 . y)
by A15, WAYBEL_0:def 30
.=
1
by A12, A13, YELLOW_5:2
;
hence
p in { f where f is Element of H : f . (x "/\" y) = 1 }
by A12;
:: thesis: verum
end;
A16:
{ 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
set ;
:: 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 } )
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 A17:
(
g = p &
g . (x "/\" y) = 1 )
;
g in H
;
then consider a being
Element of
L such that A18:
(
chi ((downarrow a) ` ),the
carrier of
L = g &
a is
prime )
;
reconsider g =
g as
Function of
L,
(BoolePoset {{} }) by A18, Th31;
dom g = the
carrier of
L
by FUNCT_2:def 1;
then A19:
{(g . x),(g . y)} = g .: {x,y}
by FUNCT_1:118;
A20:
1
= Top (BoolePoset {{} })
by CARD_1:87, YELLOW_1:19;
A21:
(
g . x <= Top (BoolePoset {{} }) &
g . y <= Top (BoolePoset {{} }) )
by YELLOW_0:45;
g is
meet-preserving
by A18, Th33;
then
(
g preserves_inf_of {x,y} &
ex_inf_of {x,y},
L &
x "/\" y = inf {x,y} &
(g . x) "/\" (g . y) = inf {(g . x),(g . y)} )
by WAYBEL_0:def 34, YELLOW_0:17, YELLOW_0:40;
then
g . (x "/\" y) = (g . x) "/\" (g . y)
by A19, WAYBEL_0:def 30;
then A22:
(
g . x >= Top (BoolePoset {{} }) &
g . y >= Top (BoolePoset {{} }) )
by A17, A20, YELLOW_0:23;
then A23:
g . x = 1
by A20, A21, ORDERS_2:25;
g . y = 1
by A20, A21, A22, ORDERS_2:25;
then
(
p in { f where f is Element of H : f . x = 1 } &
p in { f where f is Element of H : f . y = 1 } )
by A17, A23;
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 4;
:: thesis: verum
end;
thus inf (F .: {x,y}) =
(F . x) "/\" (F . y)
by A9, YELLOW_0:40
.=
(F . x) /\ (F . y)
by YELLOW_1:17
.=
{ f where f is Element of H : f . x = 1 } /\ (F . y)
by A5
.=
{ f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 }
by A5
.=
{ f where f is Element of H : f . (x "/\" y) = 1 }
by A10, A16, XBOOLE_0:def 10
.=
F . (x "/\" y)
by A5
.=
F . (inf {x,y})
by YELLOW_0:40
;
:: thesis: verum
end;
A24:
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)
A25:
F .: {x,y} = {(F . x),(F . y)}
by A4, FUNCT_1:118;
A26:
{ 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
set ;
:: 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 A27:
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 A27, 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 A28:
(
f1 = p &
f1 . x = 1 )
;
f1 in H
;
then consider a being
Element of
L such that A29:
(
chi ((downarrow a) ` ),the
carrier of
L = f1 &
a is
prime )
;
reconsider f1 =
f1 as
Function of
L,
(BoolePoset {{} }) by A29, Th31;
dom f1 = the
carrier of
L
by FUNCT_2:def 1;
then A30:
{(f1 . x),(f1 . y)} = f1 .: {x,y}
by FUNCT_1:118;
A31:
1
= Top (BoolePoset {{} })
by CARD_1:87, YELLOW_1:19;
A32:
f1 . y <= Top (BoolePoset {{} })
by YELLOW_0:45;
for
x being
Element of
L holds
(
f1 . x = {} iff
x <= a )
by A29, Th32;
then
f1 is
join-preserving
by A29, Th25;
then
(
f1 preserves_sup_of {x,y} &
ex_sup_of {x,y},
L &
x "\/" y = sup {x,y} &
(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} )
by WAYBEL_0:def 35, YELLOW_0:17, YELLOW_0:41;
then f1 . (x "\/" y) =
(f1 . x) "\/" (f1 . y)
by A30, WAYBEL_0:def 31
.=
1
by A28, A31, A32, YELLOW_0:24
;
hence
p in { f where f is Element of H : f . (x "\/" y) = 1 }
by A28;
:: 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 A33:
(
f1 = p &
f1 . y = 1 )
;
f1 in H
;
then consider b being
Element of
L such that A34:
(
chi ((downarrow b) ` ),the
carrier of
L = f1 &
b is
prime )
;
reconsider f1 =
f1 as
Function of
L,
(BoolePoset {{} }) by A34, Th31;
dom f1 = the
carrier of
L
by FUNCT_2:def 1;
then A35:
{(f1 . x),(f1 . y)} = f1 .: {x,y}
by FUNCT_1:118;
A36:
1
= Top (BoolePoset {{} })
by CARD_1:87, YELLOW_1:19;
A37:
f1 . x <= Top (BoolePoset {{} })
by YELLOW_0:45;
for
x being
Element of
L holds
(
f1 . x = {} iff
x <= b )
by A34, Th32;
then
f1 is
join-preserving
by A34, Th25;
then
(
f1 preserves_sup_of {x,y} &
ex_sup_of {x,y},
L &
x "\/" y = sup {x,y} &
(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} )
by WAYBEL_0:def 35, YELLOW_0:17, YELLOW_0:41;
then f1 . (x "\/" y) =
(f1 . y) "\/" (f1 . x)
by A35, WAYBEL_0:def 31
.=
1
by A33, A36, A37, YELLOW_0:24
;
hence
p in { f where f is Element of H : f . (x "\/" y) = 1 }
by A33;
:: thesis: verum end;
end;
A38:
{ 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
set ;
:: 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 } )
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 A39:
(
g = p &
g . (x "\/" y) = 1 )
;
g in H
;
then consider a being
Element of
L such that A40:
(
chi ((downarrow a) ` ),the
carrier of
L = g &
a is
prime )
;
reconsider g =
g as
Function of
L,
(BoolePoset {{} }) by A40, Th31;
A41:
(
dom g = the
carrier of
L &
rng g c= the
carrier of
(BoolePoset {{} }) )
by FUNCT_2:def 1;
A42: the
carrier of
(BoolePoset {{} }) =
the
carrier of
(InclPoset (bool {{} }))
by YELLOW_1:4
.=
bool {{} }
by YELLOW_1:1
.=
{{} ,{{} }}
by ZFMISC_1:30
;
A43:
g .: {x,y} = {(g . x),(g . y)}
by A41, FUNCT_1:118;
A44:
( (
g . x = {} or
g . x = {{} } ) & (
g . y = {} or
g . y = {{} } ) )
by A42, TARSKI:def 2;
A45:
1
= Top (BoolePoset {{} })
by CARD_1:87, YELLOW_1:19;
g is
join-preserving
by A40, Th33;
then A46:
(
g preserves_sup_of {x,y} &
ex_sup_of {x,y},
L &
x "\/" y = sup {x,y} &
(g . x) "\/" (g . y) = sup {(g . x),(g . y)} )
by WAYBEL_0:def 35, YELLOW_0:17, YELLOW_0:41;
then
(
g . x = Top (BoolePoset {{} }) or
g . y = Top (BoolePoset {{} }) )
by A44, 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 A39, 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;
thus sup (F .: {x,y}) =
(F . x) "\/" (F . y)
by A25, YELLOW_0:41
.=
(F . x) \/ (F . y)
by YELLOW_1:17
.=
{ f where f is Element of H : f . x = 1 } \/ (F . y)
by A5
.=
{ f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 }
by A5
.=
{ f where f is Element of H : f . (x "\/" y) = 1 }
by A26, A38, XBOOLE_0:def 10
.=
F . (x "\/" y)
by A5
.=
F . (sup {x,y})
by YELLOW_0:41
;
:: thesis: verum
end;
A47:
F is one-to-one
proof
let x1,
x2 be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 )
assume A48:
(
x1 in dom F &
x2 in dom F &
F . x1 = F . x2 )
;
:: thesis: x1 = x2
then reconsider l1 =
x1 as
Element of
L ;
reconsider l2 =
x2 as
Element of
L by A48;
now assume A49:
l1 <> l2
;
:: thesis: contradictionA50:
F . l1 = { f where f is Element of H : f . l1 = 1 }
by A5;
A51:
F . l2 = { f where f is Element of H : f . l2 = 1 }
by A5;
per cases
( not l1 <= l2 or not l2 <= l1 )
by A49, ORDERS_2:25;
suppose
not
l1 <= l2
;
:: thesis: contradictionthen consider p being
Element of
L such that A52:
(
p in PRIME L &
l2 <= p & not
l1 <= p )
by A1, Th17;
set CH =
chi ((downarrow p) ` ),the
carrier of
L;
p is
prime
by A52, 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 ;
A53:
(
dom CH = the
carrier of
L &
rng CH c= {0 ,1} )
by FUNCT_2:def 1, RELAT_1:def 19;
then
CH . l1 in rng CH
by FUNCT_1:def 5;
then A54:
(
CH . l1 = 0 or
CH . l1 = 1 )
by A53, TARSKI:def 2;
hence
contradiction
by A48, A50, A52, A54, Th32;
:: thesis: verum end; suppose
not
l2 <= l1
;
:: thesis: contradictionthen consider p being
Element of
L such that A55:
(
p in PRIME L &
l1 <= p & not
l2 <= p )
by A1, Th17;
set CH =
chi ((downarrow p) ` ),the
carrier of
L;
p is
prime
by A55, 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 ;
A56:
(
dom CH = the
carrier of
L &
rng CH c= {0 ,1} )
by FUNCT_2:def 1, RELAT_1:def 19;
then
CH . l2 in rng CH
by FUNCT_1:def 5;
then A57:
(
CH . l2 = 0 or
CH . l2 = 1 )
by A56, TARSKI:def 2;
hence
contradiction
by A48, A51, A55, A57, Th32;
:: thesis: verum end; end;
hence
x1 = x2
;
:: thesis: verum
end;
hence
L is distributive
by A8, A24, 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)
A58:
F . (sup X) = { g where g is Element of H : g . (sup X) = 1 }
by A5;
A59:
sup (F .: X) c= F . (sup X)
F . (sup X) c= sup (F .: X)
proof
let a be
set ;
:: 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 A67:
(
a = f &
f . (sup X) = 1 )
by A58;
f in H
;
then consider p being
Element of
L such that A68:
(
f = chi ((downarrow p) ` ),the
carrier of
L &
p is
prime )
;
A69:
not
sup X <= p
by A67, A68, Th32;
then consider l being
Element of
L such that A70:
(
l in X & not
l <= p )
;
A71:
(
dom f = the
carrier of
L &
rng f c= {0 ,1} )
by A68, FUNCT_2:def 1, RELAT_1:def 19;
then
f . l in rng f
by FUNCT_1:def 5;
then
(
f . l = 0 or
f . l = 1 )
by A71, TARSKI:def 2;
then
f in { g where g is Element of H : g . l = 1 }
by A68, A70, Th32;
then A72:
f in F . l
by A5;
F . l in F .: X
by A4, A70, FUNCT_1:def 12;
then
a in union (F .: X)
by A67, A72, 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 A59, XBOOLE_0:def 10;
:: thesis: verum
end;
hence
F preserves_sup_of X
;
:: thesis: verum
end;
hence
L is meet-continuous
by A8, A47, Th4; :: thesis: verum