let L be lower-bounded LATTICE; :: thesis: 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;
A1:
BasicDF L is onto
by Th43;
consider S being ExtensionSeq of the carrier of L, BasicDF L;
set FS = union { ((S . i) `1 ) where i is Element of NAT : verum } ;
A2:
S . 0 = [the carrier of L,(BasicDF L)]
by Def21;
then A3:
(S . 0 ) `1 = the carrier of L
by MCART_1:def 1;
(S . 0 ) `1 in { ((S . i) `1 ) where i is Element of NAT : verum }
;
then A4:
the carrier of L c= union { ((S . i) `1 ) where i is Element of NAT : verum }
by A3, ZFMISC_1:92;
reconsider FS = union { ((S . i) `1 ) where i is Element of NAT : verum } as non empty set by A4;
reconsider FD = union { ((S . i) `2 ) where i is Element of NAT : verum } as distance_function of FS,L by Th44;
A6:
FD is onto
proof
A7:
rng (BasicDF L) = the
carrier of
L
by A1, 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 ;
:: thesis: ( w in the carrier of L implies ex z being set st
( z in [:FS,FS:] & w = FD . z ) )
assume
w in the
carrier of
L
;
:: thesis: ex z being set st
( z in [:FS,FS:] & w = FD . z )
then consider z being
set such that A8:
z in [:the carrier of L,the carrier of L:]
and A9:
(BasicDF L) . z = w
by A7, FUNCT_2:17;
take
z
;
:: thesis: ( z in [:FS,FS:] & w = FD . z )
A10:
S . 0 = [the carrier of L,(BasicDF L)]
by Def21;
then A11:
the
carrier of
L = (S . 0 ) `1
by MCART_1:def 1;
(S . 0 ) `1 in { ((S . i) `1 ) where i is Element of NAT : verum }
;
then
the
carrier of
L c= FS
by A11, ZFMISC_1:92;
then
[:the carrier of L,the carrier of L:] c= [:FS,FS:]
by ZFMISC_1:119;
hence
z in [:FS,FS:]
by A8;
:: thesis: w = FD . z
A12:
z in dom (BasicDF L)
by A8, FUNCT_2:def 1;
A13:
BasicDF L = (S . 0 ) `2
by A10, MCART_1:def 2;
(S . 0 ) `2 in { ((S . i) `2 ) where i is Element of NAT : verum }
;
then
BasicDF L c= FD
by A13, ZFMISC_1:92;
hence
w = FD . z
by A9, A12, GRFUNC_1:8;
:: thesis: verum
end;
then
rng FD = the
carrier of
L
by FUNCT_2:16;
hence
FD is
onto
by FUNCT_2:def 3;
:: thesis: verum
end;
alpha FD is join-preserving
proof
let a,
b be
Element of
L;
:: according to WAYBEL_0:def 35 :: thesis: alpha FD preserves_sup_of {a,b}
set f =
alpha FD;
A14:
ex_sup_of (alpha FD) .: {a,b},
EqRelLATT FS
by YELLOW_0:17;
A15:
dom (alpha FD) = the
carrier of
L
by FUNCT_2:def 1;
consider e1 being
Equivalence_Relation of
FS such that A16:
e1 = (alpha FD) . a
and A17:
for
x,
y being
Element of
FS holds
(
[x,y] in e1 iff
FD . x,
y <= a )
by Def9;
consider e2 being
Equivalence_Relation of
FS such that A18:
e2 = (alpha FD) . b
and A19:
for
x,
y being
Element of
FS holds
(
[x,y] in e2 iff
FD . x,
y <= b )
by Def9;
consider e3 being
Equivalence_Relation of
FS such that A20:
e3 = (alpha FD) . (a "\/" b)
and A21:
for
x,
y being
Element of
FS holds
(
[x,y] in e3 iff
FD . x,
y <= a "\/" b )
by Def9;
A22:
field e1 = FS
by ORDERS_1:97;
A23:
field e2 = FS
by ORDERS_1:97;
A24:
field e3 = FS
by ORDERS_1:97;
A25:
e1 "\/" e2 c= e3
proof
now let x,
y be
set ;
:: thesis: ( [x,y] in e1 implies [x,y] in e3 )assume A26:
[x,y] in e1
;
:: thesis: [x,y] in e3then reconsider x' =
x,
y' =
y as
Element of
FS by A22, RELAT_1:30;
A27:
FD . x',
y' <= a
by A17, A26;
a <= a "\/" b
by YELLOW_0:22;
then
FD . x',
y' <= a "\/" b
by A27, ORDERS_2:26;
hence
[x,y] in e3
by A21;
:: thesis: verum end;
then A28:
e1 c= e3
by RELAT_1:def 3;
now let x,
y be
set ;
:: thesis: ( [x,y] in e2 implies [x,y] in e3 )assume A29:
[x,y] in e2
;
:: thesis: [x,y] in e3then reconsider x' =
x,
y' =
y as
Element of
FS by A23, RELAT_1:30;
A30:
FD . x',
y' <= b
by A19, A29;
b <= b "\/" a
by YELLOW_0:22;
then
FD . x',
y' <= b "\/" a
by A30, ORDERS_2:26;
hence
[x,y] in e3
by A21;
:: thesis: verum end;
then
e2 c= e3
by RELAT_1:def 3;
then
e1 \/ e2 c= e3
by A28, XBOOLE_1:8;
hence
e1 "\/" e2 c= e3
by EQREL_1:def 3;
:: thesis: verum
end;
A31:
e3 c= e1 "\/" e2
proof
for
u,
v being
set st
[u,v] in e3 holds
[u,v] in e1 "\/" e2
proof
let u,
v be
set ;
:: thesis: ( [u,v] in e3 implies [u,v] in e1 "\/" e2 )
assume A32:
[u,v] in e3
;
:: thesis: [u,v] in e1 "\/" e2
then reconsider x =
u,
y =
v as
Element of
FS by A24, RELAT_1:30;
A33:
u in FS
by A24, A32, RELAT_1:30;
FD . x,
y <= a "\/" b
by A21, A32;
then consider z1,
z2,
z3 being
Element of
FS such that A34:
FD . x,
z1 = a
and A35:
FD . z2,
z3 = a
and A36:
FD . z1,
z2 = b
and A37:
FD . z3,
y = b
by Th45;
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 ) );
A39:
for
m being
Nat st
m in Seg 5 holds
ex
w being
set st
S1[
m,
w]
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(A39);
then consider h being
FinSequence such that A46:
dom h = Seg 5
and A47:
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 ) )
;
A48:
( 1
in Seg 5 & 2
in Seg 5 & 3
in Seg 5 & 4
in Seg 5 & 5
in Seg 5 )
;
A49:
len h = 5
by A46, FINSEQ_1:def 3;
A50:
u = h . 1
by A47, A48;
A51:
v =
h . 5
by A47, A48
.=
h . (len h)
by A46, FINSEQ_1:def 3
;
for
j being
Element of
NAT st 1
<= j &
j < len h holds
[(h . j),(h . (j + 1))] in e1 \/ e2
hence
[u,v] in e1 "\/" e2
by A33, A49, A50, A51, EQREL_1:36;
:: thesis: verum
end;
hence
e3 c= e1 "\/" e2
by RELAT_1:def 3;
:: thesis: verum
end;
sup ((alpha FD) .: {a,b}) =
sup {((alpha FD) . a),((alpha FD) . b)}
by A15, FUNCT_1:118
.=
((alpha FD) . a) "\/" ((alpha FD) . b)
by YELLOW_0:41
.=
e1 "\/" e2
by A16, A18, Th10
.=
(alpha FD) . (a "\/" b)
by A20, A25, A31, XBOOLE_0:def 10
.=
(alpha FD) . (sup {a,b})
by YELLOW_0:41
;
hence
alpha FD preserves_sup_of {a,b}
by A14, WAYBEL_0:def 31;
:: thesis: verum
end;
then reconsider f = alpha FD as Homomorphism of L,(EqRelLATT FS) by Th16;
take
FS
; :: thesis: ex f being Homomorphism of L,(EqRelLATT FS) st
( f is one-to-one & type_of (Image f) <= 3 )
take
f
; :: thesis: ( f is one-to-one & type_of (Image f) <= 3 )
thus
f is one-to-one
by A6, Th17; :: thesis: type_of (Image f) <= 3
A57:
Image f = subrelstr (rng f)
by YELLOW_2:def 2;
A58:
dom f = the carrier of L
by FUNCT_2:def 1;
A59:
ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS )
proof
consider A' being non
empty set ,
d' being
distance_function of
A',
L,
Aq' being non
empty set ,
dq' being
distance_function of
Aq',
L such that A60:
Aq',
dq' is_extension_of A',
d'
and A61:
(
S . 0 = [A',d'] &
S . (0 + 1) = [Aq',dq'] )
by Def21;
(
A' = the
carrier of
L &
d' = BasicDF L )
by A2, A61, ZFMISC_1:33;
then consider q being
QuadrSeq of
BasicDF L such that A62:
Aq' = NextSet (BasicDF L)
and A63:
dq' = NextDelta q
by A60, Def20;
A64:
(S . 1) `2 = NextDelta q
by A61, A63, MCART_1:def 2;
(S . 1) `2 in { ((S . i) `2 ) where i is Element of NAT : verum }
;
then A65:
NextDelta q c= FD
by A64, ZFMISC_1:92;
A66:
(S . 1) `1 = NextSet (BasicDF L)
by A61, A62, MCART_1:def 1;
(S . 1) `1 in { ((S . i) `1 ) where i is Element of NAT : verum }
;
then A67:
NextSet (BasicDF L) c= FS
by A66, ZFMISC_1:92;
succ {} c= DistEsti (BasicDF L)
by Lm4;
then
{} in DistEsti (BasicDF L)
by ORDINAL1:33;
then A68:
{} in dom q
by Th28;
then
q . {} in rng q
by FUNCT_1:def 5;
then
q . {} in { [u,v,a',b'] where u, v is Element of the carrier of L, a', b' is Element of L : (BasicDF L) . u,v <= a' "\/" b' }
by Def14;
then consider u,
v being
Element of the
carrier of
L,
a,
b being
Element of
L such that A69:
(
q . {} = [u,v,a,b] &
(BasicDF L) . u,
v <= a "\/" b )
;
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:] ;
A70:
Quadr q,
{} = [u,v,a,b]
by A68, A69, Def15;
consider e being
Equivalence_Relation of
FS such that A71:
e = f . b
and A72:
for
x,
y being
Element of
FS holds
(
[x,y] in e iff
FD . x,
y <= b )
by Def9;
take
e
;
:: thesis: ( e in the carrier of (Image f) & e <> id FS )
e in rng f
by A58, A71, FUNCT_1:def 5;
hence
e in the
carrier of
(Image f)
by A57, YELLOW_0:def 15;
:: thesis: e <> id FS
new_set the
carrier of
L =
new_set (ConsecutiveSet the carrier of L,{} )
by Th24
.=
ConsecutiveSet the
carrier of
L,
(succ {} )
by Th25
;
then A73:
new_set the
carrier of
L c= NextSet (BasicDF L)
by Lm4, Th32;
A74:
(
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 A74, Def16
;
then
new_bi_fun (BasicDF L),
Q c= NextDelta q
by Lm4, Th35;
then A75:
new_bi_fun (BasicDF L),
Q c= FD
by A65, XBOOLE_1:1;
A76:
new_set the
carrier of
L c= FS
by A67, A73, XBOOLE_1:1;
A77:
dom (new_bi_fun (BasicDF L),Q) = [:(new_set the carrier of L),(new_set the carrier of L):]
by FUNCT_2:def 1;
A78:
{the carrier of L} in {{the carrier of L},{{the carrier of L}},{{{the carrier of L}}}}
by ENUMSET1:def 1;
then A79:
{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;
A80:
{the carrier of L} in new_set the
carrier of
L
by A78, XBOOLE_0:def 3;
A81:
{{the carrier of L}} in {{the carrier of L},{{the carrier of L}},{{{the carrier of L}}}}
by ENUMSET1:def 1;
then A82:
{{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;
A83:
{{the carrier of L}} in new_set the
carrier of
L
by A81, XBOOLE_0:def 3;
A84:
[{the carrier of L},{{the carrier of L}}] in dom (new_bi_fun (BasicDF L),Q)
by A77, A80, A82, ZFMISC_1:106;
reconsider W =
{the carrier of L},
V =
{{the carrier of L}} as
Element of
FS by A76, A79, A83;
FD . W,
V =
(new_bi_fun (BasicDF L),Q) . {the carrier of L},
{{the carrier of L}}
by A75, A84, GRFUNC_1:8
.=
Q `4
by Def11
.=
b
by A70, MCART_1:def 11
;
then A85:
[{the carrier of L},{{the carrier of L}}] in e
by A72;
{the carrier of L} <> {{the carrier of L}}
hence
e <> id FS
by A85, RELAT_1:def 10;
:: thesis: verum
end;
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 A59, Th15; :: thesis: verum