let L be complete LATTICE; ( 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 }
;
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)
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;
WAYBEL_0:def 34 F preserves_inf_of {x,y}
assume
ex_inf_of {x,y},
L
;
WAYBEL_0:def 30 ( 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;
"/\" ((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 ;
TARSKI:def 3 ( 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 }
;
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;
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 ;
TARSKI:def 3 ( 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 }
;
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;
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
;
verum
end;
assume A28:
PRIME L is order-generating
; ( L is distributive & L is meet-continuous )
A29:
F is V27()
proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( 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
;
x1 = x2
reconsider l2 =
x2 as
Element of
L by A31;
reconsider l1 =
x1 as
Element of
L by A30;
now not l1 <> l2A33:
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
;
contradictionper cases
( not l1 <= l2 or not l2 <= l1 )
by A35, ORDERS_2:2;
suppose
not
l1 <= l2
;
contradictionthen 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 not CH in F . l2assume
CH in F . l2
;
contradictionthen
ex
f being
Element of
H st
(
f = CH &
f . l2 = 1 )
by A33;
hence
contradiction
by A37, Th32;
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;
verum end; suppose
not
l2 <= l1
;
contradictionthen 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 not CH in F . l1assume
CH in F . l1
;
contradictionthen
ex
f being
Element of
H st
(
f = CH &
f . l1 = 1 )
by A34;
hence
contradiction
by A41, Th32;
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;
verum end; end; end;
hence
x1 = x2
;
verum
end;
F is join-preserving
proof
let x,
y be
Element of
L;
WAYBEL_0:def 35 F preserves_sup_of {x,y}
assume
ex_sup_of {x,y},
L
;
WAYBEL_0:def 31 ( 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;
"\/" ((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 ;
TARSKI:def 3 ( 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 }
;
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;
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;
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 ;
TARSKI:def 3 ( 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 }
;
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 }
;
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;
verum end; suppose
p in { f where f is Element of H : f . y = 1 }
;
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;
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
;
verum
end;
hence
L is distributive
by A7, A29, Th3; L is meet-continuous
F is sups-preserving
proof
let X be
Subset of
L;
WAYBEL_0:def 33 F preserves_sup_of X
F preserves_sup_of X
proof
assume
ex_sup_of X,
L
;
WAYBEL_0:def 31 ( 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;
"\/" ((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)
F . (sup X) c= sup (F .: X)
proof
let a be
object ;
TARSKI:def 3 ( not a in F . (sup X) or a in sup (F .: X) )
assume
a in F . (sup X)
;
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;
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;
verum
end;
hence
"\/" (
(F .: X),
(BoolePoset H))
= F . ("\/" (X,L))
by A75;
verum
end;
hence
F preserves_sup_of X
;
verum
end;
hence
L is meet-continuous
by A7, A29, Th4; verum