let L be lower-bounded LATTICE; ex A being non empty set ex f being Homomorphism of L,(EqRelLATT A) st
( f is one-to-one & type_of (Image f) <= 3 )
set A = the carrier of L;
set D = BasicDF L;
set S = the ExtensionSeq of the carrier of L, BasicDF L;
set FS = union { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } ;
A1:
( the ExtensionSeq of the carrier of L, BasicDF L . 0) `1 in { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum }
;
A2:
the ExtensionSeq of the carrier of L, BasicDF L . 0 = [ the carrier of L,(BasicDF L)]
by Def21;
then
( the ExtensionSeq of the carrier of L, BasicDF L . 0) `1 = the carrier of L
by MCART_1:def 1;
then
the carrier of L c= union { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum }
by A1, ZFMISC_1:74;
then reconsider FS = union { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } as non empty set ;
reconsider FD = union { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum } as distance_function of FS,L by Th44;
alpha FD is join-preserving
proof
set f =
alpha FD;
let a,
b be
Element of
L;
WAYBEL_0:def 35 alpha FD preserves_sup_of {a,b}
A3:
ex_sup_of (alpha FD) .: {a,b},
EqRelLATT FS
by YELLOW_0:17;
consider e3 being
Equivalence_Relation of
FS such that A4:
e3 = (alpha FD) . (a "\/" b)
and A5:
for
x,
y being
Element of
FS holds
(
[x,y] in e3 iff
FD . (
x,
y)
<= a "\/" b )
by Def9;
consider e2 being
Equivalence_Relation of
FS such that A6:
e2 = (alpha FD) . b
and A7:
for
x,
y being
Element of
FS holds
(
[x,y] in e2 iff
FD . (
x,
y)
<= b )
by Def9;
consider e1 being
Equivalence_Relation of
FS such that A8:
e1 = (alpha FD) . a
and A9:
for
x,
y being
Element of
FS holds
(
[x,y] in e1 iff
FD . (
x,
y)
<= a )
by Def9;
A10:
field e2 = FS
by ORDERS_1:12;
now let x,
y be
set ;
( [x,y] in e2 implies [x,y] in e3 )A11:
b <= b "\/" a
by YELLOW_0:22;
assume A12:
[x,y] in e2
;
[x,y] in e3then reconsider x9 =
x,
y9 =
y as
Element of
FS by A10, RELAT_1:15;
FD . (
x9,
y9)
<= b
by A7, A12;
then
FD . (
x9,
y9)
<= b "\/" a
by A11, ORDERS_2:3;
hence
[x,y] in e3
by A5;
verum end;
then A13:
e2 c= e3
by RELAT_1:def 3;
A14:
field e3 = FS
by ORDERS_1:12;
for
u,
v being
set st
[u,v] in e3 holds
[u,v] in e1 "\/" e2
proof
let u,
v be
set ;
( [u,v] in e3 implies [u,v] in e1 "\/" e2 )
A15:
3
in Seg 5
;
assume A16:
[u,v] in e3
;
[u,v] in e1 "\/" e2
then reconsider x =
u,
y =
v as
Element of
FS by A14, RELAT_1:15;
FD . (
x,
y)
<= a "\/" b
by A5, A16;
then consider z1,
z2,
z3 being
Element of
FS such that A17:
FD . (
x,
z1)
= a
and A18:
FD . (
z2,
z3)
= a
and A19:
FD . (
z1,
z2)
= b
and A20:
FD . (
z3,
y)
= b
by Th45;
A21:
u in FS
by A14, A16, RELAT_1:15;
defpred S1[
set ,
set ]
means ( ( $1
= 1 implies $2
= x ) & ( $1
= 2 implies $2
= z1 ) & ( $1
= 3 implies $2
= z2 ) & ( $1
= 4 implies $2
= z3 ) & ( $1
= 5 implies $2
= y ) );
A22:
for
m being
Nat st
m in Seg 5 holds
ex
w being
set st
S1[
m,
w]
proof
let m be
Nat;
( m in Seg 5 implies ex w being set st S1[m,w] )
assume A23:
m in Seg 5
;
ex w being set st S1[m,w]
per cases
( m = 1 or m = 2 or m = 3 or m = 4 or m = 5 )
by A23, Lm3;
suppose A24:
m = 1
;
ex w being set st S1[m,w]take
x
;
S1[m,x]thus
S1[
m,
x]
by A24;
verum end; suppose A25:
m = 2
;
ex w being set st S1[m,w]take
z1
;
S1[m,z1]thus
S1[
m,
z1]
by A25;
verum end; suppose A26:
m = 3
;
ex w being set st S1[m,w]take
z2
;
S1[m,z2]thus
S1[
m,
z2]
by A26;
verum end; suppose A27:
m = 4
;
ex w being set st S1[m,w]take
z3
;
S1[m,z3]thus
S1[
m,
z3]
by A27;
verum end; suppose A28:
m = 5
;
ex w being set st S1[m,w]take
y
;
S1[m,y]thus
S1[
m,
y]
by A28;
verum end;
end;
ex
p being
FinSequence st
(
dom p = Seg 5 & ( for
k being
Nat st
k in Seg 5 holds
S1[
k,
p . k] ) )
from FINSEQ_1:sch 1(A22);
then consider h being
FinSequence such that A29:
dom h = Seg 5
and A30:
for
m being
Nat st
m in Seg 5 holds
( (
m = 1 implies
h . m = x ) & (
m = 2 implies
h . m = z1 ) & (
m = 3 implies
h . m = z2 ) & (
m = 4 implies
h . m = z3 ) & (
m = 5 implies
h . m = y ) )
;
A31:
len h = 5
by A29, FINSEQ_1:def 3;
A32:
5
in Seg 5
;
A33:
4
in Seg 5
;
A34:
1
in Seg 5
;
then A35:
u = h . 1
by A30;
A36:
2
in Seg 5
;
A37:
for
j being
Element of
NAT st 1
<= j &
j < len h holds
[(h . j),(h . (j + 1))] in e1 \/ e2
v =
h . 5
by A30, A32
.=
h . (len h)
by A29, FINSEQ_1:def 3
;
hence
[u,v] in e1 "\/" e2
by A21, A31, A35, A37, EQREL_1:28;
verum
end;
then A43:
e3 c= e1 "\/" e2
by RELAT_1:def 3;
A44:
field e1 = FS
by ORDERS_1:12;
now let x,
y be
set ;
( [x,y] in e1 implies [x,y] in e3 )A45:
a <= a "\/" b
by YELLOW_0:22;
assume A46:
[x,y] in e1
;
[x,y] in e3then reconsider x9 =
x,
y9 =
y as
Element of
FS by A44, RELAT_1:15;
FD . (
x9,
y9)
<= a
by A9, A46;
then
FD . (
x9,
y9)
<= a "\/" b
by A45, ORDERS_2:3;
hence
[x,y] in e3
by A5;
verum end;
then
e1 c= e3
by RELAT_1:def 3;
then
e1 \/ e2 c= e3
by A13, XBOOLE_1:8;
then A47:
e1 "\/" e2 c= e3
by EQREL_1:def 2;
dom (alpha FD) = the
carrier of
L
by FUNCT_2:def 1;
then sup ((alpha FD) .: {a,b}) =
sup {((alpha FD) . a),((alpha FD) . b)}
by FUNCT_1:60
.=
((alpha FD) . a) "\/" ((alpha FD) . b)
by YELLOW_0:41
.=
e1 "\/" e2
by A8, A6, Th10
.=
(alpha FD) . (a "\/" b)
by A4, A47, A43, XBOOLE_0:def 10
.=
(alpha FD) . (sup {a,b})
by YELLOW_0:41
;
hence
alpha FD preserves_sup_of {a,b}
by A3, WAYBEL_0:def 31;
verum
end;
then reconsider f = alpha FD as Homomorphism of L,(EqRelLATT FS) by Th16;
A48:
dom f = the carrier of L
by FUNCT_2:def 1;
A49:
Image f = subrelstr (rng f)
by YELLOW_2:def 2;
A50:
ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS )
proof
A51:
{ the carrier of L} <> {{ the carrier of L}}
consider A9 being non
empty set ,
d9 being
distance_function of
A9,
L,
Aq9 being non
empty set ,
dq9 being
distance_function of
Aq9,
L such that A52:
Aq9,
dq9 is_extension_of A9,
d9
and A53:
the
ExtensionSeq of the
carrier of
L,
BasicDF L . 0 = [A9,d9]
and A54:
the
ExtensionSeq of the
carrier of
L,
BasicDF L . (0 + 1) = [Aq9,dq9]
by Def21;
(
A9 = the
carrier of
L &
d9 = BasicDF L )
by A2, A53, ZFMISC_1:27;
then consider q being
QuadrSeq of
BasicDF L such that A55:
Aq9 = NextSet (BasicDF L)
and A56:
dq9 = NextDelta q
by A52, Def20;
ConsecutiveSet ( the
carrier of
L,
{})
= the
carrier of
L
by Th24;
then reconsider Q =
Quadr (
q,
{}) as
Element of
[: the carrier of L, the carrier of L, the carrier of L, the carrier of L:] ;
A57:
( the ExtensionSeq of the carrier of L, BasicDF L . 1) `2 in { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum }
;
succ {} c= DistEsti (BasicDF L)
by Lm4;
then
{} in DistEsti (BasicDF L)
by ORDINAL1:21;
then A58:
{} in dom q
by Th28;
then
q . {} in rng q
by FUNCT_1:def 3;
then
q . {} in { [u,v,a9,b9] where u, v is Element of the carrier of L, a9, b9 is Element of L : (BasicDF L) . (u,v) <= a9 "\/" b9 }
by Def14;
then consider u,
v being
Element of the
carrier of
L,
a,
b being
Element of
L such that A59:
q . {} = [u,v,a,b]
and
(BasicDF L) . (
u,
v)
<= a "\/" b
;
consider e being
Equivalence_Relation of
FS such that A60:
e = f . b
and A61:
for
x,
y being
Element of
FS holds
(
[x,y] in e iff
FD . (
x,
y)
<= b )
by Def9;
A62:
Quadr (
q,
{})
= [u,v,a,b]
by A58, A59, Def15;
( the ExtensionSeq of the carrier of L, BasicDF L . 1) `2 = NextDelta q
by A54, A56, MCART_1:def 2;
then A63:
NextDelta q c= FD
by A57, ZFMISC_1:74;
A64:
{{ the carrier of L}} in {{ the carrier of L},{{ the carrier of L}},{{{ the carrier of L}}}}
by ENUMSET1:def 1;
then A65:
{{ the carrier of L}} in the
carrier of
L \/ {{ the carrier of L},{{ the carrier of L}},{{{ the carrier of L}}}}
by XBOOLE_0:def 3;
take
e
;
( e in the carrier of (Image f) & e <> id FS )
e in rng f
by A48, A60, FUNCT_1:def 3;
hence
e in the
carrier of
(Image f)
by A49, YELLOW_0:def 15;
e <> id FS
A66:
( the ExtensionSeq of the carrier of L, BasicDF L . 1) `1 in { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum }
;
( the ExtensionSeq of the carrier of L, BasicDF L . 1) `1 = NextSet (BasicDF L)
by A54, A55, MCART_1:def 1;
then A67:
NextSet (BasicDF L) c= FS
by A66, ZFMISC_1:74;
new_set the
carrier of
L =
new_set (ConsecutiveSet ( the carrier of L,{}))
by Th24
.=
ConsecutiveSet ( the
carrier of
L,
(succ {}))
by Th25
;
then
new_set the
carrier of
L c= NextSet (BasicDF L)
by Lm4, Th32;
then A68:
new_set the
carrier of
L c= FS
by A67, XBOOLE_1:1;
A69:
{{ the carrier of L}} in new_set the
carrier of
L
by A64, XBOOLE_0:def 3;
A70:
{ the carrier of L} in {{ the carrier of L},{{ the carrier of L}},{{{ the carrier of L}}}}
by ENUMSET1:def 1;
then
{ the carrier of L} in the
carrier of
L \/ {{ the carrier of L},{{ the carrier of L}},{{{ the carrier of L}}}}
by XBOOLE_0:def 3;
then reconsider W =
{ the carrier of L},
V =
{{ the carrier of L}} as
Element of
FS by A68, A69;
A71:
(
ConsecutiveSet ( the
carrier of
L,
{})
= the
carrier of
L &
ConsecutiveDelta (
q,
{})
= BasicDF L )
by Th24, Th29;
ConsecutiveDelta (
q,
(succ {})) =
new_bi_fun (
(BiFun ((ConsecutiveDelta (q,{})),(ConsecutiveSet ( the carrier of L,{})),L)),
(Quadr (q,{})))
by Th30
.=
new_bi_fun (
(BasicDF L),
Q)
by A71, Def16
;
then
new_bi_fun (
(BasicDF L),
Q)
c= NextDelta q
by Lm4, Th35;
then A72:
new_bi_fun (
(BasicDF L),
Q)
c= FD
by A63, XBOOLE_1:1;
(
dom (new_bi_fun ((BasicDF L),Q)) = [:(new_set the carrier of L),(new_set the carrier of L):] &
{ the carrier of L} in new_set the
carrier of
L )
by A70, FUNCT_2:def 1, XBOOLE_0:def 3;
then
[{ the carrier of L},{{ the carrier of L}}] in dom (new_bi_fun ((BasicDF L),Q))
by A65, ZFMISC_1:87;
then FD . (
W,
V) =
(new_bi_fun ((BasicDF L),Q)) . (
{ the carrier of L},
{{ the carrier of L}})
by A72, GRFUNC_1:2
.=
Q `4
by Def11
.=
b
by A62, MCART_1:def 11
;
then
[{ the carrier of L},{{ the carrier of L}}] in e
by A61;
hence
e <> id FS
by A51, RELAT_1:def 10;
verum
end;
take
FS
; ex f being Homomorphism of L,(EqRelLATT FS) st
( f is one-to-one & type_of (Image f) <= 3 )
take
f
; ( f is one-to-one & type_of (Image f) <= 3 )
BasicDF L is onto
by Th43;
then A73:
rng (BasicDF L) = the carrier of L
by FUNCT_2:def 3;
for w being set st w in the carrier of L holds
ex z being set st
( z in [:FS,FS:] & w = FD . z )
proof
let w be
set ;
( w in the carrier of L implies ex z being set st
( z in [:FS,FS:] & w = FD . z ) )
A74:
( the ExtensionSeq of the carrier of L, BasicDF L . 0) `1 in { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum }
;
A75:
( the ExtensionSeq of the carrier of L, BasicDF L . 0) `2 in { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum }
;
A76:
the
ExtensionSeq of the
carrier of
L,
BasicDF L . 0 = [ the carrier of L,(BasicDF L)]
by Def21;
then
BasicDF L = ( the ExtensionSeq of the carrier of L, BasicDF L . 0) `2
by MCART_1:def 2;
then A77:
BasicDF L c= FD
by A75, ZFMISC_1:74;
assume
w in the
carrier of
L
;
ex z being set st
( z in [:FS,FS:] & w = FD . z )
then consider z being
set such that A78:
z in [: the carrier of L, the carrier of L:]
and A79:
(BasicDF L) . z = w
by A73, FUNCT_2:11;
take
z
;
( z in [:FS,FS:] & w = FD . z )
the
carrier of
L = ( the ExtensionSeq of the carrier of L, BasicDF L . 0) `1
by A76, MCART_1:def 1;
then
the
carrier of
L c= FS
by A74, ZFMISC_1:74;
then
[: the carrier of L, the carrier of L:] c= [:FS,FS:]
by ZFMISC_1:96;
hence
z in [:FS,FS:]
by A78;
w = FD . z
z in dom (BasicDF L)
by A78, FUNCT_2:def 1;
hence
w = FD . z
by A79, A77, GRFUNC_1:2;
verum
end;
then
rng FD = the carrier of L
by FUNCT_2:10;
then
FD is onto
by FUNCT_2:def 3;
hence
f is one-to-one
by Th17; type_of (Image f) <= 3
for e1, e2 being Equivalence_Relation of FS
for x, y being set st e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = 3 + 2 & x,y are_joint_by F,e1,e2 )
by Th46;
hence
type_of (Image f) <= 3
by A50, Th15; verum