let L be finite distributive LATTICE; ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st
( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) )
set I = InclPoset (LOWER (subrelstr (Join-IRR L)));
deffunc H1( Element of L) -> Element of bool the carrier of L = (downarrow $1) /\ (Join-IRR L);
consider r being ManySortedSet of the carrier of L such that
A1:
for d being Element of L holds r . d = H1(d)
from PBOOLE:sch 5();
A2:
rng r c= the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))
proof
let t be
object ;
TARSKI:def 3 ( not t in rng r or t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) )
reconsider tt =
t as
set by TARSKI:1;
assume
t in rng r
;
t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))
then consider x being
object such that A3:
x in dom r
and A4:
t = r . x
by FUNCT_1:def 3;
reconsider x =
x as
Element of
L by A3;
A5:
t = (downarrow x) /\ (Join-IRR L)
by A1, A4;
then
tt c= Join-IRR L
by XBOOLE_1:17;
then reconsider t =
t as
Subset of
(subrelstr (Join-IRR L)) by YELLOW_0:def 15;
A6:
t is
lower
proof
let c,
d be
Element of
(subrelstr (Join-IRR L));
WAYBEL_0:def 19 ( not c in t or not d <= c or d in t )
assume that A7:
c in t
and A8:
d <= c
;
d in t
A9:
d is
Element of
Join-IRR L
by YELLOW_0:def 15;
A10:
not
Join-IRR L is
empty
by A5, A7;
then
d in Join-IRR L
by A9;
then reconsider c1 =
c,
d1 =
d as
Element of
L by A5, A7;
c in downarrow x
by A5, A7, XBOOLE_0:def 4;
then A11:
c1 <= x
by WAYBEL_0:17;
d1 <= c1
by A8, YELLOW_0:59;
then
d1 <= x
by A11, ORDERS_2:3;
then
d1 in downarrow x
by WAYBEL_0:17;
hence
d in t
by A5, A10, A9, XBOOLE_0:def 4;
verum
end;
the
carrier of
(InclPoset (LOWER (subrelstr (Join-IRR L)))) = LOWER (subrelstr (Join-IRR L))
by YELLOW_1:1;
hence
t in the
carrier of
(InclPoset (LOWER (subrelstr (Join-IRR L))))
by A6;
verum
end;
dom r = the carrier of L
by PARTFUN1:def 2;
then reconsider r = r as Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) by A2, FUNCT_2:def 1, RELSET_1:4;
A12:
for x, y being Element of L holds
( x <= y iff r . x <= r . y )
proof
let x,
y be
Element of
L;
( x <= y iff r . x <= r . y )
thus
(
x <= y implies
r . x <= r . y )
( r . x <= r . y implies x <= y )
thus
(
r . x <= r . y implies
x <= y )
verum
end;
the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) c= rng r
proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) or x in rng r )
assume A16:
x in the
carrier of
(InclPoset (LOWER (subrelstr (Join-IRR L))))
;
x in rng r
thus
x in rng r
verumproof
x in LOWER (subrelstr (Join-IRR L))
by A16, YELLOW_1:1;
then consider X being
Subset of
(subrelstr (Join-IRR L)) such that A17:
x = X
and A18:
X is
lower
;
the
carrier of
(subrelstr (Join-IRR L)) c= Join-IRR L
by YELLOW_0:def 15;
then
the
carrier of
(subrelstr (Join-IRR L)) c= the
carrier of
L
by XBOOLE_1:1;
then reconsider X1 =
X as
Subset of
L by XBOOLE_1:1;
ex
y being
set st
(
y in dom r &
x = r . y )
proof
take y =
sup X1;
( y in dom r & x = r . y )
dom r = the
carrier of
L
by FUNCT_2:def 1;
hence
y in dom r
;
x = r . y
A19:
(downarrow (sup X1)) /\ (Join-IRR L) c= X1
proof
let r be
Element of
L;
LATTICE7:def 1 ( r in (downarrow (sup X1)) /\ (Join-IRR L) implies r in X1 )
reconsider r1 =
r as
Element of
L ;
assume A20:
r in (downarrow (sup X1)) /\ (Join-IRR L)
;
r in X1
then
r in downarrow (sup X1)
by XBOOLE_0:def 4;
then A21:
r1 <= sup X1
by WAYBEL_0:17;
per cases
( r1 in X1 or not r1 in X1 )
;
suppose A22:
not
r1 in X1
;
r in X1A23:
r1 in Join-IRR L
by A20, XBOOLE_0:def 4;
then consider z being
Element of
L such that A24:
z < r1
and A25:
for
y being
Element of
L st
y < r1 holds
y <= z
by Th11;
{r1} "/\" X1 is_<=_than z
proof
let a be
Element of
L;
LATTICE3:def 9 ( not a in {r1} "/\" X1 or a <= z )
A26:
r1 in the
carrier of
(subrelstr (Join-IRR L))
by A23, YELLOW_0:def 15;
assume
a in {r1} "/\" X1
;
a <= z
then
a in { (r1 "/\" k) where k is Element of L : k in X1 }
by YELLOW_4:42;
then consider x being
Element of
L such that A27:
a = r1 "/\" x
and A28:
x in X1
;
reconsider r9 =
r1,
x9 =
x as
Element of
(subrelstr (Join-IRR L)) by A23, A28, YELLOW_0:def 15;
A29:
ex_inf_of {r1,x},
L
by YELLOW_0:17;
then A30:
a <= x
by A27, YELLOW_0:19;
A31:
a <> r1
by A18, A22, A28, A30, A26, YELLOW_0:60;
a <= r1
by A27, A29, YELLOW_0:19;
then
a < r1
by A31, ORDERS_2:def 6;
hence
a <= z
by A25;
verum
end; then A32:
sup ({r1} "/\" X1) <= z
by YELLOW_0:32;
(
r1 = r1 "/\" (sup X1) &
r1 "/\" (sup X1) = sup ({r1} "/\" X1) )
by A21, WAYBEL_2:15, YELLOW_0:25;
hence
r in X1
by A24, A32, ORDERS_2:7;
verum end;
end;
X1 c= (downarrow (sup X1)) /\ (Join-IRR L)
then
X1 = (downarrow (sup X1)) /\ (Join-IRR L)
by A19, XBOOLE_0:def 10;
hence
x = r . y
by A1, A17;
verum
end;
hence
x in rng r
by FUNCT_1:def 3;
verum
end;
end;
then A36:
rng r = the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))
by XBOOLE_0:def 10;
r is one-to-one
then
r is isomorphic
by A36, A12, WAYBEL_0:66;
hence
ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st
( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) )
by A1; verum