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 Def20;
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, A2, 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 Th41;
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 Def8;
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 Def8;
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 Def8;
A10:
field e2 = FS
by ORDERS_1:12;
now for x, y being object st [x,y] in e2 holds
[x,y] in e3let x,
y be
object ;
( [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
object st
[u,v] in e3 holds
[u,v] in e1 "\/" e2
proof
let u,
v be
object ;
( [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 Th42;
A21:
u in FS
by A14, A16, RELAT_1:15;
defpred S1[
set ,
object ]
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
object st
S1[
m,
w]
proof
let m be
Nat;
( m in Seg 5 implies ex w being object st S1[m,w] )
assume
m in Seg 5
;
ex w being object st S1[m,w]
then
not not
m = 1 & ... & not
m = 5
by Lm3;
per cases then
( m = 1 or m = 2 or m = 3 or m = 4 or m = 5 )
;
suppose A23:
m = 1
;
ex w being object st S1[m,w]take
x
;
S1[m,x]thus
S1[
m,
x]
by A23;
verum end; suppose A24:
m = 2
;
ex w being object st S1[m,w]take
z1
;
S1[m,z1]thus
S1[
m,
z1]
by A24;
verum end; suppose A25:
m = 3
;
ex w being object st S1[m,w]take
z2
;
S1[m,z2]thus
S1[
m,
z2]
by A25;
verum end; suppose A26:
m = 4
;
ex w being object st S1[m,w]take
z3
;
S1[m,z3]thus
S1[
m,
z3]
by A26;
verum end; suppose A27:
m = 5
;
ex w being object st S1[m,w]take
y
;
S1[m,y]thus
S1[
m,
y]
by A27;
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 A28:
dom h = Seg 5
and A29:
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 ) )
;
A30:
len h = 5
by A28, FINSEQ_1:def 3;
A31:
5
in Seg 5
;
A32:
4
in Seg 5
;
A33:
1
in Seg 5
;
then A34:
u = h . 1
by A29;
A35:
2
in Seg 5
;
A36:
for
j being
Nat st 1
<= j &
j < len h holds
[(h . j),(h . (j + 1))] in e1 \/ e2
v =
h . 5
by A29, A31
.=
h . (len h)
by A28, FINSEQ_1:def 3
;
hence
[u,v] in e1 "\/" e2
by A21, A30, A34, A36, EQREL_1:28;
verum
end;
then A41:
e3 c= e1 "\/" e2
by RELAT_1:def 3;
A42:
field e1 = FS
by ORDERS_1:12;
now for x, y being object st [x,y] in e1 holds
[x,y] in e3let x,
y be
object ;
( [x,y] in e1 implies [x,y] in e3 )A43:
a <= a "\/" b
by YELLOW_0:22;
assume A44:
[x,y] in e1
;
[x,y] in e3then reconsider x9 =
x,
y9 =
y as
Element of
FS by A42, RELAT_1:15;
FD . (
x9,
y9)
<= a
by A9, A44;
then
FD . (
x9,
y9)
<= a "\/" b
by A43, 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 A45:
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, A45, A41
.=
(alpha FD) . (sup {a,b})
by YELLOW_0:41
;
hence
alpha FD preserves_sup_of {a,b}
by A3;
verum
end;
then reconsider f = alpha FD as Homomorphism of L,(EqRelLATT FS) by Th14;
A46:
dom f = the carrier of L
by FUNCT_2:def 1;
A47:
Image f = subrelstr (rng f)
by YELLOW_2:def 2;
A48:
ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS )
proof
A49:
{ 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 A50:
Aq9,
dq9 is_extension_of A9,
d9
and A51:
the
ExtensionSeq of the
carrier of
L,
BasicDF L . 0 = [A9,d9]
and A52:
the
ExtensionSeq of the
carrier of
L,
BasicDF L . (0 + 1) = [Aq9,dq9]
by Def20;
(
A9 = the
carrier of
L &
d9 = BasicDF L )
by A2, A51, XTUPLE_0:1;
then consider q being
QuadrSeq of
BasicDF L such that A53:
Aq9 = NextSet (BasicDF L)
and A54:
dq9 = NextDelta q
by A50;
ConsecutiveSet ( the
carrier of
L,
{})
= the
carrier of
L
by Th21;
then reconsider Q =
Quadr (
q,
{}) as
Element of
[: the carrier of L, the carrier of L, the carrier of L, the carrier of L:] ;
A55:
( 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 A56:
{} in dom q
by Th25;
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 Def13;
then consider u,
v being
Element of the
carrier of
L,
a,
b being
Element of
L such that A57:
q . {} = [u,v,a,b]
and
(BasicDF L) . (
u,
v)
<= a "\/" b
;
consider e being
Equivalence_Relation of
FS such that A58:
e = f . b
and A59:
for
x,
y being
Element of
FS holds
(
[x,y] in e iff
FD . (
x,
y)
<= b )
by Def8;
A60:
Quadr (
q,
{})
= [u,v,a,b]
by A56, A57, Def14;
[Aq9,dq9] `2 = NextDelta q
by A54;
then A61:
NextDelta q c= FD
by A55, A52, ZFMISC_1:74;
A62:
{{ the carrier of L}} in {{ the carrier of L},{{ the carrier of L}},{{{ the carrier of L}}}}
by ENUMSET1:def 1;
then A63:
{{ 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 A46, A58, FUNCT_1:def 3;
hence
e in the
carrier of
(Image f)
by A47, YELLOW_0:def 15;
e <> id FS
A64:
( 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 }
;
[Aq9,dq9] `1 = NextSet (BasicDF L)
by A53;
then A65:
NextSet (BasicDF L) c= FS
by A64, A52, ZFMISC_1:74;
new_set the
carrier of
L =
new_set (ConsecutiveSet ( the carrier of L,{}))
by Th21
.=
ConsecutiveSet ( the
carrier of
L,
(succ {}))
by Th22
;
then
new_set the
carrier of
L c= NextSet (BasicDF L)
by Lm4, Th29;
then A66:
new_set the
carrier of
L c= FS
by A65;
A67:
{{ the carrier of L}} in new_set the
carrier of
L
by A62, XBOOLE_0:def 3;
A68:
{ 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 A66, A67;
A69:
(
ConsecutiveSet ( the
carrier of
L,
{})
= the
carrier of
L &
ConsecutiveDelta (
q,
{})
= BasicDF L )
by Th21, Th26;
ConsecutiveDelta (
q,
(succ {})) =
new_bi_fun (
(BiFun ((ConsecutiveDelta (q,{})),(ConsecutiveSet ( the carrier of L,{})),L)),
(Quadr (q,{})))
by Th27
.=
new_bi_fun (
(BasicDF L),
Q)
by A69, Def15
;
then
new_bi_fun (
(BasicDF L),
Q)
c= NextDelta q
by Lm4, Th32;
then A70:
new_bi_fun (
(BasicDF L),
Q)
c= FD
by A61;
(
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 A68, 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 A63, ZFMISC_1:87;
then FD . (
W,
V) =
(new_bi_fun ((BasicDF L),Q)) . (
{ the carrier of L},
{{ the carrier of L}})
by A70, GRFUNC_1:2
.=
Q `4_4
by Def10
.=
b
by A60
;
then
[{ the carrier of L},{{ the carrier of L}}] in e
by A59;
hence
e <> id FS
by A49, 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 Th40;
then A71:
rng (BasicDF L) = the carrier of L
by FUNCT_2:def 3;
for w being object st w in the carrier of L holds
ex z being object st
( z in [:FS,FS:] & w = FD . z )
proof
let w be
object ;
( w in the carrier of L implies ex z being object st
( z in [:FS,FS:] & w = FD . z ) )
A72:
( 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 }
;
A73:
( 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 }
;
A74:
the
ExtensionSeq of the
carrier of
L,
BasicDF L . 0 = [ the carrier of L,(BasicDF L)]
by Def20;
A75:
BasicDF L c= FD
by A73, A74, ZFMISC_1:74;
assume
w in the
carrier of
L
;
ex z being object st
( z in [:FS,FS:] & w = FD . z )
then consider z being
object such that A76:
z in [: the carrier of L, the carrier of L:]
and A77:
(BasicDF L) . z = w
by A71, FUNCT_2:11;
take
z
;
( z in [:FS,FS:] & w = FD . z )
the
carrier of
L c= FS
by A72, 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 A76;
w = FD . z
z in dom (BasicDF L)
by A76, FUNCT_2:def 1;
hence
w = FD . z
by A77, A75, 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 Th15; type_of (Image f) <= 3
for e1, e2 being Equivalence_Relation of FS
for x, y being object 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 Th43;
hence
type_of (Image f) <= 3
by A48, Th13; verum