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