:: J\'onsson Theorem about Representation of Modular Lattices
:: by Mariusz {\L}api\'nski
::
:: Received June 29, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDERS_2, XBOOLE_0, STRUCT_0, EQREL_1, SUBSET_1,
FINSEQ_1, LATTICE5, LATTICES, WAYBEL_0, ZFMISC_1, GROUP_6, FUNCT_1,
RELAT_1, XXREAL_0, FINSET_1, ABIAN, CARD_1, ARYTM_3, CAT_1, YELLOW_0,
ORDINAL2, ORDINAL1, TARSKI, WELLORD1, SEQM_3, LATTICE3, WAYBEL_1,
MCART_1, VALUED_0, RELAT_2, PARTFUN1, FUNCOP_1, FUNCT_6, NAT_1, FUNCT_2,
LATTICE8, RECDEF_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1,
FUNCT_1, RELSET_1, FUNCT_2, FUNCT_6, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
ORDINAL2, MCART_1, DOMAIN_1, PARTFUN1, FUNCOP_1, STRUCT_0, ORDERS_2,
EQREL_1, FINSEQ_1, LATTICE3, BINOP_1, YELLOW_0, YELLOW_2, LATTICE5,
YELLOW11, WAYBEL_1, WAYBEL_0, ABIAN, XXREAL_0;
constructors ORDINAL2, FUNCT_6, RFUNCT_3, ABIAN, REALSET2, ORDERS_3, WAYBEL_1,
LATTICE5, YELLOW11, RELSET_1, XTUPLE_0, NUMBERS, XFAMILY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1,
XREAL_0, INT_1, CARD_1, FINSEQ_1, EQREL_1, ABIAN, STRUCT_0, LATTICE3,
YELLOW_0, YELLOW_2, WAYBEL_1, WAYBEL10, LATTICE5, YELLOW11, WAYBEL21,
LATTICE7, ZFMISC_1, FUNCT_1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, LATTICE3, FUNCOP_1, WAYBEL_0, YELLOW_0, YELLOW11,
LATTICE5, XBOOLE_0, RELSET_1;
equalities TARSKI, BINOP_1, YELLOW_2, ORDINAL1;
expansions TARSKI, LATTICE3, WAYBEL_0, YELLOW11, LATTICE5, XBOOLE_0, BINOP_1,
RELSET_1, ORDINAL1;
theorems EQREL_1, RELAT_1, RELAT_2, FINSEQ_1, FINSEQ_2, ORDERS_2, TARSKI,
ORDINAL1, ORDINAL3, TREES_2, PARTFUN1, GRFUNC_1, FUNCT_6, NAT_1,
ZFMISC_1, FUNCT_1, FUNCT_2, LATTICE3, YELLOW_0, YELLOW_3, YELLOW_5,
WAYBEL_0, WAYBEL_1, WAYBEL_6, RELSET_1, LATTICE5, YELLOW11, WAYBEL13,
ORDERS_3, TEX_1, SYSREL, XBOOLE_0, XBOOLE_1, ORDERS_1, STRUCT_0,
XTUPLE_0, XREGULAR;
schemes RECDEF_1, ORDINAL2, NAT_1, FINSEQ_1, BINOP_1, CLASSES1;
begin :: Preliminaries
definition
let L be RelStr;
attr L is finitely_typed means
:Def1:
ex A being non empty set st
(for e being object
st e in the carrier of L holds e is Equivalence_Relation of A) & ex o
being Element of NAT st
for e1,e2 being Equivalence_Relation of A, x,y being object
st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2
holds ex F being non empty FinSequence of A st len F = o & x,y are_joint_by F,
e1,e2;
end;
definition
let L be lower-bounded LATTICE;
let n be Element of NAT;
pred L has_a_representation_of_type<= n means
ex A being non trivial
set, f be Homomorphism of L,EqRelLATT A st f is one-to-one & Image f is
finitely_typed & (ex e being Equivalence_Relation of A st e in the carrier of
Image f & e <> id A) & type_of Image f <= n;
end;
registration
cluster lower-bounded distributive finite for LATTICE;
existence
proof
set L = the distributive finite LATTICE;
take L;
thus thesis;
end;
end;
Lm1: 1 is odd
proof
2*0+1 = 1;
hence thesis;
end;
Lm2: 2 is even
proof
2*1 = 2;
hence thesis;
end;
registration
let A be non trivial set;
cluster non trivial finitely_typed full for
non empty Sublattice of EqRelLATT A;
existence
proof
reconsider e1 = nabla A, e2 = id A as Element of EqRelLATT A by LATTICE5:4;
set a = the Element of A;
set b = the Element of A\{a};
set Y = subrelstr {e1,e2};
A1: the carrier of Y = {e1,e2} by YELLOW_0:def 15;
e1 = [:A,A:] by EQREL_1:def 1;
then
A2: e2 <= e1 by LATTICE5:6;
A3: for x,y being Element of EqRelLATT A st x in the carrier of Y & y in
the carrier of Y & ex_inf_of {x,y},EqRelLATT A holds inf {x,y} in the carrier
of Y
proof
let x,y be Element of EqRelLATT A;
assume that
A4: x in the carrier of Y & y in the carrier of Y and
ex_inf_of {x,y},EqRelLATT A;
per cases by A1,A4,TARSKI:def 2;
suppose
x = e1 & y = e1;
then inf {x,y} = e1"/\"e1 by YELLOW_0:40
.= e1 by YELLOW_5:2;
hence thesis by A1,TARSKI:def 2;
end;
suppose
x = e1 & y = e2;
then inf {x,y} = e1"/\"e2 by YELLOW_0:40
.= e2 by A2,YELLOW_5:10;
hence thesis by A1,TARSKI:def 2;
end;
suppose
x = e2 & y = e1;
then inf {x,y} = e2"/\"e1 by YELLOW_0:40
.= e2 by A2,YELLOW_5:10;
hence thesis by A1,TARSKI:def 2;
end;
suppose
x = e2 & y = e2;
then inf {x,y} = e2"/\"e2 by YELLOW_0:40
.= e2 by YELLOW_5:2;
hence thesis by A1,TARSKI:def 2;
end;
end;
A5: Y is finitely_typed
proof
take A;
thus for e being object st e in the carrier of Y holds e is
Equivalence_Relation of A by A1,TARSKI:def 2;
take o = 3;
thus for eq1,eq2 being Equivalence_Relation of A,
x1,y1 being object st eq1
in the carrier of Y & eq2 in the carrier of Y & [x1,y1] in eq1 "\/" eq2 holds
ex F being non empty FinSequence of A st len F = o & x1,y1 are_joint_by F,eq1,
eq2
proof
let eq1,eq2 be Equivalence_Relation of A;
let x1,y1 be object;
assume that
A6: eq1 in the carrier of Y and
A7: eq2 in the carrier of Y and
A8: [x1,y1] in eq1 "\/" eq2;
eq1 = e2 or eq1 <> e2;
then consider z being object such that
A9: eq1 = e2 & z = x1 or eq1 <> e2 & z = y1;
ex x2,y2 being object st [x1,y1] = [x2,y2] & x2 in A & y2 in A by A8,
RELSET_1:2;
then x1 in A & y1 in A by XTUPLE_0:1;
then reconsider F = <*x1,z,y1*> as non empty FinSequence of A by A9,
FINSEQ_2:14;
take F;
per cases by A9;
suppose
A10: eq1 = e2 & z = x1;
then
A11: F.2 = x1;
A13: for i being Element of NAT st 1 <= i & i < len F holds (i is
odd implies [F.i,F.(i+1)] in eq1) & (i is even implies [F.i,F.(i+1)] in eq2)
proof
let i be Element of NAT;
assume that
A14: 1 <= i and
A15: i < len F;
i < 2+1 by A15,FINSEQ_1:45;
then i <= 2 by NAT_1:13;
then
A16: i = 0 or ... or i = 2 by NAT_1:60;
per cases by A1,A7,A10,A14,A16,Lm1,Lm2,TARSKI:def 2;
suppose
A17: i = 1 & i is odd & eq1 = e2 & eq2 = e1;
ex x2,y2 being object st [x1,y1] = [x2,y2] & x2 in A & y2 in A
by A8,RELSET_1:2;
then x1 in A by XTUPLE_0:1;
hence thesis by A11,A17,EQREL_1:5;
end;
suppose
A18: i = 1 & i is odd & eq1 = e2 & eq2 = e2;
ex x2,y2 being object st [x1,y1] = [x2,y2] & x2 in A & y2 in A
by A8,RELSET_1:2;
then x1 in A by XTUPLE_0:1;
hence thesis by A11,A18,EQREL_1:5;
end;
suppose
A19: i = 2 & i is even & eq1 = e2 & eq2 = e1;
then eq1 "\/" eq2 = e2 "\/" e1 by LATTICE5:10
.= eq2 by A2,A19,YELLOW_5:8;
hence thesis by A8,A11,A19;
end;
suppose
i = 2 & i is even & eq1 = e2 & eq2 = e2;
hence thesis by A8,A11;
end;
end;
len F = 3 & F.3 = y1 by FINSEQ_1:45;
hence thesis by A13;
end;
suppose
A20: eq1 <> e2 & z = y1;
then
A21: F.2 = y1;
A23: for i being Element of NAT st 1 <= i & i < len F holds (i is
odd implies [F.i,F.(i+1)] in eq1) & (i is even implies [F.i,F.(i+1)] in eq2)
proof
let i be Element of NAT;
assume that
A24: 1 <= i and
A25: i < len F;
i < 2+1 by A25,FINSEQ_1:45;
then i <= 2 by NAT_1:13;
then
A26: i = 0 or ... or i = 2 by NAT_1:60;
per cases by A1,A6,A7,A20,A24,A26,Lm1,Lm2,TARSKI:def 2;
suppose
i = 1 & i is odd & eq1 = e1 & eq2 = e1;
hence thesis by A8,A21;
end;
suppose
A27: i = 1 & i is odd & eq1 = e1 & eq2 = e2;
then eq1 "\/" eq2 = e1 "\/" e2 by LATTICE5:10
.= eq1 by A2,A27,YELLOW_5:8;
hence thesis by A8,A21,A27;
end;
suppose
A28: i = 2 & i is even & eq1 = e1 & eq2 = e1;
ex x2,y2 being object st [x1,y1] = [x2,y2] & x2 in A & y2 in A
by A8,RELSET_1:2;
then y1 in A by XTUPLE_0:1;
hence thesis by A21,A28,EQREL_1:5;
end;
suppose
A29: i = 2 & i is even & eq1 = e1 & eq2 = e2;
ex x2,y2 being object st [x1,y1] = [x2,y2] & x2 in A & y2 in A
by A8,RELSET_1:2;
then y1 in A by XTUPLE_0:1;
hence thesis by A21,A29,EQREL_1:5;
end;
end;
len F = 3 & F.1 = x1 by FINSEQ_1:45;
hence thesis by A23;
end;
end;
end;
A30: for x,y being Element of EqRelLATT A st x in the carrier of Y & y in
the carrier of Y & ex_sup_of {x,y},EqRelLATT A holds sup {x,y} in the carrier
of Y
proof
let x,y be Element of EqRelLATT A;
assume that
A31: x in the carrier of Y & y in the carrier of Y and
ex_sup_of {x,y},EqRelLATT A;
per cases by A1,A31,TARSKI:def 2;
suppose
x = e1 & y = e1;
then sup {x,y} = e1"\/"e1 by YELLOW_0:41
.= e1 by YELLOW_5:1;
hence thesis by A1,TARSKI:def 2;
end;
suppose
x = e1 & y = e2;
then sup {x,y} = e1"\/"e2 by YELLOW_0:41
.= e1 by A2,YELLOW_5:8;
hence thesis by A1,TARSKI:def 2;
end;
suppose
x = e2 & y = e1;
then sup {x,y} = e2"\/"e1 by YELLOW_0:41
.= e1 by A2,YELLOW_5:8;
hence thesis by A1,TARSKI:def 2;
end;
suppose
x = e2 & y = e2;
then sup {x,y} = e2"\/"e2 by YELLOW_0:41
.= e2 by YELLOW_5:1;
hence thesis by A1,TARSKI:def 2;
end;
end;
A32: a <> b by ZFMISC_1:56;
A33: Y is non trivial
proof
assume Y is trivial;
then ex s being Element of Y st the carrier of Y = {s} by TEX_1:def 1;
then nabla A = id A by A1,ZFMISC_1:5;
then [:A,A:] = id A by EQREL_1:def 1;
then [a,b] in id A by ZFMISC_1:def 2;
hence contradiction by A32,RELAT_1:def 10;
end;
reconsider Y as full non empty Sublattice of EqRelLATT A by A3,A30,
YELLOW_0:def 16,def 17;
take Y;
thus thesis by A33,A5;
end;
end;
theorem Th1:
for A be non empty set for L be lower-bounded LATTICE for d be
distance_function of A,L holds succ {} c= DistEsti(d)
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
succ {} c= DistEsti(d) or DistEsti(d) in succ {} by ORDINAL1:16;
then succ {} c= DistEsti(d) or DistEsti(d) c= {} by ORDINAL1:22;
hence thesis by LATTICE5:20,XBOOLE_1:3;
end;
theorem
for L being trivial Semilattice holds L is modular
by STRUCT_0:def 10;
theorem
for A being non empty set for L being non empty Sublattice of
EqRelLATT A holds L is trivial or ex e being Equivalence_Relation of A st e in
the carrier of L & e <> id A
proof
let A be non empty set;
let L be non empty Sublattice of EqRelLATT A;
now
assume
A1: not ex e being Equivalence_Relation of A st e in the carrier of L
& e <> id A;
thus L is trivial
proof
consider x be object such that
A2: x in the carrier of L by XBOOLE_0:def 1;
the carrier of L c= the carrier of EqRelLATT A by YELLOW_0:def 13;
then reconsider e=x as Equivalence_Relation of A by A2,LATTICE5:4;
the carrier of L = {x}
proof
thus the carrier of L c= {x}
proof
let a be object;
assume
A3: a in the carrier of L;
the carrier of L c= the carrier of EqRelLATT A by YELLOW_0:def 13;
then reconsider B=a as Equivalence_Relation of A by A3,LATTICE5:4;
B = id A by A1,A3
.= e by A1,A2;
hence thesis by TARSKI:def 1;
end;
let A be object;
assume A in {x};
hence thesis by A2,TARSKI:def 1;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for L1,L2 be lower-bounded LATTICE for f being Function of L1,L2
st f is infs-preserving sups-preserving holds f is meet-preserving
join-preserving;
theorem Th5:
for L1,L2 be lower-bounded LATTICE st L1,L2 are_isomorphic & L1
is modular holds L2 is modular
proof
let L1,L2 be lower-bounded LATTICE;
assume that
A1: L1,L2 are_isomorphic and
A2: L1 is modular;
let a,b,c be Element of L2;
consider f be Function of L1,L2 such that
A3: f is isomorphic by A1,WAYBEL_1:def 8;
set C = f".c;
set A = f".a;
set B = f".b;
A4: f is one-to-one & rng f = the carrier of L2 by A3,WAYBEL_0:66;
then
A5: b = f.B by FUNCT_1:35;
A6: C in dom f by A4,FUNCT_1:32;
A7: A in dom f & B in dom f by A4,FUNCT_1:32;
A8: a = f.A & c = f.C by A4,FUNCT_1:35;
reconsider A,B,C as Element of L1 by A7,A6;
assume a <= c;
then A <= C by A3,A8,WAYBEL_0:66;
then
A9: A"\/"(B"/\"C) = (A"\/"B)"/\"C by A2;
f is infs-preserving sups-preserving by A3,WAYBEL13:20;
then
A10: f is meet-preserving join-preserving;
hence a"\/"(b"/\"c) = f.A "\/" f.(B"/\"C) by A5,A8,WAYBEL_6:1
.= f.((A"\/"B)"/\"C) by A10,A9,WAYBEL_6:2
.= (f.(A"\/"B)"/\"f.C) by A10,WAYBEL_6:1
.= (a"\/"b)"/\"c by A10,A5,A8,WAYBEL_6:2;
end;
theorem Th6:
for S being lower-bounded non empty Poset for T being non empty
Poset for f being monotone Function of S,T holds Image f is lower-bounded
proof
let S be lower-bounded non empty Poset;
let T be non empty Poset;
let f be monotone Function of S,T;
thus Image f is lower-bounded
proof
consider x being Element of S such that
A1: x is_<=_than the carrier of S by YELLOW_0:def 4;
dom f = the carrier of S by FUNCT_2:def 1;
then f.x in rng f by FUNCT_1:def 3;
then reconsider fx = f.x as Element of Image f by YELLOW_0:def 15;
take fx;
let b be Element of Image f;
b in the carrier of subrelstr (rng f);
then b in rng f by YELLOW_0:def 15;
then consider c be object such that
A2: c in dom f and
A3: f.c = b by FUNCT_1:def 3;
A4: the carrier of Image f c= the carrier of T by YELLOW_0:def 13;
assume b in the carrier of Image f;
reconsider b1 = b as Element of T by A4;
reconsider c as Element of S by A2;
x <= c by A1;
then f.x <= b1 by A3,ORDERS_3:def 5;
hence fx <= b by YELLOW_0:60;
end;
end;
theorem Th7:
for L being lower-bounded LATTICE for x,y being Element of L for
A being non empty set for f be Homomorphism of L,EqRelLATT A st f is one-to-one
holds (corestr f).x <= (corestr f).y implies x <= y
proof
let L be lower-bounded LATTICE;
let x,y be Element of L;
let A be non empty set;
let f be Homomorphism of L,EqRelLATT A;
assume that
A1: f is one-to-one and
A2: (corestr f).x <= (corestr f).y;
now
A3: corestr f = f by WAYBEL_1:30;
A4: for x,y being Element of L holds (corestr f).(x "/\" y) = (corestr f).
x "/\" (corestr f).y
proof
let x,y be Element of L;
thus (corestr f).(x "/\" y) = f.x "/\" f.y by A3,WAYBEL_6:1
.= (corestr f).x "/\" (corestr f).y by A3,YELLOW_0:69;
end;
A5: corestr f is one-to-one by A1,WAYBEL_1:30;
(corestr f).y "/\" (corestr f).x = (corestr f).x by A2,YELLOW_5:10;
then (corestr f).x = (corestr f).(x "/\" y) by A4;
then
A6: x = x "/\" y by A5,WAYBEL_1:def 1;
assume not x <= y;
hence contradiction by A6,YELLOW_0:25;
end;
hence thesis;
end;
begin
theorem Th8:
for A being non trivial set for L being finitely_typed full non
empty Sublattice of EqRelLATT A for e being Equivalence_Relation of A st e in
the carrier of L & e <> id A holds type_of L <= 2 implies L is modular
proof
let A be non trivial set;
let L be finitely_typed full non empty Sublattice of EqRelLATT A;
let e be Equivalence_Relation of A;
assume that
A1: e in the carrier of L and
A2: e <> id A;
assume
A3: type_of L <= 2;
let a,b,c be Element of L;
A4: the carrier of L c= the carrier of EqRelLATT A by YELLOW_0:def 13;
reconsider b9 = b as Equivalence_Relation of A by A4,LATTICE5:4;
reconsider b99 = b9 as Element of EqRelLATT A by A4;
reconsider a9 = a as Equivalence_Relation of A by A4,LATTICE5:4;
reconsider c9 = c as Equivalence_Relation of A by A4,LATTICE5:4;
reconsider c99 = c9 as Element of EqRelLATT A by A4;
reconsider a99 = a9 as Element of EqRelLATT A by A4;
A5: (a99"\/"b99)"/\"c99 = (a99"\/"b99) /\ c9 by LATTICE5:8
.= (a9"\/"b9) /\ c9 by LATTICE5:10;
assume
A6: a <= c;
then a99 <= c99 by YELLOW_0:59;
then
A7: a9 c= c9 by LATTICE5:6;
A8: a99"\/"(b99"/\"c99) <= (a99"\/"b99)"/\"c99 by A6,YELLOW11:8,YELLOW_0:59;
A9: b9 /\ c9 = b99"/\"c99 by LATTICE5:8;
then a9"\/"(b9 /\ c9) = a99"\/"(b99"/\"c99) by LATTICE5:10;
then
A10: a9"\/"(b9 /\ c9) c= (a9"\/"b9) /\ c9 by A8,A5,LATTICE5:6;
consider AA being non empty set such that
A11: for e being object st e in the carrier of L holds e is
Equivalence_Relation of AA and
A12: ex i being Element of NAT st for e1,e2 being Equivalence_Relation
of AA, x,y being object
st e1 in the carrier of L & e2 in the carrier of L & [x,y]
in e1 "\/" e2 holds ex F being non empty FinSequence of AA st len F = i & x,y
are_joint_by F,e1,e2 by Def1;
e is Equivalence_Relation of AA by A1,A11;
then
A13: field e = A & field e = AA by EQREL_1:9;
A14: (a9"\/"b9) /\ c9 c= a9"\/"(b9 /\ c9)
proof
let x,y be Element of A;
assume
A15: [x,y] in (a9 "\/" b9) /\ c9;
then
A16: [x,y] in a9 "\/" b9 by XBOOLE_0:def 4;
A17: [x,y] in c9 by A15,XBOOLE_0:def 4;
type_of L = 0 or ... or type_of L = 2 by A3,NAT_1:60;
then per cases;
suppose
type_of L = 2;
then consider F being non empty FinSequence of A such that
A18: len F = 2+2 and
A19: x,y are_joint_by F,a9,b9 by A1,A2,A12,A13,A16,LATTICE5:def 4;
A20: F.4 = y by A18,A19;
consider l being Element of NAT such that
A21: l = 1;
2*l+1 = 3 by A21;
then
A22: [F.3,F.(3+1)] in a9 by A18,A19;
consider k being Element of NAT such that
A23: k = 1;
2*k = 2 by A23;
then
A24: [F.2,F.(2+1)] in b9 by A18,A19;
A25: F.1 = x by A19;
reconsider BC = b9 /\ c9 as Element of EqRelLATT A by A9;
set z1 = F.2;
set z2 = F.3;
consider j being Element of NAT such that
A26: j = 0;
2*j+1 = 1 by A26;
then
A27: [F.1,F.(1+1)] in a9 by A18,A19;
A28: a9 "\/" (b9 /\ c9) = a99"\/" BC by LATTICE5:10;
BC <= BC "\/" a99 by YELLOW_0:22;
then
A29: b9 /\ c9 c= a9 "\/" (b9 /\ c9) by A28,LATTICE5:6;
a99 <= a99 "\/" BC by YELLOW_0:22;
then
A30: a9 c= a9 "\/" (b9 /\ c9) by A28,LATTICE5:6;
[y,x] in c9 by A17,EQREL_1:6;
then [z2,x] in c9 by A7,A20,A22,EQREL_1:7;
then [z2,z1] in c9 by A7,A25,A27,EQREL_1:7;
then [z1,z2] in c9 by EQREL_1:6;
then [z1,z2] in b9 /\ c9 by A24,XBOOLE_0:def 4;
then [x,z2] in a9 "\/" (b9 /\ c9) by A25,A27,A30,A29,EQREL_1:7;
hence thesis by A20,A22,A30,EQREL_1:7;
end;
suppose
type_of L = 1;
then consider F being non empty FinSequence of A such that
A31: len F = 1+2 and
A32: x,y are_joint_by F,a9,b9 by A1,A2,A12,A13,A16,LATTICE5:def 4;
set z1 = F.2;
consider k being Element of NAT such that
A33: k = 1;
reconsider BC = b9 /\ c9 as Element of EqRelLATT A by A9;
consider j being Element of NAT such that
A34: j = 0;
2*j+1 = 1 by A34;
then
A35: [F.1,F.(1+1)] in a9 by A31,A32;
2*k = 2 by A33;
then
A36: [F.2,F.(2+1)] in b9 by A31,A32;
A37: a9 "\/" (b9 /\ c9) = a99"\/" BC by LATTICE5:10;
A38: [x,y] in c9 by A15,XBOOLE_0:def 4;
A39: F.1 = x by A32;
then [z1,x] in c9 by A7,A35,EQREL_1:6;
then
A40: [z1,y] in c9 by A38,EQREL_1:7;
BC <= BC "\/" a99 by YELLOW_0:22;
then
A41: b9 /\ c9 c= a9 "\/" (b9 /\ c9) by A37,LATTICE5:6;
a99 <= a99 "\/" BC by YELLOW_0:22;
then
A42: a9 c= a9 "\/" (b9 /\ c9) by A37,LATTICE5:6;
F.3 = y by A31,A32;
then [z1,y] in b9 /\ c9 by A36,A40,XBOOLE_0:def 4;
hence thesis by A39,A35,A42,A41,EQREL_1:7;
end;
suppose
type_of L = 0;
then consider F being non empty FinSequence of A such that
A43: len F = 0+2 & x,y are_joint_by F,a9,b9 by A1,A2,A12,A13,A16,
LATTICE5:def 4;
reconsider BC = b9 /\ c9 as Element of EqRelLATT A by A9;
consider j being Element of NAT such that
A44: j = 0;
2*j+1 = 1 by A44;
then
A45: [F.1,F.(1+1)] in a9 by A43;
a99 <= a99 "\/" BC & a9 "\/" (b9 /\ c9) = a99"\/" BC by LATTICE5:10
,YELLOW_0:22;
then
A46: a9 c= a9 "\/" (b9 /\ c9) by LATTICE5:6;
F.1 = x & F.2 = y by A43;
hence thesis by A45,A46;
end;
end;
a99"\/"b99 = a"\/"b by YELLOW_0:70;
then
A47: (a"\/"b)"/\"c = (a99"\/"b99)"/\"c99 by YELLOW_0:69
.= (a99"\/"b99) /\ c9 by LATTICE5:8
.= (a9"\/"b9) /\ c9 by LATTICE5:10;
A48: b99"/\"c99 = b"/\"c by YELLOW_0:69;
a9"\/"(b9 /\ c9) = a99"\/"(b99"/\"c99) by A9,LATTICE5:10
.= a"\/"(b"/\"c) by A48,YELLOW_0:70;
hence thesis by A10,A14,A47;
end;
theorem Th9:
for L be lower-bounded LATTICE holds L
has_a_representation_of_type<= 2 implies L is modular
proof
let L be lower-bounded LATTICE;
assume L has_a_representation_of_type<= 2;
then consider
A being non trivial set, f being Homomorphism of L,EqRelLATT A such
that
A1: f is one-to-one and
A2: ( Image f is finitely_typed & ex e being Equivalence_Relation of A
st e in the carrier of Image f & e <> id A )& type_of Image f <= 2;
A3: rng (corestr f) = the carrier of Image f & for x,y being Element of L
holds x <= y implies (corestr f).x <= (corestr f).y by FUNCT_2:def 3
,WAYBEL_1:def 2;
corestr f is one-to-one & for x,y being Element of L holds (corestr f).x
<= (corestr f).y implies x <= y by A1,Th7,WAYBEL_1:30;
then corestr f is isomorphic by A3,WAYBEL_0:66;
then
A4: L, Image f are_isomorphic by WAYBEL_1:def 8;
A5: Image f is lower-bounded LATTICE by Th6;
Image f is modular by A2,Th8;
hence thesis by A5,A4,Th5,WAYBEL_1:6;
end;
:: <= :: L is modular implies L has_a_representation_of_type<= 2
definition
let A be set;
func new_set2 A -> set equals
A \/ {{A}, {{A}}};
correctness;
end;
registration
let A be set;
cluster new_set2 A -> non empty;
coherence;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
func new_bi_fun2(d,q) -> BiFunction of new_set2 A,L means
:Def4:
(for u,v being Element of A holds it.(u,v) = d.(u,v)) &
it.({A},{A}) = Bottom L & it.({{A}},{{A}}) = Bottom L &
it.({A},{{A}}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) &
it.({{A}
},{A}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) &
for u being Element of A
holds it.(u,{A}) = d.(u,q`1_4)"\/"(q`3_4) &
it.({A},u) = d.(u,q`1_4)"\/"(q`3_4) &
it.(u,{{A}}) = d.(u,q`2_4) "\/"(q`3_4) &
it.({{A}},u) = d.(u,q`2_4)"\/"(q`3_4);
existence
proof
reconsider a = q`3_4, b = q`4_4 as Element of L;
set x = q`1_4, y = q`2_4;
defpred X[Element of new_set2 A,Element of new_set2 A,set] means ($1 in A
& $2 in A implies $3 = d.($1,$2)) & ($1 = {A} & $2 = {{A}} or $2 = {A} & $1 = {
{A}} implies $3 = (d.(x,y)"\/"a)"/\"b) & (($1 = {A} or $1 = {{A}}) & $2 = $1
implies $3 = Bottom L) & ($1 in A & $2 = {A} implies ex p9 being Element of A
st p9 = $1 & $3 = d.(p9,x)"\/"a) & ($1 in A & $2 = {{A}} implies ex p9 being
Element of A st p9 = $1 & $3 = d.(p9,y)"\/"a) & ($2 in A & $1 = {A} implies ex
q9 being Element of A st q9 = $2 & $3 = d.(q9,x)"\/"a) & ($2 in A & $1 = {{A}}
implies ex q9 being Element of A st q9 = $2 & $3 = d.(q9,y)"\/"a);
{{A}} in {{A}, {{A}} } by TARSKI:def 2;
then
A1: {{A}} in new_set2 A by XBOOLE_0:def 3;
A2: for p,q being Element of new_set2 A ex r being Element of L st X[p,q,r ]
proof
let p,q be Element of new_set2 A;
A3: p in A or p in {{A},{{A}}} by XBOOLE_0:def 3;
A4: q in A or q in {{A},{{A}}} by XBOOLE_0:def 3;
A5: (p = {A} or p = {{A}}) & p = q iff p = {A} & q = {A} or p = {{A}} &
q = {{A}};
A6: not {A} in A by TARSKI:def 1;
A7: {A} <> {{A}}
proof
assume {A} = {{A}};
then {A} in {A} by TARSKI:def 1;
hence contradiction;
end;
A8: not {{A}} in A
proof
A9: A in {A} & {A} in {{A}} by TARSKI:def 1;
assume {{A}} in A;
hence contradiction by A9,XREGULAR:7;
end;
per cases by A3,A4,A5,TARSKI:def 2;
suppose
p in A & q in A;
then reconsider p9=p,q9=q as Element of A;
take d.(p9,q9);
thus thesis by A6,A8;
end;
suppose
A10: p = {A} & q = {{A}} or q = {A} & p = {{A}};
take (d.(x,y)"\/"a)"/\"b;
thus thesis by A7,A8,A10,TARSKI:def 1;
end;
suppose
A11: (p = {A} or p = {{A}}) & q = p;
take Bottom L;
thus thesis by A7,A8,A11,TARSKI:def 1;
end;
suppose
A12: p in A & q = {A};
then reconsider p9 = p as Element of A;
take d.(p9,x)"\/"a;
thus thesis by A7,A8,A12,TARSKI:def 1;
end;
suppose
A13: p in A & q = {{A}};
then reconsider p9 = p as Element of A;
take d.(p9,y)"\/"a;
thus thesis by A7,A8,A13,TARSKI:def 1;
end;
suppose
A14: q in A & p = {A};
then reconsider q9 = q as Element of A;
take d.(q9,x)"\/"a;
thus thesis by A7,A8,A14,TARSKI:def 1;
end;
suppose
A15: q in A & p = {{A}};
then reconsider q9 = q as Element of A;
take d.(q9,y)"\/"a;
thus thesis by A7,A8,A15,TARSKI:def 1;
end;
end;
consider f being Function of [:new_set2 A,new_set2 A:],the carrier of L
such that
A16: for p,q being Element of new_set2 A holds X[p,q,f.(p,q)] from
BINOP_1:sch 3(A2);
reconsider f as BiFunction of new_set2 A,L;
{A} in {{A}, {{A}} } by TARSKI:def 2;
then
A17: {A} in new_set2 A by XBOOLE_0:def 3;
A18: for u being Element of A holds f.({A},u) = d.(u,x)"\/"a & f.({{A}},u)
= d.(u,y)"\/"a
proof
let u be Element of A;
reconsider u9 = u as Element of new_set2 A by XBOOLE_0:def 3;
ex u1 being Element of A st u1 = u9 & f.({A},u9) = d.(u1, x)"\/"a by A17
,A16;
hence f.({A},u) = d.(u,x)"\/"a;
ex u2 being Element of A st u2 = u9 & f.({{A}},u9) = d.( u2,y)"\/"a
by A1,A16;
hence thesis;
end;
take f;
A19: for u,v being Element of A holds f.(u,v) = d.(u,v)
proof
let u,v be Element of A;
reconsider u9 = u, v9 = v as Element of new_set2 A by XBOOLE_0:def 3;
thus f.(u,v) = f.(u9,v9) .= d.(u,v) by A16;
end;
for u being Element of A holds f.(u,{A}) = d.(u,x)"\/"a & f.(u,{{A}})
= d.(u,y)"\/"a
proof
let u be Element of A;
reconsider u9 = u as Element of new_set2 A by XBOOLE_0:def 3;
ex u1 being Element of A st u1 = u9 & f.(u9,{A}) = d.(u1, x)"\/"a by A17
,A16;
hence f.(u,{A}) = d.(u,x)"\/"a;
ex u2 being Element of A st u2 = u9 & f.(u9,{{A}}) = d.( u2,y)"\/"a
by A1,A16;
hence thesis;
end;
hence thesis by A17,A1,A16,A19,A18;
end;
uniqueness
proof
set x = q`1_4, y = q`2_4, a = q`3_4;
let f1,f2 be BiFunction of new_set2 A,L such that
A20: for u,v being Element of A holds f1.(u,v) = d.(u,v) and
A21: f1.({A},{A}) = Bottom L and
A22: f1.({{A}},{{A}}) = Bottom L and
A23: f1.({A},{{A}}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) and
A24: f1.({{A}},{A}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) and
A25: for u being Element of A
holds
f1.(u,{A}) = d.(u,q`1_4)"\/"(q`3_4) &
f1.( {A},u) = d.(u,q`1_4)"\/"(q`3_4) &
f1.(u,{{A}}) = d.(u,q`2_4)"\/"(q`3_4) &
f1.({{A}},u) = d. (u,q`2_4)"\/"(q`3_4) and
A26: for u,v being Element of A holds f2.(u,v) = d.(u,v) and
A27: f2.({A},{A}) = Bottom L and
A28: f2.({{A}},{{A}}) = Bottom L and
A29: f2.({A},{{A}}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) and
A30: f2.({{A}},{A}) = (d.(q`1_4,q`2_4)"\/"(q`3_4))"/\"(q`4_4) and
A31: for u being Element of A holds
f2.(u,{A}) = d.(u,q`1_4)"\/"(q`3_4) &
f2.({A},u) = d.(u,q`1_4)"\/"(q`3_4) &
f2.(u,{{A}}) = d.(u,q`2_4)"\/"(q`3_4) &
f2.({{A}},u) = d. (u,q`2_4)"\/"(q`3_4);
now
let p,q be Element of new_set2 A;
A32: p in A or p in {{A},{{A}}} by XBOOLE_0:def 3;
A33: q in A or q in {{A},{{A}}} by XBOOLE_0:def 3;
per cases by A32,A33,TARSKI:def 2;
suppose
A34: p in A & q in A;
hence f1.(p,q) = d.(p,q) by A20
.= f2.(p,q) by A26,A34;
end;
suppose
A35: p in A & q = {A};
then reconsider p9 = p as Element of A;
thus f1.(p,q) = d.(p9,x)"\/"a by A25,A35
.= f2.(p,q) by A31,A35;
end;
suppose
A36: p in A & q = {{A}};
then reconsider p9 = p as Element of A;
thus f1.(p,q) = d.(p9,y)"\/"a by A25,A36
.= f2.(p,q) by A31,A36;
end;
suppose
A37: p = {A} & q in A;
then reconsider q9 = q as Element of A;
thus f1.(p,q) = d.(q9,x)"\/"a by A25,A37
.= f2.(p,q) by A31,A37;
end;
suppose
p = {A} & q = {A};
hence f1.(p,q) = f2.(p,q) by A21,A27;
end;
suppose
p = {A} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A23,A29;
end;
suppose
A38: p = {{A}} & q in A;
then reconsider q9 = q as Element of A;
thus f1.(p,q) = d.(q9,y)"\/"a by A25,A38
.= f2.(p,q) by A31,A38;
end;
suppose
p = {{A}} & q = {A};
hence f1.(p,q) = f2.(p,q) by A24,A30;
end;
suppose
p = {{A}} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A22,A28;
end;
end;
hence f1 = f2;
end;
end;
theorem Th10:
for A being non empty set for L being lower-bounded LATTICE for
d being BiFunction of A,L st d is zeroed for q being Element of [:A,A,the
carrier of L,the carrier of L:] holds new_bi_fun2(d,q) is zeroed
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
assume
A1: d is zeroed;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set f = new_bi_fun2(d,q);
for u being Element of new_set2 A holds f.(u,u) = Bottom L
proof
let u be Element of new_set2 A;
A2: u in A or u in {{A},{{A}}} by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 2;
suppose
u in A;
then reconsider u9 = u as Element of A;
thus f.(u,u) = d.(u9,u9) by Def4
.= Bottom L by A1;
end;
suppose
u = {A} or u = {{A}};
hence thesis by Def4;
end;
end;
hence thesis;
end;
theorem Th11:
for A being non empty set for L being lower-bounded LATTICE for
d being BiFunction of A,L st d is symmetric for q being Element of [:A,A,the
carrier of L,the carrier of L:] holds new_bi_fun2(d,q) is symmetric
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
assume
A1: d is symmetric;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set f = new_bi_fun2(d,q), x = q`1_4, y = q`2_4, a = q`3_4, b = q`4_4;
let p,q be Element of new_set2 A;
A2: p in A or p in {{A},{{A}}} by XBOOLE_0:def 3;
A3: q in A or q in {{A},{{A}}} by XBOOLE_0:def 3;
per cases by A2,A3,TARSKI:def 2;
suppose
p in A & q in A;
then reconsider p9 = p, q9 = q as Element of A;
thus f.(p,q) = d.(p9,q9) by Def4
.= d.(q9,p9) by A1
.= f.(q,p) by Def4;
end;
suppose
A4: p in A & q = {A};
then reconsider p9 = p as Element of A;
thus f.(p,q) = d.(p9,x)"\/"a by A4,Def4
.= f.(q,p) by A4,Def4;
end;
suppose
A5: p in A & q = {{A}};
then reconsider p9 = p as Element of A;
thus f.(p,q) = d.(p9,y)"\/"a by A5,Def4
.= f.(q,p) by A5,Def4;
end;
suppose
A6: p = {A} & q in A;
then reconsider q9 = q as Element of A;
thus f.(p,q) = d.(q9,x)"\/"a by A6,Def4
.= f.(q,p) by A6,Def4;
end;
suppose
p = {A} & q = {A};
hence thesis;
end;
suppose
A7: p = {A} & q = {{A}};
hence f.(p,q) = (d.(x,y)"\/"a)"/\"b by Def4
.= f.(q,p) by A7,Def4;
end;
suppose
A8: p = {{A}} & q in A;
then reconsider q9 = q as Element of A;
thus f.(p,q) = d.(q9,y)"\/"a by A8,Def4
.= f.(q,p) by A8,Def4;
end;
suppose
A9: p = {{A}} & q = {A};
hence f.(p,q) = (d.(x,y)"\/"a)"/\"b by Def4
.= f.(q,p) by A9,Def4;
end;
suppose
p = {{A}} & q = {{A}};
hence thesis;
end;
end;
theorem Th12:
for A being non empty set for L being lower-bounded LATTICE st L
is modular for d being BiFunction of A,L st d is symmetric & d is u.t.i. for q
being Element of [:A,A,the carrier of L,the carrier of L:]
st d.(q`1_4,q`2_4) <= (q`3_4)"\/"(q`4_4) holds new_bi_fun2(d,q) is u.t.i.
proof
let A be non empty set;
let L be lower-bounded LATTICE;
assume
A1: L is modular;
reconsider B = {{A}, {{A}}} as non empty set;
let d be BiFunction of A,L;
assume that
A2: d is symmetric and
A3: d is u.t.i.;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set x = q`1_4, y = q`2_4, a = q`3_4, b = q`4_4, f = new_bi_fun2(d,q);
reconsider a,b as Element of L;
A4: for p,q,u being Element of new_set2 A st p in A & q in A & u in B holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set2 A;
assume
A5: p in A & q in A & u in B;
per cases by A5,TARSKI:def 2;
suppose
A6: p in A & q in A & u = {A};
then reconsider p9 = p, q9 = q as Element of A;
A7: f.(p,q) = d.(p9,q9) by Def4;
d.(p9,x) <= d.(p9,q9) "\/" d.(q9,x) by A3;
then
A8: d.(p9,x)"\/"a <= (d.(p9,q9) "\/" d.(q9,x))"\/"a by WAYBEL_1:2;
f.(p,u) = d.(p9,x)"\/"a & f.(q,u) = d.(q9,x)"\/"a by A6,Def4;
hence thesis by A7,A8,LATTICE3:14;
end;
suppose
A9: p in A & q in A & u = {{A}};
then reconsider p9 = p, q9 = q as Element of A;
A10: f.(p,q) = d.(p9,q9) by Def4;
d.(p9,y) <= d.(p9,q9) "\/" d.(q9,y) by A3;
then
A11: d.(p9,y)"\/"a <= (d.(p9,q9) "\/" d.(q9,y))"\/"a by WAYBEL_1:2;
f.(p,u) = d.(p9,y)"\/"a & f.(q,u) = d.(q9,y)"\/"a by A9,Def4;
hence thesis by A10,A11,LATTICE3:14;
end;
end;
assume
A12: d.(q`1_4,q`2_4) <= (q`3_4)"\/"(q`4_4);
A13: for p,q,u being Element of new_set2 A st p in A & q in B & u in B holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set2 A;
assume
A14: p in A & q in B & u in B;
per cases by A14,TARSKI:def 2;
suppose
A15: p in A & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def4
.= f.(p,q) by WAYBEL_1:3;
hence thesis by A15;
end;
suppose
A16: p in A & q = {A} & u = {{A}};
then reconsider p9 = p as Element of A;
a <= a "\/" d.(x,y) by YELLOW_0:22;
then
A17: a"\/"((d.(x,y)"\/"a)"/\"b) = (a"\/"b)"/\"(a"\/" d.(x,y)) by A1;
d.(p9,y) <= d.(p9,x)"\/"d.(x,y) by A3;
then
A18: d.(p9,y)"\/"a <= (d.(p9,x)"\/"d.(x,y))"\/"a by YELLOW_5:7;
a <= a;
then d.(x,y)"\/"a <= (a"\/"b)"\/"a by A12,YELLOW_3:3;
then
(d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) <= (d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a) by YELLOW_5:6;
then
A19: d.(x,y)"\/"a = (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) & d.(p9,x)"\/"((d.(
x,y)"\/"a )"/\"(d.(x,y)"\/"a)) <= d.(p9,x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by WAYBEL_1:2,YELLOW_5:2;
f.(p,q) = d.(p9,x)"\/"a & f.(q,u) = (d.(x,y)"\/"a)"/\"b by A16,Def4;
then
f.(p,q) "\/" f.(q,u) = d.(p9,x)"\/"((a"\/"b)"/\"(a"\/" d.(x,y))) by A17,
LATTICE3:14
.= d.(p9,x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"a)"\/"b)) by YELLOW_5:1
.= d.(p9,x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/" a)) by LATTICE3:14;
then (d.(p9,x)"\/"d.(x,y))"\/"a <= f.(p,q) "\/" f.(q,u) by A19,
LATTICE3:14;
then d.(p9,y)"\/"a <= f.(p,q) "\/" f.(q,u) by A18,ORDERS_2:3;
hence thesis by A16,Def4;
end;
suppose
A20: p in A & q = {{A}} & u = {A};
then reconsider p9 = p as Element of A;
a <= a "\/" d.(x,y) by YELLOW_0:22;
then
A21: a"\/"((d.(x,y)"\/"a)"/\"b) = (a"\/"b)"/\"(a"\/" d.(x,y)) by A1;
a <= a;
then d.(x,y)"\/"a <= (a"\/"b)"\/"a by A12,YELLOW_3:3;
then
(d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) <= (d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a) by YELLOW_5:6;
then
A22: d.(x,y)"\/"a = (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) & d.(p9,y)"\/"((d.(
x,y)"\/"a )"/\"(d.(x,y)"\/"a)) <= d.(p9,y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by WAYBEL_1:2,YELLOW_5:2;
d.(y,x) = d.(x,y) by A2;
then d.(p9,x) <= d.(p9,y)"\/"d.(x,y) by A3;
then
A23: d.(p9,x)"\/"a <= (d.(p9,y)"\/"d.(x,y))"\/"a by YELLOW_5:7;
f.(p,q) = d.(p9,y)"\/"a & f.(q,u) = (d.(x,y)"\/"a)"/\"b by A20,Def4;
then
f.(p,q) "\/" f.(q,u) = d.(p9,y)"\/"((a"\/"b)"/\"(a"\/" d.(x,y))) by A21,
LATTICE3:14
.= d.(p9,y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"a)"\/"b)) by YELLOW_5:1
.= d.(p9,y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/" a)) by LATTICE3:14;
then (d.(p9,y)"\/"d.(x,y))"\/"a <= f.(p,q) "\/" f.(q,u) by A22,
LATTICE3:14;
then d.(p9,x)"\/"a <= f.(p,q) "\/" f.(q,u) by A23,ORDERS_2:3;
hence thesis by A20,Def4;
end;
suppose
A24: p in A & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def4
.= f.(p,q) by WAYBEL_1:3;
hence thesis by A24;
end;
end;
A25: for p,q,u being Element of new_set2 A st p in B & q in A & u in B holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set2 A;
assume
A26: p in B & q in A & u in B;
per cases by A26,TARSKI:def 2;
suppose
q in A & p = {A} & u = {A};
then f.(p,u) = Bottom L by Def4;
hence thesis by YELLOW_0:44;
end;
suppose
A27: q in A & p = {A} & u = {{A}};
then reconsider q9 = q as Element of A;
d.(q9,x) = d.(x,q9) by A2;
then
A28: d.(x,y) <= d.(q9,x)"\/"d.(q9,y) by A3;
f.(p,q) = d.(q9,x)"\/"a by A27,Def4;
then f.(p,q) "\/" f.(q,u) = d.(q9,x)"\/"a"\/"(d.(q9,y)"\/"a) by A27,Def4
.= d.(q9,x)"\/"(d.(q9,y)"\/"a)"\/"a by LATTICE3:14
.= d.(q9,x)"\/"d.(q9,y)"\/"a"\/"a by LATTICE3:14
.= d.(q9,x)"\/"d.(q9,y)"\/"(a"\/"a) by LATTICE3:14
.= d.(q9,x)"\/"d.(q9,y)"\/"a by YELLOW_5:1;
then
A29: d.(x,y)"\/"a <= f.(p,q) "\/" f.(q,u) by A28,YELLOW_5:7;
A30: (d.(x,y)"\/"a)"/\"b <= d.(x,y)"\/"a by YELLOW_0:23;
f.(p,u) = (d.(x,y)"\/"a)"/\"b by A27,Def4;
hence thesis by A29,A30,ORDERS_2:3;
end;
suppose
A31: q in A & p = {{A}} & u = {A};
then reconsider q9 = q as Element of A;
d.(q9,x) = d.(x,q9) by A2;
then
A32: d.(x,y) <= d.(q9,x)"\/"d.(q9,y) by A3;
f.(p,q) = d.(q9,y)"\/"a by A31,Def4;
then
f.(p,q) "\/" f.(q,u) = d.(q9,x)"\/"a"\/"(d.(q9,y)"\/"a) by A31,Def4
.= d.(q9,x)"\/"(d.(q9,y)"\/"a)"\/"a by LATTICE3:14
.= d.(q9,x)"\/"d.(q9,y)"\/"a"\/"a by LATTICE3:14
.= d.(q9,x)"\/"d.(q9,y)"\/"(a"\/"a) by LATTICE3:14
.= d.(q9,x)"\/"d.(q9,y)"\/"a by YELLOW_5:1;
then
A33: d.(x,y)"\/"a <= f.(p,q) "\/" f.(q,u) by A32,YELLOW_5:7;
A34: (d.(x,y)"\/"a)"/\"b <= d.(x,y)"\/"a by YELLOW_0:23;
f.(p,u) = (d.(x,y)"\/"a)"/\"b by A31,Def4;
hence thesis by A33,A34,ORDERS_2:3;
end;
suppose
q in A & p = {{A}} & u = {{A}};
then f.(p,u) = Bottom L by Def4;
hence thesis by YELLOW_0:44;
end;
end;
A35: for p,q,u being Element of new_set2 A st p in B & q in B & u in B
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set2 A;
assume
A36: p in B & q in B & u in B;
per cases by A36,TARSKI:def 2;
suppose
A37: p = {A} & q = {A} & u = {A};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A37,Def4;
end;
suppose
A38: p = {A} & q = {A} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L "\/" f.(p,u) by Def4
.= Bottom L "\/" ((d.(x,y)"\/"a)"/\"b) by A38,Def4
.= ((d.(x,y)"\/"a)"/\"b) by WAYBEL_1:3;
hence thesis by A38,Def4;
end;
suppose
A39: p = {A} & q = {{A}} & u = {A};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A39,Def4;
end;
suppose
A40: p = {A} & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = ((d.(x,y)"\/"a)"/\"b)"\/"f.(q,u) by Def4
.= Bottom L"\/"((d.(x,y)"\/"a)"/\"b) by A40,Def4
.= ((d.(x,y)"\/"a)"/\"b) by WAYBEL_1:3;
hence thesis by A40,Def4;
end;
suppose
A41: p = {{A}} & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = ((d.(x,y)"\/"a)"/\"b)"\/" f.(q,u) by Def4
.= Bottom L"\/"((d.(x,y)"\/"a)"/\"b) by A41,Def4
.= ((d.(x,y)"\/"a)"/\"b) by WAYBEL_1:3
.= f.(p,q) by A41,Def4;
hence thesis by A41;
end;
suppose
A42: p = {{A}} & q = {A} & u = {{A}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A42,Def4;
end;
suppose
A43: p = {{A}} & q = {{A}} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def4
.= Bottom L"\/"((d.(x,y)"\/"a)"/\"b) by A43,Def4
.= ((d.(x,y)"\/"a)"/\"b) by WAYBEL_1:3;
hence thesis by A43,Def4;
end;
suppose
A44: p = {{A}} & q = {{A}} & u = {{A}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A44,Def4;
end;
end;
A45: for p,q,u being Element of new_set2 A st p in B & q in B & u in A
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set2 A;
assume
A46: p in B & q in B & u in A;
per cases by A46,TARSKI:def 2;
suppose
A47: u in A & q = {A} & p = {A};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/"f.(q,u) by Def4
.= f.(p,u) by A47,WAYBEL_1:3;
hence thesis;
end;
suppose
A48: u in A & q = {A} & p = {{A}};
then reconsider u9 = u as Element of A;
a <= a "\/" d.(x,y) by YELLOW_0:22;
then
A49: a"\/"((d.(x,y)"\/"a)"/\"b) = (a"\/"b)"/\"(a"\/" d.(x,y)) by A1;
d.(u9,y) <= d.(u9,x)"\/"d.(x,y) by A3;
then
A50: d.(u9,y)"\/"a <= (d.(u9,x)"\/"d.(x,y))"\/"a by YELLOW_5:7;
a <= a;
then d.(x,y)"\/"a <= (a"\/"b)"\/"a by A12,YELLOW_3:3;
then (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) <= (d.(x,y)"\/"a)"/\"((a"\/"b)
"\/"a) by YELLOW_5:6;
then
A51: d.(x,y)"\/"a = (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) & d.(u9,x)"\/"((d.
(x,y)"\/"a )"/\"(d.(x,y)"\/"a)) <= d.(u9,x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by WAYBEL_1:2,YELLOW_5:2;
f.(p,q) = (d.(x,y)"\/"a)"/\"b & f.(q,u) = d.(u9,x)"\/"a by A48,Def4;
then f.(p,q) "\/" f.(q,u) = d.(u9,x)"\/"((a"\/"b)"/\"(a"\/" d.(x,y)))
by A49,LATTICE3:14
.= d.(u9,x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"a)"\/"b)) by YELLOW_5:1
.= d.(u9,x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/" a)) by LATTICE3:14;
then (d.(u9,x)"\/"d.(x,y))"\/"a <= f.(p,q) "\/" f.(q,u) by A51,
LATTICE3:14;
then d.(u9,y)"\/"a <= f.(p,q) "\/" f.(q,u) by A50,ORDERS_2:3;
hence thesis by A48,Def4;
end;
suppose
A52: u in A & q = {{A}} & p = {A};
then reconsider u9 = u as Element of A;
a <= a "\/" d.(x,y) by YELLOW_0:22;
then
A53: a"\/"((d.(x,y)"\/"a)"/\"b) = (a"\/"b)"/\"(a"\/" d.(x,y)) by A1;
a <= a;
then d.(x,y)"\/"a <= (a"\/"b)"\/"a by A12,YELLOW_3:3;
then (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) <= (d.(x,y)"\/"a)"/\"((a"\/"b)
"\/"a) by YELLOW_5:6;
then
A54: d.(x,y)"\/"a = (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) & d.(u9,y)"\/"((d.
(x,y)"\/"a )"/\"(d.(x,y)"\/"a)) <= d.(u9,y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by WAYBEL_1:2,YELLOW_5:2;
d.(y,x) = d.(x,y) by A2;
then d.(u9,x) <= d.(u9,y)"\/"d.(x,y) by A3;
then
A55: d.(u9,x)"\/"a <= (d.(u9,y)"\/"d.(x,y))"\/"a by YELLOW_5:7;
f.(p,q) = (d.(x,y)"\/"a)"/\"b & f.(q,u) = d.(u9,y)"\/"a by A52,Def4;
then f.(p,q) "\/" f.(q,u) = d.(u9,y)"\/"((a"\/"b)"/\"(a"\/" d.(x,y)))
by A53,LATTICE3:14
.= d.(u9,y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"a)"\/"b)) by YELLOW_5:1
.= d.(u9,y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/" a)) by LATTICE3:14;
then (d.(u9,y)"\/"d.(x,y))"\/"a <= f.(p,q) "\/" f.(q,u) by A54,
LATTICE3:14;
then d.(u9,x)"\/"a <= f.(p,q) "\/" f.(q,u) by A55,ORDERS_2:3;
hence thesis by A52,Def4;
end;
suppose
A56: u in A & q = {{A}} & p = {{A}};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/"f.(q,u) by Def4
.= f.(p,u) by A56,WAYBEL_1:3;
hence thesis;
end;
end;
A57: for p,q,u being Element of new_set2 A st p in B & q in A & u in A holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set2 A;
assume that
A58: p in B and
A59: q in A & u in A;
reconsider q9 = q, u9 = u as Element of A by A59;
per cases by A58,A59,TARSKI:def 2;
suppose
A60: p = {A} & q in A & u in A;
d.(u9,x) <= d.(u9,q9) "\/" d.(q9,x) by A3;
then d.(u9,x) <= d.(q9,u9) "\/" d.(q9,x) by A2;
then d.(u9,x)"\/"a <= (d.(q9,x)"\/"d.(q9,u9))"\/"a by WAYBEL_1:2;
then
A61: d.(u9,x)"\/"a <= (d.(q9,x)"\/"a)"\/"d.(q9,u9) by LATTICE3:14;
A62: f.(q,u) = d.(q9,u9) by Def4;
f.(p,q) = d.(q9,x)"\/"a by A60,Def4;
hence thesis by A60,A62,A61,Def4;
end;
suppose
A63: p = {{A}} & q in A & u in A;
d.(u9,y) <= d.(u9,q9) "\/" d.(q9,y) by A3;
then d.(u9,y) <= d.(q9,u9) "\/" d.(q9,y) by A2;
then d.(u9,y)"\/"a <= (d.(q9,y)"\/"d.(q9,u9))"\/"a by WAYBEL_1:2;
then
A64: d.(u9,y)"\/"a <= (d.(q9,y)"\/"a)"\/"d.(q9,u9) by LATTICE3:14;
A65: f.(q,u) = d.(q9,u9) by Def4;
f.(p,q) = d.(q9,y)"\/"a by A63,Def4;
hence thesis by A63,A65,A64,Def4;
end;
end;
A66: for p,q,u being Element of new_set2 A st p in A & q in B & u in A holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set2 A;
assume
A67: p in A & q in B & u in A;
per cases by A67,TARSKI:def 2;
suppose
A68: p in A & u in A & q = {A};
then reconsider p9 = p, u9 = u as Element of A;
d.(p9,u9) <= d.(p9,x) "\/" d.(x,u9) by A3;
then
A69: d.(p9,x) "\/" d.(u9,x) <= (d.(p9,x) "\/" d.(u9,x))"\/"a & d.(p9,u9)
<= d.(p9,x) "\/" d.(u9,x) by A2,YELLOW_0:22;
(d.(p9,x)"\/"d.(u9,x))"\/"a = d.(p9,x)"\/"(d.(u9,x)"\/"a) by LATTICE3:14
.= d.(p9,x)"\/"(d.(u9,x)"\/"(a"\/"a)) by YELLOW_5:1
.= d.(p9,x)"\/"((d.(u9,x)"\/"a)"\/"a) by LATTICE3:14
.= (d.(p9,x)"\/"a) "\/" (d.(u9,x)"\/"a) by LATTICE3:14;
then
A70: d.(p9,u9) <= (d.(p9,x)"\/"a) "\/" (d.(u9,x)"\/"a) by A69,ORDERS_2:3;
f.(p,q) = d.(p9,x)"\/"a & f.(q,u) = d.(u9,x)"\/"a by A68,Def4;
hence thesis by A70,Def4;
end;
suppose
A71: p in A & u in A & q = {{A}};
then reconsider p9 = p, u9 = u as Element of A;
d.(p9,u9) <= d.(p9,y) "\/" d.(y,u9) by A3;
then
A72: d.(p9,y) "\/" d.(u9,y) <= (d.(p9,y) "\/" d.(u9,y))"\/"a & d.(p9,u9)
<= d.(p9,y) "\/" d.(u9,y) by A2,YELLOW_0:22;
(d.(p9,y)"\/"d.(u9,y))"\/"a = d.(p9,y)"\/"(d.(u9,y)"\/"a) by LATTICE3:14
.= d.(p9,y)"\/"(d.(u9,y)"\/"(a"\/"a)) by YELLOW_5:1
.= d.(p9,y)"\/"((d.(u9,y)"\/"a)"\/"a) by LATTICE3:14
.= (d.(p9,y)"\/"a)"\/"(d.(u9,y)"\/"a) by LATTICE3:14;
then
A73: d.(p9,u9) <= (d.(p9,y)"\/"a) "\/" (d.(u9,y)"\/"a) by A72,ORDERS_2:3;
f.(p,q) = d.(p9,y)"\/"a & f.(q,u) = d.(u9,y)"\/"a by A71,Def4;
hence thesis by A73,Def4;
end;
end;
A74: for p,q,u being Element of new_set2 A st p in A & q in A & u in A holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set2 A;
assume p in A & q in A & u in A;
then reconsider p9 = p, q9 = q, u9 = u as Element of A;
A75: f.(q,u) = d.(q9,u9) by Def4;
f.(p,u) = d.(p9,u9) & f.(p,q) = d.(p9,q9) by Def4;
hence thesis by A3,A75;
end;
for p,q,u being Element of new_set2 A holds f.(p,u) <= f.(p,q) "\/" f.
( q, u )
proof
let p,q,u be Element of new_set2 A;
per cases by XBOOLE_0:def 3;
suppose
p in A & q in A & u in A;
hence thesis by A74;
end;
suppose
p in A & q in A & u in B;
hence thesis by A4;
end;
suppose
p in A & q in B & u in A;
hence thesis by A66;
end;
suppose
p in A & q in B & u in B;
hence thesis by A13;
end;
suppose
p in B & q in A & u in A;
hence thesis by A57;
end;
suppose
p in B & q in A & u in B;
hence thesis by A25;
end;
suppose
p in B & q in B & u in A;
hence thesis by A45;
end;
suppose
p in B & q in B & u in B;
hence thesis by A35;
end;
end;
hence thesis;
end;
theorem Th13:
for A being non empty set for L being lower-bounded LATTICE for
d be BiFunction of A,L for q be Element of [:A,A,the carrier of L,the carrier
of L:] holds d c= new_bi_fun2(d,q)
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set g = new_bi_fun2(d,q);
A1: A c= new_set2 A by XBOOLE_1:7;
A2: for z being object st z in dom d holds d.z = g.z
proof
let z be object;
assume
A3: z in dom d;
then consider x,y being object such that
A4: [x,y] = z by RELAT_1:def 1;
reconsider x9 = x, y9 = y as Element of A by A3,A4,ZFMISC_1:87;
d.[x,y] = d.(x9,y9) .= g.(x9,y9) by Def4
.= g.[x,y];
hence thesis by A4;
end;
dom d = [:A,A:] & dom g = [:new_set2 A,new_set2 A:] by FUNCT_2:def 1;
then dom d c= dom g by A1,ZFMISC_1:96;
hence thesis by A2,GRFUNC_1:2;
end;
reserve x for set,
C for Ordinal,
L0 for Sequence;
definition
let A be non empty set;
let O be Ordinal;
func ConsecutiveSet2(A,O) -> set means
:Def5:
ex L0 being Sequence st it = last
L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal st succ C in succ O
holds L0.succ C = new_set2(L0.C)) & for C being Ordinal st C in succ O & C <>
0 & C is limit_ordinal holds L0.C = union rng (L0|C);
correctness
proof
deffunc D(set,Sequence) = union rng $2;
deffunc C(Ordinal,set) = new_set2 $2;
(ex x being object,L0
st x = last L0 & dom L0 = succ O & L0.0 = A & (for C st
succ C in succ O holds L0.succ C = C(C,L0.C)) & for C st C in succ O & C <> 0
& C is limit_ordinal holds L0.C = D(C,L0|C) ) & for x1,x2 being set st (ex L0
st x1 = last L0 & dom L0 = succ O & L0.0 = A & (for C st succ C in succ O
holds L0.succ C = C(C,L0.C)) & for C st C in succ O & C <> 0 & C is
limit_ordinal holds L0.C = D(C,L0|C) ) & (ex L0 st x2 = last L0 & dom L0 = succ
O & L0.0 = A & (for C st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C
st C in succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) ) holds x1
= x2 from ORDINAL2:sch 7;
hence thesis;
end;
end;
theorem Th14:
for A being non empty set holds ConsecutiveSet2(A,0) = A
proof
deffunc D(set,Sequence) = union rng $2;
deffunc C(Ordinal,set) = new_set2 $2;
let A be non empty set;
deffunc F(Ordinal) = ConsecutiveSet2(A,$1);
A1: for O being Ordinal, It being object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def5;
thus F(0) = A from ORDINAL2:sch 8(A1);
end;
theorem Th15:
for A being non empty set for O being Ordinal holds
ConsecutiveSet2(A,succ O) = new_set2 ConsecutiveSet2(A,O)
proof
deffunc D(set,Sequence) = union rng $2;
deffunc C(Ordinal,set) = new_set2 $2;
let A be non empty set;
let O be Ordinal;
deffunc F(Ordinal) = ConsecutiveSet2(A,$1);
A1: for O being Ordinal, It being object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def5;
for O being Ordinal holds F(succ O) = C(O,F(O)) from ORDINAL2:sch 9( A1);
hence thesis;
end;
theorem Th16:
for A being non empty set for O being Ordinal for T being
Sequence holds O <> 0 & O is limit_ordinal & dom T = O & (for O1 being
Ordinal st O1 in O holds T.O1 = ConsecutiveSet2(A,O1)) implies ConsecutiveSet2(
A,O) = union rng T
proof
deffunc D(set,Sequence) = union rng $2;
deffunc C(Ordinal,set) = new_set2 $2;
let A be non empty set;
let O be Ordinal;
let T be Sequence;
deffunc F(Ordinal) = ConsecutiveSet2(A,$1);
assume that
A1: O <> 0 & O is limit_ordinal and
A2: dom T = O and
A3: for O1 being Ordinal st O1 in O holds T.O1 = F(O1);
A4: for O being Ordinal, It being object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def5;
thus F(O) = D(O,T) from ORDINAL2:sch 10(A4,A1,A2,A3);
end;
reserve O1,O2 for Ordinal;
registration
let A be non empty set;
let O be Ordinal;
cluster ConsecutiveSet2(A,O) -> non empty;
coherence
proof
defpred X[Ordinal] means ConsecutiveSet2(A,$1) is non empty;
A1: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume ConsecutiveSet2(A,O1) is non empty;
ConsecutiveSet2(A,succ O1) = new_set2 ConsecutiveSet2(A,O1) by Th15;
hence thesis;
end;
A2: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[
O2] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
let O1 be Ordinal;
assume that
A3: O1 <> 0 and
A4: O1 is limit_ordinal and
for O2 being Ordinal st O2 in O1 holds ConsecutiveSet2(A,O2) is non
empty;
A5: {} in O1 by A3,ORDINAL3:8;
consider Ls being Sequence such that
A6: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = U(
O2) from ORDINAL2:sch 2;
Ls.{} = ConsecutiveSet2(A,{}) by A3,A6,ORDINAL3:8
.= A by Th14;
then
A7: A in rng Ls by A6,A5,FUNCT_1:def 3;
ConsecutiveSet2(A,O1) = union rng Ls by A3,A4,A6,Th16;
then A c= ConsecutiveSet2(A,O1) by A7,ZFMISC_1:74;
hence thesis;
end;
A8: X[0] by Th14;
for O being Ordinal holds X[O] from ORDINAL2:sch 1(A8,A1,A2);
hence thesis;
end;
end;
theorem Th17:
for A being non empty set for O being Ordinal holds A c= ConsecutiveSet2(A,O)
proof
let A be non empty set;
let O be Ordinal;
defpred X[Ordinal] means A c= ConsecutiveSet2(A,$1);
A1: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
ConsecutiveSet2(A,succ O1) = new_set2 ConsecutiveSet2(A,O1) by Th15;
then
A2: ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,succ O1) by XBOOLE_1:7;
assume A c= ConsecutiveSet2(A,O1);
hence thesis by A2,XBOOLE_1:1;
end;
A3: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2
] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
let O2 be Ordinal;
assume that
A4: O2 <> 0 and
A5: O2 is limit_ordinal and
for O1 be Ordinal st O1 in O2 holds A c= ConsecutiveSet2(A,O1);
A6: {} in O2 by A4,ORDINAL3:8;
consider Ls being Sequence such that
A7: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1)
from ORDINAL2:sch 2;
Ls.{} = ConsecutiveSet2(A,{}) by A4,A7,ORDINAL3:8
.= A by Th14;
then
A8: A in rng Ls by A7,A6,FUNCT_1:def 3;
ConsecutiveSet2(A,O2) = union rng Ls by A4,A5,A7,Th16;
hence thesis by A8,ZFMISC_1:74;
end;
A9: X[0] by Th14;
for O being Ordinal holds X[O] from ORDINAL2:sch 1(A9,A1,A3);
hence thesis;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
assume
A1: O in dom q;
func Quadr2(q,O) -> Element of [:ConsecutiveSet2(A,O),ConsecutiveSet2(A,O),
the carrier of L,the carrier of L:] equals
:Def6:
q.O;
correctness
proof
q.O in rng q by A1,FUNCT_1:def 3;
then q.O in {[x,y,a,b] where x is Element of A, y is Element of A, a is
Element of L, b is Element of L: d.(x,y) <= a"\/"b} by LATTICE5:def 13;
then consider x,y be Element of A, a,b be Element of L such that
A2: q.O = [x,y,a,b] and
d.(x,y) <= a"\/"b;
reconsider a,b as Element of L;
A c= ConsecutiveSet2(A,O) by Th17;
then reconsider x,y as Element of ConsecutiveSet2(A,O);
reconsider z = [x,y,a,b] as Element of [:ConsecutiveSet2(A,O),
ConsecutiveSet2(A,O), the carrier of L,the carrier of L:];
z = q.O by A2;
hence thesis;
end;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
func ConsecutiveDelta2(q,O) -> set means
:Def7:
ex L0 being Sequence st it = last
L0 & dom L0 = succ O & L0.0 = d & (for C being Ordinal st succ C in succ O
holds L0.succ C = new_bi_fun2(BiFun(L0.C,ConsecutiveSet2(A,C),L),Quadr2(q,C)))
& for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds L0.C
= union rng(L0|C);
correctness
proof
deffunc D(set,Sequence) = union rng $2;
deffunc C(Ordinal,set) = new_bi_fun2(BiFun($2,ConsecutiveSet2(A,$1),L),
Quadr2(q,$1));
(ex x being object,L0
st x = last L0 & dom L0 = succ O & L0.0 = d & (for C st
succ C in succ O holds L0.succ C = C(C,L0.C)) & for C st C in succ O & C <> 0
& C is limit_ordinal holds L0.C = D(C,L0|C)) & for x1,x2 being set st (ex L0 st
x1 = last L0 & dom L0 = succ O & L0.0= d & (for C st succ C in succ O holds
L0.succ C = C(C,L0.C)) & for C st C in succ O & C <> 0 & C is limit_ordinal
holds L0.C = D(C,L0|C) ) & (ex L0 st x2 = last L0 & dom L0 = succ O & L0.0 = d
& (for C st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C st C in succ
O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) ) holds x1 = x2 from
ORDINAL2:sch 7;
hence thesis;
end;
end;
theorem Th18:
for A being non empty set for L be lower-bounded LATTICE for d
being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta2(q,0)
= d
proof
deffunc D(set,Sequence) = union rng $2;
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
deffunc C(Ordinal,set) = new_bi_fun2(BiFun($2,ConsecutiveSet2(A,$1),L),
Quadr2(q,$1));
deffunc F(Ordinal) = ConsecutiveDelta2(q,$1);
A1: for O being Ordinal, It being object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = d & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def7;
thus F(0) = d from ORDINAL2:sch 8(A1);
end;
theorem Th19:
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds
ConsecutiveDelta2(q,succ O) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,O),
ConsecutiveSet2(A,O),L),Quadr2(q,O))
proof
deffunc D(set,Sequence) = union rng $2;
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
deffunc C(Ordinal,set) = new_bi_fun2(BiFun($2,ConsecutiveSet2(A,$1),L),
Quadr2(q,$1));
deffunc F(Ordinal) = ConsecutiveDelta2(q,$1);
A1: for O being Ordinal, It being object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = d & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def7;
for O being Ordinal holds F(succ O) = C(O,F(O)) from ORDINAL2:sch 9( A1);
hence thesis;
end;
theorem Th20:
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L for q being QuadrSeq of d for T being Sequence for O
being Ordinal holds O <> 0 & O is limit_ordinal & dom T = O & (for O1 being
Ordinal st O1 in O holds T.O1 = ConsecutiveDelta2(q,O1)) implies
ConsecutiveDelta2(q,O) = union rng T
proof
deffunc D(set,Sequence) = union rng $2;
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let T be Sequence;
let O be Ordinal;
deffunc C(Ordinal,set) = new_bi_fun2(BiFun($2,ConsecutiveSet2(A,$1),L),
Quadr2(q,$1));
deffunc F(Ordinal) = ConsecutiveDelta2(q,$1);
assume that
A1: O <> 0 & O is limit_ordinal and
A2: dom T = O and
A3: for O1 being Ordinal st O1 in O holds T.O1 = F(O1);
A4: for O being Ordinal, It being object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = d & (for C being Ordinal
st succ C in succ O holds L0.succ C = C(C,L0.C) ) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def7;
thus F(O) = D(O,T) from ORDINAL2:sch 10(A4,A1,A2,A3);
end;
theorem Th21:
for A being non empty set for O,O1,O2 being Ordinal holds O1 c=
O2 implies ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O2)
proof
let A be non empty set;
let O,O1,02 be Ordinal;
defpred X[Ordinal] means O1 c= $1 implies ConsecutiveSet2(A,O1) c=
ConsecutiveSet2(A,$1);
A1: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O2 be Ordinal;
assume
A2: O1 c= O2 implies ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O2);
assume
A3: O1 c= succ O2;
per cases;
suppose
O1 = succ O2;
hence thesis;
end;
suppose
O1 <> succ O2;
then O1 c< succ O2 by A3;
then
A4: O1 in succ O2 by ORDINAL1:11;
ConsecutiveSet2(A,O2) c= new_set2 ConsecutiveSet2(A,O2) by XBOOLE_1:7;
then ConsecutiveSet2(A,O1) c= new_set2 ConsecutiveSet2(A,O2) by A2,A4,
ORDINAL1:22;
hence thesis by Th15;
end;
end;
A5: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[
O2] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
let O2 be Ordinal;
assume that
A6: O2 <> 0 & O2 is limit_ordinal and
for O3 being Ordinal st O3 in O2 holds O1 c= O3 implies
ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O3);
consider L being Sequence such that
A7: dom L = O2 & for O3 being Ordinal st O3 in O2 holds L.O3 = U(O3)
from ORDINAL2:sch 2;
A8: ConsecutiveSet2(A,O2) = union rng L by A6,A7,Th16;
assume
A9: O1 c= O2;
per cases;
suppose
O1 = O2;
hence thesis;
end;
suppose
O1 <> O2;
then
A10: O1 c< O2 by A9;
then O1 in O2 by ORDINAL1:11;
then
A11: L.O1 in rng L by A7,FUNCT_1:def 3;
L.O1 = ConsecutiveSet2(A,O1) by A7,A10,ORDINAL1:11;
hence thesis by A8,A11,ZFMISC_1:74;
end;
end;
A12: X[0];
for O being Ordinal holds X[O] from ORDINAL2:sch 1(A12,A1,A5);
hence thesis;
end;
theorem Th22:
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds
ConsecutiveDelta2(q,O) is BiFunction of ConsecutiveSet2(A,O),L
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
defpred X[Ordinal] means ConsecutiveDelta2(q,$1) is BiFunction of
ConsecutiveSet2(A,$1),L;
A1: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume ConsecutiveDelta2(q,O1) is BiFunction of ConsecutiveSet2(A,O1),L;
then reconsider
CD = ConsecutiveDelta2(q,O1) as BiFunction of ConsecutiveSet2(A
,O1),L;
A2: ConsecutiveDelta2(q,succ O1) = new_bi_fun2(BiFun(ConsecutiveDelta2( q,
O1 ) , ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th19
.= new_bi_fun2(CD,Quadr2(q,O1)) by LATTICE5:def 15;
ConsecutiveSet2(A,succ O1) = new_set2 ConsecutiveSet2(A,O1) by Th15;
hence thesis by A2;
end;
A3: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2
] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
let O1 be Ordinal;
assume that
A4: O1 <> 0 and
A5: O1 is limit_ordinal and
A6: for O2 be Ordinal st O2 in O1 holds ConsecutiveDelta2(q,O2) is
BiFunction of ConsecutiveSet2(A,O2),L;
reconsider o1 = O1 as non empty Ordinal by A4;
set YY = the set of all
[:ConsecutiveSet2(A,O2),ConsecutiveSet2(A,O2):] where O2 is
Element of o1 ;
consider Ls being Sequence such that
A7: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = U(O2
) from ORDINAL2:sch 2;
A8: for O,O2 being Ordinal st O c= O2 & O2 in dom Ls holds Ls.O c= Ls.O2
proof
let O be Ordinal;
defpred X[Ordinal] means O c= $1 & $1 in dom Ls implies Ls.O c= Ls.$1;
A9: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds
X[O2] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
let O2 be Ordinal;
assume that
A10: O2 <> 0 & O2 is limit_ordinal and
for O3 be Ordinal st O3 in O2 holds O c= O3 & O3 in dom Ls implies
Ls.O c= Ls.O3;
assume that
A11: O c= O2 and
A12: O2 in dom Ls;
consider Lt being Sequence such that
A13: dom Lt = O2 & for O3 being Ordinal st O3 in O2 holds Lt.O3 =
U(O3) from ORDINAL2:sch 2;
A14: Ls.O2 = ConsecutiveDelta2(q,O2) by A7,A12
.= union rng Lt by A10,A13,Th20;
per cases;
suppose
O = O2;
hence thesis;
end;
suppose
O <> O2;
then
A15: O c< O2 by A11;
then
A16: O in O2 by ORDINAL1:11;
then Ls.O = ConsecutiveDelta2(q,O) by A7,A12,ORDINAL1:10
.= Lt.O by A13,A15,ORDINAL1:11;
then Ls.O in rng Lt by A13,A16,FUNCT_1:def 3;
hence thesis by A14,ZFMISC_1:74;
end;
end;
A17: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O2 be Ordinal;
assume
A18: O c= O2 & O2 in dom Ls implies Ls.O c= Ls.O2;
assume that
A19: O c= succ O2 and
A20: succ O2 in dom Ls;
per cases;
suppose
O = succ O2;
hence thesis;
end;
suppose
O <> succ O2;
then O c< succ O2 by A19;
then
A21: O in succ O2 by ORDINAL1:11;
A22: O2 in succ O2 by ORDINAL1:6;
then O2 in dom Ls by A20,ORDINAL1:10;
then reconsider Def8 = ConsecutiveDelta2(q,O2) as BiFunction of
ConsecutiveSet2(A,O2),L by A6,A7;
Ls.succ O2 = ConsecutiveDelta2(q,succ O2) by A7,A20
.= new_bi_fun2(BiFun(ConsecutiveDelta2(q,O2), ConsecutiveSet2(A,
O2),L),Quadr2(q,O2)) by Th19
.= new_bi_fun2(Def8,Quadr2(q,O2)) by LATTICE5:def 15;
then ConsecutiveDelta2(q,O2) c= Ls.succ O2 by Th13;
then Ls.O2 c= Ls.succ O2 by A7,A20,A22,ORDINAL1:10;
hence thesis by A18,A20,A21,A22,ORDINAL1:10,22;
end;
end;
A23: X[0];
thus for O being Ordinal holds X[O] from ORDINAL2:sch 1(A23,A17, A9);
end;
for x,y being set st x in rng Ls & y in rng Ls holds x,y are_c=-comparable
proof
let x,y be set;
assume that
A24: x in rng Ls and
A25: y in rng Ls;
consider o1 being object such that
A26: o1 in dom Ls and
A27: Ls.o1 = x by A24,FUNCT_1:def 3;
consider o2 being object such that
A28: o2 in dom Ls and
A29: Ls.o2 = y by A25,FUNCT_1:def 3;
reconsider o19 = o1, o29 = o2 as Ordinal by A26,A28;
o19 c= o29 or o29 c= o19;
then x c= y or y c= x by A8,A26,A27,A28,A29;
hence thesis;
end;
then
A30: rng Ls is c=-linear;
set Y = the carrier of L, X = [:
ConsecutiveSet2(A,O1),ConsecutiveSet2(A,O1):], f = union rng Ls;
rng Ls c= PFuncs(X,Y)
proof
let z be object;
assume z in rng Ls;
then consider o being object such that
A31: o in dom Ls and
A32: z = Ls.o by FUNCT_1:def 3;
reconsider o as Ordinal by A31;
Ls.o = ConsecutiveDelta2(q,o) by A7,A31;
then reconsider
h = Ls.o as BiFunction of ConsecutiveSet2(A,o),L by A6,A7,A31;
o c= O1 by A7,A31,ORDINAL1:def 2;
then dom h = [:ConsecutiveSet2(A,o),ConsecutiveSet2(A,o):] &
ConsecutiveSet2(A,o) c= ConsecutiveSet2(A,O1) by Th21,FUNCT_2:def 1;
then rng h c= Y & dom h c= X by ZFMISC_1:96;
hence thesis by A32,PARTFUN1:def 3;
end;
then f in PFuncs(X,Y) by A30,TREES_2:40;
then
A33: ex g being Function st f = g & dom g c= X & rng g c= Y by PARTFUN1:def 3;
Ls is Function-yielding
proof
let x be object;
assume
A34: x in dom Ls;
then reconsider o = x as Ordinal;
Ls.o = ConsecutiveDelta2(q,o) by A7,A34;
hence thesis by A6,A7,A34;
end;
then reconsider LsF = Ls as Function-yielding Function;
A35: rng doms LsF = YY
proof
thus rng doms LsF c= YY
proof
let Z be object;
assume Z in rng doms LsF;
then consider o being object such that
A36: o in dom doms LsF and
A37: Z = (doms LsF).o by FUNCT_1:def 3;
A38: o in dom LsF by A36,FUNCT_6:59;
then reconsider o9 = o as Element of o1 by A7;
Ls.o9 = ConsecutiveDelta2(q,o9) by A7;
then reconsider
ls = Ls.o9 as BiFunction of ConsecutiveSet2(A,o9),L by A6;
Z = dom ls by A37,A38,FUNCT_6:22
.= [:ConsecutiveSet2(A,o9),ConsecutiveSet2(A,o9):] by FUNCT_2:def 1;
hence thesis;
end;
let Z be object;
assume Z in YY;
then consider o being Element of o1 such that
A39: Z = [:ConsecutiveSet2(A,o),ConsecutiveSet2(A,o):];
Ls.o = ConsecutiveDelta2(q,o) by A7;
then reconsider ls = Ls.o as BiFunction of ConsecutiveSet2(A,o),L by A6;
o in dom LsF by A7;
then
A40: o in dom doms LsF by FUNCT_6:59;
Z = dom ls by A39,FUNCT_2:def 1
.= (doms LsF).o by A7,FUNCT_6:22;
hence thesis by A40,FUNCT_1:def 3;
end;
A41: ConsecutiveDelta2(q,O1) = union rng Ls by A4,A5,A7,Th20;
reconsider f as Function by A33;
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
consider Ts being Sequence such that
A42: dom Ts = O1 & for O2 being Ordinal st O2 in O1 holds Ts.O2 = U(O2
) from ORDINAL2:sch 2;
{} in O1 by A4,ORDINAL3:8;
then reconsider RTs = rng Ts as non empty set by A42,FUNCT_1:3;
A43: YY = { [:a,a:] where a is Element of RTs : a in RTs }
proof
set XX = { [:a,a:] where a is Element of RTs : a in RTs };
thus YY c= XX
proof
let Z be object;
assume Z in YY;
then consider o being Element of o1 such that
A44: Z = [:ConsecutiveSet2(A,o),ConsecutiveSet2(A,o):];
Ts.o = ConsecutiveSet2(A,o) by A42;
then reconsider CoS = ConsecutiveSet2(A,o) as Element of RTs by A42,
FUNCT_1:def 3;
Z = [:CoS,CoS:] by A44;
hence thesis;
end;
let Z be object;
assume Z in XX;
then consider a being Element of RTs such that
A45: Z = [:a,a:] and
a in RTs;
consider o being object such that
A46: o in dom Ts and
A47: a = Ts.o by FUNCT_1:def 3;
reconsider o9 = o as Ordinal by A46;
a = ConsecutiveSet2(A,o9) by A42,A46,A47;
hence thesis by A42,A45,A46;
end;
for x,y being set st x in RTs & y in RTs holds x,y are_c=-comparable
proof
let x,y be set;
assume that
A48: x in RTs and
A49: y in RTs;
consider o1 being object such that
A50: o1 in dom Ts and
A51: Ts.o1 = x by A48,FUNCT_1:def 3;
consider o2 being object such that
A52: o2 in dom Ts and
A53: Ts.o2 = y by A49,FUNCT_1:def 3;
reconsider o19 = o1, o29 = o2 as Ordinal by A50,A52;
A54: Ts.o29 = ConsecutiveSet2(A,o29) by A42,A52;
A55: o19 c= o29 or o29 c= o19;
Ts.o19 = ConsecutiveSet2(A,o19) by A42,A50;
then x c= y or y c= x by A51,A53,A54,A55,Th21;
hence thesis;
end;
then
A56: dom f = union rng doms LsF & RTs is c=-linear by LATTICE5:1;
X = [:union rng Ts, ConsecutiveSet2(A,O1):] by A4,A5,A42,Th16
.= [:union RTs, union RTs :] by A4,A5,A42,Th16
.= dom f by A35,A56,A43,LATTICE5:3;
hence thesis by A41,A33,FUNCT_2:def 1,RELSET_1:4;
end;
ConsecutiveSet2(A,{}) = A by Th14;
then
A57: X[0] by Th18;
for O being Ordinal holds X[O] from ORDINAL2:sch 1(A57,A1,A3);
hence thesis;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
redefine func ConsecutiveDelta2(q,O) -> BiFunction of ConsecutiveSet2(A,O),L; :: redefines ConsecutiveDelta2 (LATTICE8, definition)
coherence by Th22;
end;
theorem Th23:
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds d c=
ConsecutiveDelta2(q,O)
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
defpred X[Ordinal] means d c= ConsecutiveDelta2(q,$1);
A1: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
ConsecutiveDelta2(q,succ O1) = new_bi_fun2(BiFun(ConsecutiveDelta2( q,
O1 ) , ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th19
.= new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) by LATTICE5:def 15;
then
A2: ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,succ O1) by Th13;
assume d c= ConsecutiveDelta2(q,O1);
hence thesis by A2,XBOOLE_1:1;
end;
A3: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2
] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
let O2 be Ordinal;
assume that
A4: O2 <> 0 and
A5: O2 is limit_ordinal and
for O1 be Ordinal st O1 in O2 holds d c= ConsecutiveDelta2(q,O1);
A6: {} in O2 by A4,ORDINAL3:8;
consider Ls being Sequence such that
A7: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1)
from ORDINAL2:sch 2;
Ls.{} = ConsecutiveDelta2(q,{}) by A4,A7,ORDINAL3:8
.= d by Th18;
then
A8: d in rng Ls by A7,A6,FUNCT_1:def 3;
ConsecutiveDelta2(q,O2) = union rng Ls by A4,A5,A7,Th20;
hence thesis by A8,ZFMISC_1:74;
end;
A9: X[0] by Th18;
for O being Ordinal holds X[O] from ORDINAL2:sch 1(A9,A1,A3);
hence thesis;
end;
theorem Th24:
for A being non empty set for L be lower-bounded LATTICE for d
being BiFunction of A,L for O1,O2 being Ordinal for q being QuadrSeq of d st O1
c= O2 holds ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,O2)
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let O1,O2 be Ordinal;
let q be QuadrSeq of d;
defpred X[Ordinal] means O1 c= $1 implies ConsecutiveDelta2(q,O1) c=
ConsecutiveDelta2(q,$1);
A1: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[
O2] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
let O2 be Ordinal;
assume that
A2: O2 <> 0 & O2 is limit_ordinal and
for O3 be Ordinal st O3 in O2 holds O1 c= O3 implies ConsecutiveDelta2
(q,O1) c= ConsecutiveDelta2(q,O3);
consider L being Sequence such that
A3: dom L = O2 & for O3 being Ordinal st O3 in O2 holds L.O3 = U(O3)
from ORDINAL2:sch 2;
A4: ConsecutiveDelta2(q,O2) = union rng L by A2,A3,Th20;
assume
A5: O1 c= O2;
per cases;
suppose
O1 = O2;
hence thesis;
end;
suppose
O1 <> O2;
then
A6: O1 c< O2 by A5;
then O1 in O2 by ORDINAL1:11;
then
A7: L.O1 in rng L by A3,FUNCT_1:def 3;
L.O1 = ConsecutiveDelta2(q,O1) by A3,A6,ORDINAL1:11;
hence thesis by A4,A7,ZFMISC_1:74;
end;
end;
A8: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O2 be Ordinal;
assume
A9: O1 c= O2 implies ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,O2 );
assume
A10: O1 c= succ O2;
per cases;
suppose
O1 = succ O2;
hence thesis;
end;
suppose
A11: O1 <> succ O2;
ConsecutiveDelta2(q,succ O2) = new_bi_fun2(BiFun(ConsecutiveDelta2(q
,O2), ConsecutiveSet2(A,O2),L),Quadr2(q,O2)) by Th19
.= new_bi_fun2(ConsecutiveDelta2(q,O2),Quadr2(q,O2)) by LATTICE5:def 15
;
then
A12: ConsecutiveDelta2(q,O2) c= ConsecutiveDelta2(q,succ O2) by Th13;
O1 c< succ O2 by A10,A11;
then O1 in succ O2 by ORDINAL1:11;
hence thesis by A9,A12,ORDINAL1:22;
end;
end;
A13: X[0];
for O being Ordinal holds X[O] from ORDINAL2:sch 1(A13,A8,A1);
hence thesis;
end;
theorem Th25:
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L st d is zeroed for q being QuadrSeq of d for O being
Ordinal holds ConsecutiveDelta2(q,O) is zeroed
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
assume
A1: d is zeroed;
let q be QuadrSeq of d;
let O be Ordinal;
defpred X[Ordinal] means ConsecutiveDelta2(q,$1) is zeroed;
A2: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume ConsecutiveDelta2(q,O1) is zeroed;
then
A3: new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) is zeroed by Th10;
let z be Element of ConsecutiveSet2(A,succ O1);
reconsider z9 = z as Element of new_set2 ConsecutiveSet2(A,O1) by Th15;
ConsecutiveDelta2(q,succ O1) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,
O1 ) , ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th19
.= new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) by LATTICE5:def 15;
hence
ConsecutiveDelta2(q,succ O1).(z,z) = new_bi_fun2(ConsecutiveDelta2(q,
O1),Quadr2(q,O1)).(z9,z9)
.= Bottom L by A3;
end;
A4: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2
] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
let O2 be Ordinal;
assume that
A5: O2 <> 0 & O2 is limit_ordinal and
A6: for O1 be Ordinal st O1 in O2 holds ConsecutiveDelta2(q,O1) is zeroed;
set CS = ConsecutiveSet2(A,O2);
consider Ls being Sequence such that
A7: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1
) from ORDINAL2:sch 2;
ConsecutiveDelta2(q,O2) = union rng Ls by A5,A7,Th20;
then reconsider f = union rng Ls as BiFunction of CS,L;
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
consider Ts being Sequence such that
A8: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds Ts.O1 = U(O1
) from ORDINAL2:sch 2;
A9: ConsecutiveSet2(A,O2) = union rng Ts by A5,A8,Th16;
f is zeroed
proof
let x be Element of CS;
consider y being set such that
A10: x in y and
A11: y in rng Ts by A9,TARSKI:def 4;
consider o being object such that
A12: o in dom Ts and
A13: y = Ts.o by A11,FUNCT_1:def 3;
reconsider o as Ordinal by A12;
A14: Ls.o = ConsecutiveDelta2(q,o) by A7,A8,A12;
then reconsider h = Ls.o as BiFunction of ConsecutiveSet2(A,o),L;
reconsider x9 = x as Element of ConsecutiveSet2(A,o) by A8,A10,A12,A13;
A15: dom h = [:ConsecutiveSet2(A,o),ConsecutiveSet2(A,o):] by FUNCT_2:def 1;
A16: h is zeroed
proof
let z be Element of ConsecutiveSet2(A,o);
A17: ConsecutiveDelta2(q,o) is zeroed by A6,A8,A12;
thus h.(z,z) = ConsecutiveDelta2(q,o).(z,z) by A7,A8,A12
.= Bottom L by A17;
end;
ConsecutiveDelta2(q,o) in rng Ls by A7,A8,A12,A14,FUNCT_1:def 3;
then
A18: h c= f by A14,ZFMISC_1:74;
x in ConsecutiveSet2(A,o) by A8,A10,A12,A13;
then [x,x] in dom h by A15,ZFMISC_1:87;
hence f.(x,x) = h.(x9,x9) by A18,GRFUNC_1:2
.= Bottom L by A16;
end;
hence thesis by A5,A7,Th20;
end;
A19: X[0]
proof
let z be Element of ConsecutiveSet2(A,0);
reconsider z9 = z as Element of A by Th14;
thus ConsecutiveDelta2(q,0).(z,z) = d.(z9,z9) by Th18
.= Bottom L by A1;
end;
for O being Ordinal holds X[O] from ORDINAL2:sch 1(A19,A2,A4);
hence thesis;
end;
theorem Th26:
for A being non empty set for L be lower-bounded LATTICE for d
be BiFunction of A,L st d is symmetric for q being QuadrSeq of d for O being
Ordinal holds ConsecutiveDelta2(q,O) is symmetric
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
assume
A1: d is symmetric;
let q be QuadrSeq of d;
let O be Ordinal;
defpred X[Ordinal] means ConsecutiveDelta2(q,$1) is symmetric;
A2: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume ConsecutiveDelta2(q,O1) is symmetric;
then
A3: new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) is symmetric by Th11;
let x,y be Element of ConsecutiveSet2(A,succ O1);
reconsider x9=x, y9=y as Element of new_set2 ConsecutiveSet2(A,O1) by Th15;
A4: ConsecutiveDelta2(q,succ O1) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,
O1), ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th19
.= new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) by LATTICE5:def 15;
hence
ConsecutiveDelta2(q,succ O1).(x,y) = new_bi_fun2(ConsecutiveDelta2(q,
O1),Quadr2(q,O1)).(y9,x9) by A3
.= ConsecutiveDelta2(q,succ O1).(y,x) by A4;
end;
A5: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[O2
] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
let O2 be Ordinal;
assume that
A6: O2 <> 0 & O2 is limit_ordinal and
A7: for O1 being Ordinal st O1 in O2 holds ConsecutiveDelta2(q,O1) is
symmetric;
set CS = ConsecutiveSet2(A,O2);
consider Ls being Sequence such that
A8: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1
) from ORDINAL2:sch 2;
ConsecutiveDelta2(q,O2) = union rng Ls by A6,A8,Th20;
then reconsider f = union rng Ls as BiFunction of CS,L;
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
consider Ts being Sequence such that
A9: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds Ts.O1 = U(O1
) from ORDINAL2:sch 2;
A10: ConsecutiveSet2(A,O2) = union rng Ts by A6,A9,Th16;
f is symmetric
proof
let x,y be Element of CS;
consider x1 being set such that
A11: x in x1 and
A12: x1 in rng Ts by A10,TARSKI:def 4;
consider o1 being object such that
A13: o1 in dom Ts and
A14: x1 = Ts.o1 by A12,FUNCT_1:def 3;
consider y1 being set such that
A15: y in y1 and
A16: y1 in rng Ts by A10,TARSKI:def 4;
consider o2 being object such that
A17: o2 in dom Ts and
A18: y1 = Ts.o2 by A16,FUNCT_1:def 3;
reconsider o1,o2 as Ordinal by A13,A17;
A19: x in ConsecutiveSet2(A,o1) by A9,A11,A13,A14;
A20: Ls.o1 = ConsecutiveDelta2(q,o1) by A8,A9,A13;
then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet2(A,o1),L;
A21: h1 is symmetric
proof
let x,y be Element of ConsecutiveSet2(A,o1);
A22: ConsecutiveDelta2(q,o1) is symmetric by A7,A9,A13;
thus h1.(x,y) = ConsecutiveDelta2(q,o1).(x,y) by A8,A9,A13
.= ConsecutiveDelta2(q,o1).(y,x) by A22
.= h1.(y,x) by A8,A9,A13;
end;
A23: dom h1 = [:ConsecutiveSet2(A,o1),ConsecutiveSet2(A,o1):] by FUNCT_2:def 1
;
A24: y in ConsecutiveSet2(A,o2) by A9,A15,A17,A18;
A25: Ls.o2 = ConsecutiveDelta2(q,o2) by A8,A9,A17;
then reconsider h2 = Ls.o2 as BiFunction of ConsecutiveSet2(A,o2),L;
A26: h2 is symmetric
proof
let x,y be Element of ConsecutiveSet2(A,o2);
A27: ConsecutiveDelta2(q,o2) is symmetric by A7,A9,A17;
thus h2.(x,y) = ConsecutiveDelta2(q,o2).(x,y) by A8,A9,A17
.= ConsecutiveDelta2(q,o2).(y,x) by A27
.= h2.(y,x) by A8,A9,A17;
end;
A28: dom h2 = [:ConsecutiveSet2(A,o2),ConsecutiveSet2(A,o2):] by FUNCT_2:def 1
;
per cases;
suppose
o1 c= o2;
then
A29: ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o2) by Th21;
then
A30: [y,x] in dom h2 by A19,A24,A28,ZFMISC_1:87;
ConsecutiveDelta2(q,o2) in rng Ls by A8,A9,A17,A25,FUNCT_1:def 3;
then
A31: h2 c= f by A25,ZFMISC_1:74;
reconsider x9=x, y9=y as Element of ConsecutiveSet2(A,o2) by A9,A15,A17
,A18,A19,A29;
[x,y] in dom h2 by A19,A24,A28,A29,ZFMISC_1:87;
hence f.(x,y) = h2.(x9,y9) by A31,GRFUNC_1:2
.= h2.(y9,x9) by A26
.= f.(y,x) by A31,A30,GRFUNC_1:2;
end;
suppose
o2 c= o1;
then
A32: ConsecutiveSet2(A,o2) c= ConsecutiveSet2(A,o1) by Th21;
then
A33: [y,x] in dom h1 by A19,A24,A23,ZFMISC_1:87;
ConsecutiveDelta2(q,o1) in rng Ls by A8,A9,A13,A20,FUNCT_1:def 3;
then
A34: h1 c= f by A20,ZFMISC_1:74;
reconsider x9=x, y9=y as Element of ConsecutiveSet2(A,o1) by A9,A11,A13
,A14,A24,A32;
[x,y] in dom h1 by A19,A24,A23,A32,ZFMISC_1:87;
hence f.(x,y) = h1.(x9,y9) by A34,GRFUNC_1:2
.= h1.(y9,x9) by A21
.= f.(y,x) by A34,A33,GRFUNC_1:2;
end;
end;
hence thesis by A6,A8,Th20;
end;
A35: X[0]
proof
let x,y be Element of ConsecutiveSet2(A,0);
reconsider x9 = x, y9 = y as Element of A by Th14;
thus ConsecutiveDelta2(q,0).(x,y) = d.(x9,y9) by Th18
.= d.(y9,x9) by A1
.= ConsecutiveDelta2(q,0).(y,x) by Th18;
end;
for O being Ordinal holds X[O] from ORDINAL2:sch 1(A35,A2,A5);
hence thesis;
end;
theorem Th27:
for A being non empty set for L being lower-bounded LATTICE st L
is modular for d be BiFunction of A,L st d is symmetric u.t.i. for O being
Ordinal for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta2(q
,O) is u.t.i.
proof
let A be non empty set;
let L be lower-bounded LATTICE;
assume
A1: L is modular;
let d be BiFunction of A,L;
assume that
A2: d is symmetric and
A3: d is u.t.i.;
let O be Ordinal;
let q be QuadrSeq of d;
defpred X[Ordinal] means $1 c= DistEsti(d) implies ConsecutiveDelta2(q,$1)
is u.t.i.;
A4: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume that
A5: O1 c= DistEsti(d) implies ConsecutiveDelta2(q,O1) is u.t.i. and
A6: succ O1 c= DistEsti(d);
A7: O1 in DistEsti(d) by A6,ORDINAL1:21;
then
A8: O1 in dom q by LATTICE5:25;
then q.O1 in rng q by FUNCT_1:def 3;
then
A9: q.O1 in {[u,v,a9,b9] where u is Element of A, v is Element of A, a9
is Element of L, b9 is Element of L: d.(u,v) <= a9"\/"b9} by
LATTICE5:def 13;
let x,y,z be Element of ConsecutiveSet2(A,succ O1);
A10: ConsecutiveDelta2(q,O1) is symmetric by A2,Th26;
reconsider x9 = x, y9 = y, z9 = z as Element of new_set2 ConsecutiveSet2(A
,O1) by Th15;
set f = new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1));
set X = Quadr2(q,O1)`1_4, Y = Quadr2(q,O1)`2_4;
reconsider a = Quadr2(q,O1)`3_4, b = Quadr2(q,O1)`4_4 as Element of L;
A11: dom d = [:A,A:] & d c= ConsecutiveDelta2(q,O1) by Th23,FUNCT_2:def 1;
consider u,v be Element of A, a9,b9 be Element of L such that
A12: q.O1 = [u,v,a9,b9] and
A13: d.(u,v) <= a9"\/"b9 by A9;
A14: Quadr2(q,O1) = [u,v,a9,b9] by A8,A12,Def6;
then
A15: u = X & v = Y;
A16: a9 = a & b9 = b by A14;
d.(u,v) = d.[u,v] .= ConsecutiveDelta2(q,O1).(X,Y) by A15,A11,GRFUNC_1:2;
then
new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) is u.t.i. by A1,A5,A7,A10
,A13,A16,Th12,ORDINAL1:def 2;
then
A17: f.(x9,z9) <= f.(x9,y9) "\/" f.(y9,z9);
ConsecutiveDelta2(q,succ O1) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,
O1), ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th19
.= new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) by LATTICE5:def 15;
hence
ConsecutiveDelta2(q,succ O1).(x,z) <= ConsecutiveDelta2(q,succ O1).(x
,y) "\/" ConsecutiveDelta2(q,succ O1).(y,z) by A17;
end;
A18: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds X[
O2] holds X[O1]
proof
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
let O2 be Ordinal;
assume that
A19: O2 <> 0 & O2 is limit_ordinal and
A20: for O1 be Ordinal st O1 in O2 holds (O1 c= DistEsti(d) implies
ConsecutiveDelta2(q,O1) is u.t.i.) and
A21: O2 c= DistEsti(d);
set CS = ConsecutiveSet2(A,O2);
consider Ls being Sequence such that
A22: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1
) from ORDINAL2:sch 2;
ConsecutiveDelta2(q,O2) = union rng Ls by A19,A22,Th20;
then reconsider f = union rng Ls as BiFunction of CS,L;
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
consider Ts being Sequence such that
A23: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds Ts.O1 = U(O1
) from ORDINAL2:sch 2;
A24: ConsecutiveSet2(A,O2) = union rng Ts by A19,A23,Th16;
f is u.t.i.
proof
let x,y,z be Element of CS;
consider X being set such that
A25: x in X and
A26: X in rng Ts by A24,TARSKI:def 4;
consider o1 being object such that
A27: o1 in dom Ts and
A28: X = Ts.o1 by A26,FUNCT_1:def 3;
consider Y being set such that
A29: y in Y and
A30: Y in rng Ts by A24,TARSKI:def 4;
consider o2 being object such that
A31: o2 in dom Ts and
A32: Y = Ts.o2 by A30,FUNCT_1:def 3;
consider Z being set such that
A33: z in Z and
A34: Z in rng Ts by A24,TARSKI:def 4;
consider o3 being object such that
A35: o3 in dom Ts and
A36: Z = Ts.o3 by A34,FUNCT_1:def 3;
reconsider o1,o2,o3 as Ordinal by A27,A31,A35;
A37: x in ConsecutiveSet2(A,o1) by A23,A25,A27,A28;
A38: Ls.o3 = ConsecutiveDelta2(q,o3) by A22,A23,A35;
then reconsider h3 = Ls.o3 as BiFunction of ConsecutiveSet2(A,o3),L;
A39: h3 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet2(A,o3);
o3 c= DistEsti(d) by A21,A23,A35,ORDINAL1:def 2;
then
A40: ConsecutiveDelta2(q,o3) is u.t.i. by A20,A23,A35;
ConsecutiveDelta2(q,o3) = h3 by A22,A23,A35;
hence h3.(x,z) <= h3.(x,y) "\/" h3.(y,z) by A40;
end;
A41: dom h3 = [:ConsecutiveSet2(A,o3),ConsecutiveSet2(A,o3):] by FUNCT_2:def 1
;
A42: z in ConsecutiveSet2(A,o3) by A23,A33,A35,A36;
A43: Ls.o2 = ConsecutiveDelta2(q,o2) by A22,A23,A31;
then reconsider h2 = Ls.o2 as BiFunction of ConsecutiveSet2(A,o2),L;
A44: h2 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet2(A,o2);
o2 c= DistEsti(d) by A21,A23,A31,ORDINAL1:def 2;
then
A45: ConsecutiveDelta2(q,o2) is u.t.i. by A20,A23,A31;
ConsecutiveDelta2(q,o2) = h2 by A22,A23,A31;
hence h2.(x,z) <= h2.(x,y) "\/" h2.(y,z) by A45;
end;
A46: dom h2 = [:ConsecutiveSet2(A,o2),ConsecutiveSet2(A,o2):] by FUNCT_2:def 1
;
A47: Ls.o1 = ConsecutiveDelta2(q,o1) by A22,A23,A27;
then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet2(A,o1),L;
A48: h1 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet2(A,o1);
o1 c= DistEsti(d) by A21,A23,A27,ORDINAL1:def 2;
then
A49: ConsecutiveDelta2(q,o1) is u.t.i. by A20,A23,A27;
ConsecutiveDelta2(q,o1) = h1 by A22,A23,A27;
hence h1.(x,z) <= h1.(x,y) "\/" h1.(y,z) by A49;
end;
A50: dom h1 = [:ConsecutiveSet2(A,o1),ConsecutiveSet2(A,o1):] by FUNCT_2:def 1
;
A51: y in ConsecutiveSet2(A,o2) by A23,A29,A31,A32;
per cases;
suppose
A52: o1 c= o3;
then
A53: ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o3) by Th21;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose
A54: o2 c= o3;
reconsider z9 = z as Element of ConsecutiveSet2(A,o3) by A23,A33
,A35,A36;
reconsider x9 = x as Element of ConsecutiveSet2(A,o3) by A37,A53;
ConsecutiveDelta2(q,o3) in rng Ls by A22,A23,A35,A38,FUNCT_1:def 3;
then
A55: h3 c= f by A38,ZFMISC_1:74;
A56: ConsecutiveSet2(A,o2) c= ConsecutiveSet2(A,o3) by A54,Th21;
then reconsider y9 = y as Element of ConsecutiveSet2(A,o3) by A51;
[y,z] in dom h3 by A51,A42,A41,A56,ZFMISC_1:87;
then
A57: f.(y,z) = h3.(y9,z9) by A55,GRFUNC_1:2;
[x,z] in dom h3 by A37,A42,A41,A53,ZFMISC_1:87;
then
A58: f.(x,z) = h3.(x9,z9) by A55,GRFUNC_1:2;
[x,y] in dom h3 by A37,A51,A41,A53,A56,ZFMISC_1:87;
then f.(x,y) = h3.(x9,y9) by A55,GRFUNC_1:2;
hence thesis by A39,A57,A58;
end;
suppose
A59: o3 c= o2;
reconsider y9 = y as Element of ConsecutiveSet2(A,o2) by A23,A29
,A31,A32;
ConsecutiveDelta2(q,o2) in rng Ls by A22,A23,A31,A43,FUNCT_1:def 3;
then
A60: h2 c= f by A43,ZFMISC_1:74;
A61: ConsecutiveSet2(A,o3) c= ConsecutiveSet2(A,o2) by A59,Th21;
then reconsider z9 = z as Element of ConsecutiveSet2(A,o2) by A42;
[y,z] in dom h2 by A51,A42,A46,A61,ZFMISC_1:87;
then
A62: f.(y,z) = h2.(y9,z9) by A60,GRFUNC_1:2;
ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o3) by A52,Th21;
then
A63: ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o2) by A61;
then reconsider x9 = x as Element of ConsecutiveSet2(A,o2) by A37;
[x,y] in dom h2 by A37,A51,A46,A63,ZFMISC_1:87;
then
A64: f.(x,y) = h2.(x9,y9) by A60,GRFUNC_1:2;
[x,z] in dom h2 by A37,A42,A46,A61,A63,ZFMISC_1:87;
then f.(x,z) = h2.(x9,z9) by A60,GRFUNC_1:2;
hence thesis by A44,A64,A62;
end;
end;
end;
suppose
A65: o3 c= o1;
then
A66: ConsecutiveSet2(A,o3) c= ConsecutiveSet2(A,o1) by Th21;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose
A67: o1 c= o2;
reconsider y9 = y as Element of ConsecutiveSet2(A,o2) by A23,A29
,A31,A32;
ConsecutiveDelta2(q,o2) in rng Ls by A22,A23,A31,A43,FUNCT_1:def 3;
then
A68: h2 c= f by A43,ZFMISC_1:74;
A69: ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o2) by A67,Th21;
then reconsider x9 = x as Element of ConsecutiveSet2(A,o2) by A37;
[x,y] in dom h2 by A37,A51,A46,A69,ZFMISC_1:87;
then
A70: f.(x,y) = h2.(x9,y9) by A68,GRFUNC_1:2;
ConsecutiveSet2(A,o3) c= ConsecutiveSet2(A,o1) by A65,Th21;
then
A71: ConsecutiveSet2(A,o3) c= ConsecutiveSet2(A,o2) by A69;
then reconsider z9 = z as Element of ConsecutiveSet2(A,o2) by A42;
[y,z] in dom h2 by A51,A42,A46,A71,ZFMISC_1:87;
then
A72: f.(y,z) = h2.(y9,z9) by A68,GRFUNC_1:2;
[x,z] in dom h2 by A37,A42,A46,A69,A71,ZFMISC_1:87;
then f.(x,z) = h2.(x9,z9) by A68,GRFUNC_1:2;
hence thesis by A44,A70,A72;
end;
suppose
A73: o2 c= o1;
reconsider x9 = x as Element of ConsecutiveSet2(A,o1) by A23,A25
,A27,A28;
reconsider z9 = z as Element of ConsecutiveSet2(A,o1) by A42,A66;
ConsecutiveDelta2(q,o1) in rng Ls by A22,A23,A27,A47,FUNCT_1:def 3;
then
A74: h1 c= f by A47,ZFMISC_1:74;
A75: ConsecutiveSet2(A,o2) c= ConsecutiveSet2(A,o1) by A73,Th21;
then reconsider y9 = y as Element of ConsecutiveSet2(A,o1) by A51;
[x,y] in dom h1 by A37,A51,A50,A75,ZFMISC_1:87;
then
A76: f.(x,y) = h1.(x9,y9) by A74,GRFUNC_1:2;
[x,z] in dom h1 by A37,A42,A50,A66,ZFMISC_1:87;
then
A77: f.(x,z) = h1.(x9,z9) by A74,GRFUNC_1:2;
[y,z] in dom h1 by A51,A42,A50,A66,A75,ZFMISC_1:87;
then f.(y,z) = h1.(y9,z9) by A74,GRFUNC_1:2;
hence thesis by A48,A76,A77;
end;
end;
end;
end;
hence thesis by A19,A22,Th20;
end;
A78: X[0]
proof
assume 0 c= DistEsti(d);
let x,y,z be Element of ConsecutiveSet2(A,0);
reconsider x9 = x, y9 = y, z9 = z as Element of A by Th14;
ConsecutiveDelta2(q,0) = d & d.(x9,z9) <= d.(x9,y9) "\/" d.(y9,z9) by A3
,Th18;
hence ConsecutiveDelta2(q,0).(x,z) <= ConsecutiveDelta2(q,0).(x,y) "\/"
ConsecutiveDelta2(q,0).(y,z);
end;
for O being Ordinal holds X[O] from ORDINAL2:sch 1(A78,A4,A18);
hence thesis;
end;
theorem
for A being non empty set for L being lower-bounded modular LATTICE
for d being distance_function of A,L for O being Ordinal for q being QuadrSeq
of d st O c= DistEsti(d) holds ConsecutiveDelta2(q,O) is distance_function of
ConsecutiveSet2(A,O),L by Th25,Th26,Th27;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
func NextSet2(d) -> set equals
ConsecutiveSet2(A,DistEsti(d));
correctness;
end;
registration
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
cluster NextSet2(d) -> non empty;
coherence;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
func NextDelta2(q) -> set equals
ConsecutiveDelta2(q,DistEsti(d));
correctness;
end;
definition
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let q be QuadrSeq of d;
redefine func NextDelta2(q) -> distance_function of NextSet2(d),L; :: redefines NextDelta2 (LATTICE8, definition)
coherence by Th25,Th26,Th27;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let Aq be non empty set;
let dq be distance_function of Aq,L;
pred Aq, dq is_extension2_of A,d means
ex q being QuadrSeq of d st Aq = NextSet2(d) & dq = NextDelta2(q);
end;
theorem Th29:
for A being non empty set for L be lower-bounded LATTICE for d
be distance_function of A,L for Aq be non empty set for dq be distance_function
of Aq,L st Aq, dq is_extension2_of A,d for x,y being Element of A, a,b being
Element of L st d.(x,y) <= a "\/" b ex z1,z2 being Element of Aq st dq.(x,z1) =
a & dq.(z1,z2) = (d.(x,y) "\/" a) "/\" b & dq.(z2,y) = a
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let Aq be non empty set;
let dq be distance_function of Aq,L;
assume Aq, dq is_extension2_of A,d;
then consider q being QuadrSeq of d such that
A1: Aq = NextSet2(d) and
A2: dq = NextDelta2(q);
let x,y be Element of A;
let a,b be Element of L;
A3: rng q = {[x9,y9,a9,b9] where x9 is Element of A, y9 is Element of A, a9
is Element of L, b9 is Element of L: d.(x9,y9) <= a9"\/"b9} by LATTICE5:def 13;
assume d.(x,y) <= a "\/" b;
then [x,y,a,b] in rng q by A3;
then consider o being object such that
A4: o in dom q and
A5: q.o = [x,y,a,b] by FUNCT_1:def 3;
reconsider o as Ordinal by A4;
A6: q.o = Quadr2(q,o) by A4,Def6;
then
A7: x = Quadr2(q,o)`1_4 by A5;
A8: b = Quadr2(q,o)`4_4 by A5,A6;
A9: y = Quadr2(q,o)`2_4 by A5,A6;
reconsider B = ConsecutiveSet2(A,o) as non empty set;
{B} in {{B}, {{B}} } by TARSKI:def 2;
then
A10: {B} in B \/ {{B}, {{B}} } by XBOOLE_0:def 3;
o in DistEsti(d) by A4,LATTICE5:25;
then
A11: succ o c= DistEsti(d) by ORDINAL1:21;
then
A12: ConsecutiveDelta2(q,succ o) c= ConsecutiveDelta2(q,DistEsti(d)) by Th24;
reconsider cd = ConsecutiveDelta2(q,o) as BiFunction of B,L;
reconsider Q = Quadr2(q,o) as Element of [:B,B,the carrier of L,the carrier
of L:];
A13: {{B}} in {{B}, {{B}} } by TARSKI:def 2;
then
A14: {{B}} in new_set2 B by XBOOLE_0:def 3;
ConsecutiveSet2(A,succ o) = new_set2 B by Th15;
then new_set2 B c= ConsecutiveSet2(A,DistEsti(d)) by A11,Th21;
then reconsider z1={B},z2={{B}} as Element of Aq by A1,A10,A14;
take z1,z2;
A15: cd is zeroed by Th25;
A c= B by Th17;
then reconsider xo = x, yo = y as Element of B;
A16: B c= new_set2 B by XBOOLE_1:7;
reconsider x1 = xo, y1 = yo as Element of new_set2 B by A16;
A17: ConsecutiveDelta2(q,succ o) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,o),
ConsecutiveSet2(A,o),L),Quadr2(q,o)) by Th19
.= new_bi_fun2(cd,Q) by LATTICE5:def 15;
dom d = [:A,A:] by FUNCT_2:def 1;
then
A18: [xo,yo] in dom d by ZFMISC_1:87;
d c= cd by Th23;
then
A19: cd.(xo,yo) = d.(x,y) by A18,GRFUNC_1:2;
A20: a = Quadr2(q,o)`3_4 by A5,A6;
A21: dom new_bi_fun2(cd,Q) = [:new_set2 B,new_set2 B:] by FUNCT_2:def 1;
then [x1,{B}] in dom new_bi_fun2(cd,Q) by A10,ZFMISC_1:87;
hence dq.(x,z1) = new_bi_fun2(cd,Q).(x1,{B}) by A2,A12,A17,GRFUNC_1:2
.= cd.(xo,xo)"\/"a by A7,A20,Def4
.= Bottom L"\/"a by A15
.= a by WAYBEL_1:3;
[{B},{{B}}] in dom new_bi_fun2(cd,Q) by A10,A14,A21,ZFMISC_1:87;
hence dq.(z1,z2) = new_bi_fun2(cd,Q).({B},{{B}}) by A2,A12,A17,GRFUNC_1:2
.= (d.(x,y)"\/"a)"/\"b by A7,A9,A20,A8,A19,Def4;
{{B}} in B \/ {{B}, {{B}} } by A13,XBOOLE_0:def 3;
then [{{B}},y1] in dom new_bi_fun2(cd,Q) by A21,ZFMISC_1:87;
hence dq.(z2,y) = new_bi_fun2(cd,Q).({{B}},y1) by A2,A12,A17,GRFUNC_1:2
.= cd.(yo,yo)"\/"a by A9,A20,Def4
.= Bottom L"\/"a by A15
.= a by WAYBEL_1:3;
end;
definition
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
mode ExtensionSeq2 of A,d -> Function means
:Def11:
dom it = NAT & it.0 = [A
,d] & for n being Nat holds ex A9 being non empty set, d9 being
distance_function of A9,L, Aq being non empty set, dq being distance_function
of Aq,L st Aq, dq is_extension2_of A9,d9 & it.n = [A9,d9] & it.(n+1) = [Aq,dq];
existence
proof
defpred P[set,set,set] means (ex A9 being non empty set, d9 being
distance_function of A9,L, Aq being non empty set, dq being distance_function
of Aq,L st Aq, dq is_extension2_of A9,d9 & $2 = [A9,d9] & $3 = [Aq,dq]) or $3=
0 & not ex A9 being non empty set, d9 being distance_function of A9,L, Aq being
non empty set, dq being distance_function of Aq,L st Aq, dq is_extension2_of A9
,d9 & $2 = [A9,d9];
A1: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat;
let x be set;
per cases;
suppose
ex A9 being non empty set, d9 being distance_function of A9,L,
Aq being non empty set, dq being distance_function of Aq,L st Aq, dq
is_extension2_of A9,d9 & x = [A9,d9];
then consider
A9 being non empty set, d9 being distance_function of A9,L,
Aq being non empty set, dq being distance_function of Aq,L such that
A2: Aq, dq is_extension2_of A9,d9 & x = [A9,d9];
take [Aq,dq];
thus thesis by A2;
end;
suppose
A3: not ex A9 being non empty set, d9 being distance_function of
A9,L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq
is_extension2_of A9,d9 & x = [A9,d9];
take 0;
thus thesis by A3;
end;
end;
consider f being Function such that
A4: dom f = NAT and
A5: f.0 = [A,d] and
A6: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:
sch 1( A1);
take f;
thus dom f = NAT by A4;
thus f.0 = [A,d] by A5;
defpred X[Nat] means ex A9 being non empty set, d9 being
distance_function of A9,L, Aq being non empty set, dq being distance_function
of Aq,L st Aq, dq is_extension2_of A9,d9 & f.$1 = [A9,d9] & f.($1+1) = [Aq,dq];
A7: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
given A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L such that
Aq, dq is_extension2_of A9,d9 and
f.k = [A9,d9] and
A8: f.(k+1) = [Aq,dq];
ex A1 being non empty set, d1 being distance_function of A1,L, AQ
being non empty set, DQ being distance_function of AQ,L st AQ, DQ
is_extension2_of A1,d1 & f.(k+1) = [A1,d1]
proof
set Q = the QuadrSeq of dq;
set AQ = NextSet2(dq);
take Aq,dq;
set DQ = NextDelta2(Q);
take AQ,DQ;
thus AQ, DQ is_extension2_of Aq,dq;
thus thesis by A8;
end;
hence thesis by A6;
end;
ex A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L st Aq, dq
is_extension2_of A9,d9 & f.0 = [A9,d9]
proof
set Aq = NextSet2(d);
set q = the QuadrSeq of d;
take A,d;
consider dq being distance_function of Aq,L such that
A9: dq = NextDelta2(q);
take Aq,dq;
thus Aq, dq is_extension2_of A,d by A9;
thus thesis by A5;
end;
then
A10: X[0] by A6;
thus for k being Nat holds X[k] from NAT_1:sch 2(A10, A7);
end;
end;
theorem Th30:
for A being non empty set for L be lower-bounded modular LATTICE
for d be distance_function of A,L for S being ExtensionSeq2 of A,d for k,l
being Nat st k <= l holds (S.k)`1 c= (S.l)`1
proof
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let S be ExtensionSeq2 of A,d;
let k be Nat;
defpred X[Nat] means k <= $1 implies (S.k)`1 c= (S.$1)`1;
A1: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat;
assume that
A2: k <= i implies (S.k)`1 c= (S.i)`1 and
A3: k <= i+1;
per cases by A3,NAT_1:8;
suppose
k = i+1;
hence thesis;
end;
suppose
A4: k <= i;
consider A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L such that
A5: Aq, dq is_extension2_of A9,d9 and
A6: S.i = [A9,d9] and
A7: S.(i+1) = [Aq,dq] by Def11;
A8: (S.i)`1 c= ConsecutiveSet2(A9,DistEsti(d9)) by Th17,A6;
ex q being QuadrSeq of d9 st Aq = NextSet2(d9) & dq = NextDelta2(q)
by A5;
then [Aq,dq]`1 = ConsecutiveSet2(A9,DistEsti(d9));
hence thesis by A2,A4,A8,A7;
end;
end;
A9: X[0] by NAT_1:3;
thus for l being Nat holds X[l] from NAT_1:sch 2(A9, A1);
end;
theorem Th31:
for A being non empty set for L be lower-bounded modular LATTICE
for d be distance_function of A,L for S being ExtensionSeq2 of A,d for k,l
being Nat st k <= l holds (S.k)`2 c= (S.l)`2
proof
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let S be ExtensionSeq2 of A,d;
let k be Nat;
defpred X[Nat] means k <= $1 implies (S.k)`2 c= (S.$1)`2;
A1: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat;
assume that
A2: k <= i implies (S.k)`2 c= (S.i)`2 and
A3: k <= i+1;
per cases by A3,NAT_1:8;
suppose
k = i+1;
hence thesis;
end;
suppose
A4: k <= i;
consider A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L such that
A5: Aq, dq is_extension2_of A9,d9 and
A6: S.i = [A9,d9] and
A7: S.(i+1) = [Aq,dq] by Def11;
consider q being QuadrSeq of d9 such that
Aq = NextSet2(d9) and
A8: dq = NextDelta2(q) by A5;
A9: (S.i)`2 c= ConsecutiveDelta2(q,DistEsti(d9)) by Th23,A6;
[Aq,dq]`2 = ConsecutiveDelta2(q,DistEsti(d9)) by A8;
hence thesis by A2,A4,A9,A7;
end;
end;
A10: X[0] by NAT_1:3;
thus for l being Nat holds X[l] from NAT_1:sch 2(A10, A1);
end;
theorem Th32:
for L be lower-bounded modular LATTICE for S being ExtensionSeq2
of the carrier of L, BasicDF(L) for FS being non empty set st FS = union the
set of all (S.i
)`1 where i is Element of NAT holds union the set of all (S.i)`2 where i
is Element of NAT is distance_function of FS,L
proof
let L be lower-bounded modular LATTICE;
let S be ExtensionSeq2 of the carrier of L, BasicDF(L);
let FS be non empty set;
assume
A1: FS = union the set of all (S.i)`1 where i is Element of NAT;
reconsider FS as non empty set;
set A = the carrier of L;
set FD = union the set of all (S.i)`2 where i is Element of NAT;
now
let x,y be set;
assume that
A2: x in the set of all (S.i)`2 where i is Element of NAT and
A3: y in the set of all (S.i)`2 where i is Element of NAT;
consider k being Element of NAT such that
A4: x = (S.k)`2 by A2;
consider l being Element of NAT such that
A5: y = (S.l)`2 by A3;
k <= l or l <= k;
then x c= y or y c= x by A4,A5,Th31;
hence x,y are_c=-comparable;
end;
then
A6: the set of all (S.i)`2 where i is Element of NAT is c=-linear;
the set of all (S.i)`2 where i is Element of NAT c= PFuncs([:FS,
FS:],A)
proof
let z be object;
assume z in the set of all (S.i)`2 where i is Element of NAT;
then consider j being Element of NAT such that
A7: z = (S.j)`2;
consider A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L such that
Aq, dq is_extension2_of A9,d9 and
A8: S.j = [A9,d9] and
S.(j+1) = [Aq,dq] by Def11;
A9: A9 = [A9,d9]`1;
A9 in the set of all (S.i)`1 where i is Element of NAT
by A9,A8;
then dom d9 = [:A9,A9:] & A9 c= FS by A1,FUNCT_2:def 1,ZFMISC_1:74;
then
A10: rng d9 c= A & dom d9 c= [:FS,FS:] by ZFMISC_1:96;
z = d9 by A7,A8;
hence thesis by A10,PARTFUN1:def 3;
end;
then FD in PFuncs([:FS,FS:],A) by A6,TREES_2:40;
then
A11: ex g being Function st FD = g & dom g c= [:FS,FS:] & rng g c= A by
PARTFUN1:def 3;
(S.0)`1 in the set of all (S.i)`1 where i is Element of NAT;
then reconsider
X = the set of all (S.i)`1 where i is Element of NAT as
non empty set;
set LL = { [:I,I:] where I is Element of X : I in X }, PP = the set of all
[:(S.i)`1,(S.i
)`1:] where i is Element of NAT;
defpred X[object,object] means $2 = (S.$1)`2;
A12: LL = PP
proof
thus LL c= PP
proof
let x be object;
assume x in LL;
then consider J being Element of X such that
A13: x = [:J,J:] and
A14: J in X;
ex j being Element of NAT st J = (S.j)`1 by A14;
hence thesis by A13;
end;
let x be object;
assume x in PP;
then consider j being Element of NAT such that
A15: x = [:(S.j)`1,(S.j)`1:];
(S.j)`1 in X;
hence thesis by A15;
end;
reconsider FD as Function by A11;
A16: for x being object st x in NAT ex y being object st X[x,y];
consider F being Function such that
A17: dom F = NAT and
A18: for x being object st x in NAT holds X[x,F.x] from CLASSES1:sch 1(A16);
A19: rng F = the set of all (S.i)`2 where i is Element of NAT
proof
thus rng F c= the set of all (S.i)`2 where i is Element of NAT
proof
let x be object;
assume x in rng F;
then consider j being object such that
A20: j in dom F and
A21: F.j = x by FUNCT_1:def 3;
reconsider j as Element of NAT by A17,A20;
x = (S.j)`2 by A18,A21;
hence thesis;
end;
let x be object;
assume x in the set of all (S.i)`2 where i is Element of NAT;
then consider j being Element of NAT such that
A22: x = (S.j)`2;
x = F.j by A18,A22;
hence thesis by A17,FUNCT_1:def 3;
end;
F is Function-yielding
proof
let x be object;
assume x in dom F;
then reconsider j = x as Element of NAT by A17;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension2_of A1,d1 and
A23: S.j = [A1,d1] and
S.(j+1) = [Aq1,dq1] by Def11;
[A1,d1]`2 = d1;
hence thesis by A18,A23;
end;
then reconsider F as Function-yielding Function;
A24: rng doms F = PP
proof
thus rng doms F c= PP
proof
let x be object;
assume x in rng doms F;
then consider j being object such that
A25: j in dom doms F and
A26: x = (doms F).j by FUNCT_1:def 3;
A27: j in dom F by A25,FUNCT_6:59;
reconsider j as Element of NAT by A17,A25,FUNCT_6:59;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension2_of A1,d1 and
A28: S.j = [A1,d1] and
S.(j+1) = [Aq1,dq1] by Def11;
A29: [A1,d1]`2 = d1;
x = dom (F.j) by A26,A27,FUNCT_6:22
.= dom d1 by A18,A29,A28
.= [:(S.j)`1,(S.j)`1:] by A28,FUNCT_2:def 1;
hence thesis;
end;
let x be object;
assume x in PP;
then consider j being Element of NAT such that
A30: x = [:(S.j)`1,(S.j)`1:];
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension2_of A1,d1 and
A31: S.j = [A1,d1] and
S.(j+1) = [Aq1,dq1] by Def11;
A32: [A1,d1]`2 = d1;
j in NAT;
then
A33: j in dom doms F by A17,FUNCT_6:59;
x = dom d1 by A30,A31,FUNCT_2:def 1
.= dom (F.j) by A18,A32,A31
.= (doms F).j by A17,FUNCT_6:22;
hence thesis by A33,FUNCT_1:def 3;
end;
now
let x,y be set;
assume that
A34: x in X and
A35: y in X;
consider k being Element of NAT such that
A36: x = (S.k)`1 by A34;
consider l being Element of NAT such that
A37: y = (S.l)`1 by A35;
k <= l or l <= k;
then x c= y or y c= x by A36,A37,Th30;
hence x,y are_c=-comparable;
end;
then X is c=-linear;
then [:FS,FS:] = union rng doms F by A1,A24,A12,LATTICE5:3
.= dom FD by A19,LATTICE5:1;
then reconsider FD as BiFunction of FS,L by A11,FUNCT_2:def 1,RELSET_1:4;
A38: FD is symmetric
proof
let x,y be Element of FS;
consider x1 being set such that
A39: x in x1 and
A40: x1 in X by A1,TARSKI:def 4;
consider k being Element of NAT such that
A41: x1 = (S.k)`1 by A40;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension2_of A1,d1 and
A42: S.k = [A1,d1] and
S.(k+1) = [Aq1,dq1] by Def11;
A43: [A1,d1]`1 = A1;
A44: x in A1 by A39,A41,A42;
[A1,d1]`2 = d1;
then d1 in the set of all (S.i)`2 where i is Element of NAT by A42;
then
A45: d1 c= FD by ZFMISC_1:74;
consider y1 being set such that
A46: y in y1 and
A47: y1 in X by A1,TARSKI:def 4;
consider l being Element of NAT such that
A48: y1 = (S.l)`1 by A47;
consider A2 being non empty set, d2 being distance_function of A2,L, Aq2
being non empty set, dq2 being distance_function of Aq2,L such that
Aq2, dq2 is_extension2_of A2,d2 and
A49: S.l = [A2,d2] and
S.(l+1) = [Aq2,dq2] by Def11;
A50: [A2,d2]`1 = A2;
A51: y in A2 by A46,A48,A49;
[A2,d2]`2 = d2;
then d2 in the set of all (S.i)`2 where i is Element of NAT by A49;
then
A52: d2 c= FD by ZFMISC_1:74;
per cases;
suppose
k <= l;
then A1 c= A2 by A43,A50,Th30,A42,A49;
then reconsider x9=x,y9=y as Element of A2 by A44,A46,A48,A49;
A53: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
hence FD.(x,y) = d2.[x9,y9] by A52,GRFUNC_1:2
.= d2.(x9,y9)
.= d2.(y9,x9) by LATTICE5:def 5
.= FD.[y9,x9] by A52,A53,GRFUNC_1:2
.= FD.(y,x);
end;
suppose
l <= k;
then A2 c= A1 by A43,A50,Th30,A42,A49;
then reconsider x9=x,y9=y as Element of A1
by A39,A41,A42,A51;
A54: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD.(x,y) = d1.[x9,y9] by A45,GRFUNC_1:2
.= d1.(x9,y9)
.= d1.(y9,x9) by LATTICE5:def 5
.= FD.[y9,x9] by A45,A54,GRFUNC_1:2
.= FD.(y,x);
end;
end;
A55: FD is u.t.i.
proof
let x,y,z be Element of FS;
consider x1 being set such that
A56: x in x1 and
A57: x1 in X by A1,TARSKI:def 4;
consider k being Element of NAT such that
A58: x1 = (S.k)`1 by A57;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension2_of A1,d1 and
A59: S.k = [A1,d1] and
S.(k+1) = [Aq1,dq1] by Def11;
A60: [A1,d1]`1 = A1;
A61: x in A1 by A56,A58,A59;
[A1,d1]`2 = d1;
then d1 in the set of all (S.i)`2 where i is Element of NAT by A59;
then
A62: d1 c= FD by ZFMISC_1:74;
A63: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
consider y1 being set such that
A64: y in y1 and
A65: y1 in X by A1,TARSKI:def 4;
consider l being Element of NAT such that
A66: y1 = (S.l)`1 by A65;
consider A2 being non empty set, d2 being distance_function of A2,L, Aq2
being non empty set, dq2 being distance_function of Aq2,L such that
Aq2, dq2 is_extension2_of A2,d2 and
A67: S.l = [A2,d2] and
S.(l+1) = [Aq2,dq2] by Def11;
A68: [A2,d2]`1 = A2;
A69: y in A2 by A64,A66,A67;
[A2,d2]`2 = d2;
then d2 in the set of all (S.i)`2 where i is Element of NAT by A67;
then
A70: d2 c= FD by ZFMISC_1:74;
A71: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
consider z1 being set such that
A72: z in z1 and
A73: z1 in X by A1,TARSKI:def 4;
consider n being Element of NAT such that
A74: z1 = (S.n)`1 by A73;
consider A3 being non empty set, d3 being distance_function of A3,L, Aq3
being non empty set, dq3 being distance_function of Aq3,L such that
Aq3, dq3 is_extension2_of A3,d3 and
A75: S.n = [A3,d3] and
S.(n+1) = [Aq3,dq3] by Def11;
A76: [A3,d3]`1 = A3;
A77: z in A3 by A72,A74,A75;
[A3,d3]`2 = d3;
then d3 in the set of all (S.i)`2 where i is Element of NAT by A75;
then
A78: d3 c= FD by ZFMISC_1:74;
A79: dom d3 = [:A3,A3:] by FUNCT_2:def 1;
per cases;
suppose
k <= l;
then
A80: A1 c= A2 by A60,A68,Th30,A59,A67;
thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z)
proof
per cases;
suppose
l <= n;
then
A81: A2 c= A3 by A68,A76,Th30,A67,A75;
then A1 c= A3 by A80;
then reconsider
x9 = x, y9 = y, z9 = z as Element of A3
by A61,A69,A72,A74,A75,A81;
A82: FD.(y,z) = d3.[y9,z9] by A78,A79,GRFUNC_1:2
.= d3.(y9,z9);
A83: FD.(x,z) = d3.[x9,z9] by A78,A79,GRFUNC_1:2
.= d3.(x9,z9);
FD.(x,y) = d3.[x9,y9] by A78,A79,GRFUNC_1:2
.= d3.(x9,y9);
hence thesis by A82,A83,LATTICE5:def 7;
end;
suppose
n <= l;
then A3 c= A2 by A68,A76,Th30,A67,A75;
then reconsider
x9 = x, y9 = y, z9 = z as Element of A2
by A61,A64,A66,A67,A77,A80;
A84: FD.(y,z) = d2.[y9,z9] by A70,A71,GRFUNC_1:2
.= d2.(y9,z9);
A85: FD.(x,z) = d2.[x9,z9] by A70,A71,GRFUNC_1:2
.= d2.(x9,z9);
FD.(x,y) = d2.[x9,y9] by A70,A71,GRFUNC_1:2
.= d2.(x9,y9);
hence thesis by A84,A85,LATTICE5:def 7;
end;
end;
end;
suppose
l <= k;
then
A86: A2 c= A1 by A60,A68,Th30,A59,A67;
thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z)
proof
per cases;
suppose
k <= n;
then
A87: A1 c= A3 by A60,A76,Th30,A59,A75;
then A2 c= A3 by A86;
then reconsider
x9 = x, y9 = y, z9 = z as Element of A3
by A61,A69,A72,A74,A75,A87;
A88: FD.(y,z) = d3.[y9,z9] by A78,A79,GRFUNC_1:2
.= d3.(y9,z9);
A89: FD.(x,z) = d3.[x9,z9] by A78,A79,GRFUNC_1:2
.= d3.(x9,z9);
FD.(x,y) = d3.[x9,y9] by A78,A79,GRFUNC_1:2
.= d3.(x9,y9);
hence thesis by A88,A89,LATTICE5:def 7;
end;
suppose
n <= k;
then A3 c= A1 by A60,A76,Th30,A59,A75;
then reconsider
x9 = x, y9 = y, z9 = z as Element of A1
by A56,A58,A59,A69,A77,A86;
A90: FD.(y,z) = d1.[y9,z9] by A62,A63,GRFUNC_1:2
.= d1.(y9,z9);
A91: FD.(x,z) = d1.[x9,z9] by A62,A63,GRFUNC_1:2
.= d1.(x9,z9);
FD.(x,y) = d1.[x9,y9] by A62,A63,GRFUNC_1:2
.= d1.(x9,y9);
hence thesis by A90,A91,LATTICE5:def 7;
end;
end;
end;
end;
FD is zeroed
proof
let x be Element of FS;
consider y being set such that
A92: x in y and
A93: y in X by A1,TARSKI:def 4;
consider j being Element of NAT such that
A94: y = (S.j)`1 by A93;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension2_of A1,d1 and
A95: S.j = [A1,d1] and
S.(j+1) = [Aq1,dq1] by Def11;
[A1,d1]`2 = d1;
then d1 in the set of all (S.i)`2 where i is Element of NAT by A95;
then
A96: d1 c= FD by ZFMISC_1:74;
reconsider x9 = x as Element of A1 by A92,A94,A95;
dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD.(x,x) = d1.[x9,x9] by A96,GRFUNC_1:2
.= d1.(x9,x9)
.= Bottom L by LATTICE5:def 6;
end;
hence thesis by A38,A55;
end;
theorem Th33:
for L be lower-bounded modular LATTICE for S being ExtensionSeq2
of the carrier of L, BasicDF(L) for FS being non empty set for FD being
distance_function of FS,L for x,y being Element of FS for a,b being Element of
L st FS = union the set of all (S.i)`1 where i is Element of NAT & FD =
union the set of all (S.i)`2 where i is Element of NAT & FD.(x,y) <= a
"\/"b ex z1,z2 being Element of FS st FD.(x,z1) = a & FD.(z1,z2) = (FD.(x,y)
"\/"a)"/\"b & FD.(z2,y) = a
proof
let L be lower-bounded modular LATTICE;
let S be ExtensionSeq2 of the carrier of L, BasicDF(L);
let FS be non empty set, FD be distance_function of FS,L;
let x,y be Element of FS;
let a,b be Element of L;
assume that
A1: FS = union the set of all (S.i)`1 where i is Element of NAT and
A2: FD = union the set of all (S.i)`2 where i is Element of NAT and
A3: FD.(x,y) <= a"\/"b;
(S.0)`1 in the set of all (S.i)`1 where i is Element of NAT;
then reconsider
X = the set of all (S.i)`1 where i is Element of NAT as
non empty set;
consider x1 being set such that
A4: x in x1 and
A5: x1 in X by A1,TARSKI:def 4;
consider k being Element of NAT such that
A6: x1 = (S.k)`1 by A5;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
A7: Aq1, dq1 is_extension2_of A1,d1 and
A8: S.k = [A1,d1] and
A9: S.(k+1) = [Aq1,dq1] by Def11;
A10: [A1,d1]`1 = A1;
A11: x in A1 by A4,A6,A8;
[A1,d1]`2 = d1;
then d1 in the set of all (S.i)`2 where i is Element of NAT by A8;
then
A12: d1 c= FD by A2,ZFMISC_1:74;
A13: [Aq1,dq1]`1 = Aq1;
then Aq1 in the set of all (S.i)`1 where i is Element of NAT by A9;
then
A14: Aq1 c= FS by A1,ZFMISC_1:74;
[Aq1,dq1]`2 = dq1;
then dq1 in the set of all (S.i)`2 where i is Element of NAT by A9;
then
A15: dq1 c= FD by A2,ZFMISC_1:74;
consider y1 being set such that
A16: y in y1 and
A17: y1 in X by A1,TARSKI:def 4;
consider l being Element of NAT such that
A18: y1 = (S.l)`1 by A17;
consider A2 being non empty set, d2 being distance_function of A2,L, Aq2
being non empty set, dq2 being distance_function of Aq2,L such that
A19: Aq2, dq2 is_extension2_of A2,d2 and
A20: S.l = [A2,d2] and
A21: S.(l+1) = [Aq2,dq2] by Def11;
A22: [A2,d2]`1 = A2;
A23: y in A2 by A16,A18,A20;
[A2,d2]`2 = d2;
then d2 in the set of all (S.i)`2 where i is Element of NAT by A20;
then
A24: d2 c= FD by A2,ZFMISC_1:74;
A25: [Aq2,dq2]`1 = Aq2;
then Aq2 in the set of all (S.i)`1 where i is Element of NAT by A21;
then
A26: Aq2 c= FS by A1,ZFMISC_1:74;
[Aq2,dq2]`2 = dq2;
then dq2 in the set of all (S.i)`2 where i is Element of NAT by A21;
then
A27: dq2 c= FD by A2,ZFMISC_1:74;
per cases;
suppose
k <= l;
then A1 c= A2 by A10,A22,Th30,A8,A20;
then reconsider x9=x,y9=y as Element of A2
by A11,A16,A18,A20;
A2 c= Aq2 by A22,A25,Th30,A20,A21,NAT_1:11;
then reconsider x99 = x9,y99 = y9 as Element of Aq2;
dom d2 = [:A2,A2:] by FUNCT_2:def 1;
then
A28: FD.(x,y) = d2.[x9,y9] by A24,GRFUNC_1:2
.= d2.(x9,y9);
then consider z1,z2 being Element of Aq2 such that
A29: dq2.(x,z1) = a and
A30: dq2.(z1,z2) = (d2.(x9,y9)"\/"a)"/\"b and
A31: dq2.(z2,y) = a by A3,A19,Th29;
reconsider z19 = z1, z29 = z2 as Element of FS by A26;
take z19,z29;
A32: dom dq2 = [:Aq2,Aq2:] by FUNCT_2:def 1;
hence FD.(x,z19) = dq2.[x99,z1] by A27,GRFUNC_1:2
.= a by A29;
thus FD.(z19,z29) = dq2.[z1,z2] by A27,A32,GRFUNC_1:2
.= (FD.(x,y)"\/"a)"/\"b by A28,A30;
thus FD.(z29,y) = dq2.[z2,y99] by A27,A32,GRFUNC_1:2
.= a by A31;
end;
suppose
l <= k;
then A2 c= A1 by A10,A22,Th30,A8,A20;
then reconsider x9=x,y9=y as Element of A1 by A4,A6,A8,A23;
A1 c= Aq1 by A10,A13,Th30,A8,A9,NAT_1:11;
then reconsider x99 = x9,y99 = y9 as Element of Aq1;
dom d1 = [:A1,A1:] by FUNCT_2:def 1;
then
A33: FD.(x,y) = d1.[x9,y9] by A12,GRFUNC_1:2
.= d1.(x9,y9);
then consider z1,z2 being Element of Aq1 such that
A34: dq1.(x,z1) = a and
A35: dq1.(z1,z2) = (d1.(x9,y9)"\/"a)"/\"b and
A36: dq1.(z2,y) = a by A3,A7,Th29;
reconsider z19 = z1, z29 = z2 as Element of FS by A14;
take z19,z29;
A37: dom dq1 = [:Aq1,Aq1:] by FUNCT_2:def 1;
hence FD.(x,z19) = dq1.[x99,z1] by A15,GRFUNC_1:2
.= a by A34;
thus FD.(z19,z29) = dq1.[z1,z2] by A15,A37,GRFUNC_1:2
.= (FD.(x,y)"\/"a)"/\"b by A33,A35;
thus FD.(z29,y) = dq1.[z2,y99] by A15,A37,GRFUNC_1:2
.= a by A36;
end;
end;
Lm3: for m being Element of NAT st m in Seg 4 holds (m = 1 or m = 2 or m = 3
or m = 4)
proof
let m be Element of NAT;
assume
A1: m in Seg 4;
then m <= 4 by FINSEQ_1:1;
then m = 0 or ... or m = 4 by NAT_1:60;
hence thesis by A1,FINSEQ_1:1;
end;
Lm4: for j being Nat st 1 <= j & j < 4 holds j = 1 or j = 2 or j = 3
proof
let j be Nat;
assume that
A1: 1 <= j and
A2: j < 4;
j < 3+1 by A2;
then j <= 3 by NAT_1:13;
then j = 0 or ... or j = 3 by NAT_1:60;
hence thesis by A1;
end;
theorem Th34:
for L be lower-bounded modular LATTICE for S being ExtensionSeq2
of the carrier of L, BasicDF(L) for FS being non empty set for FD being
distance_function of FS,L for f being Homomorphism of L,EqRelLATT FS for e1,e2
being Equivalence_Relation of FS
for x,y being object st f = alpha FD & FS = union
the set of all (S.i)`1 where i is Element of NAT & FD = union the set of all
(S.i)`2
where i is Element of NAT & e1 in the carrier of Image f &
e2 in the carrier of Image f & [x,y] in e1 "\/" e2 ex F being non empty
FinSequence of FS st len F = 2+2 & x,y are_joint_by F,e1,e2
proof
let L be lower-bounded modular LATTICE;
let S be ExtensionSeq2 of the carrier of L, BasicDF(L);
let FS be non empty set;
let FD be distance_function of FS,L;
let f be Homomorphism of L,EqRelLATT FS;
let e1,e2 be Equivalence_Relation of FS;
let x,y be object;
assume that
A1: f = alpha FD and
A2: FS = union the set of all (S.i)`1 where i is Element of NAT &
FD = union the set of all (S.i)`2 where i is Element of NAT and
A3: e1 in the carrier of Image f and
A4: e2 in the carrier of Image f and
A5: [x,y] in e1 "\/" e2;
A6: the carrier of Image f = rng f by YELLOW_0:def 15;
then consider a being object such that
A7: a in dom f and
A8: e1 = f.a by A3,FUNCT_1:def 3;
consider b being object such that
A9: b in dom f and
A10: e2 = f.b by A4,A6,FUNCT_1:def 3;
reconsider a,b as Element of L by A7,A9;
reconsider a,b as Element of L;
consider e being Equivalence_Relation of FS such that
A11: e = f.(a"\/"b) and
A12: for u,v being Element of FS holds [u,v] in e iff FD.(u,v) <= a"\/"b
by A1,LATTICE5:def 8;
consider e29 being Equivalence_Relation of FS such that
A13: e29 = f.b and
A14: for u,v being Element of FS holds [u,v] in e29 iff FD.(u,v) <= b by A1,
LATTICE5:def 8;
consider e19 being Equivalence_Relation of FS such that
A15: e19 = f.a and
A16: for u,v being Element of FS holds [u,v] in e19 iff FD.(u,v) <= a by A1,
LATTICE5:def 8;
field (e1 "\/" e2) = FS by ORDERS_1:12;
then reconsider u = x, v = y as Element of FS by A5,RELAT_1:15;
A17: Seg 4 = { n where n is Nat: 1 <= n & n <= 4 } by FINSEQ_1:def 1;
then
A18: 1 in Seg 4;
e = f.a"\/"f.b by A11,WAYBEL_6:2
.= e1 "\/" e2 by A8,A10,LATTICE5:10;
then
A19: FD.(u,v) <= a"\/"b by A5,A12;
then consider z1,z2 being Element of FS such that
A20: FD.(u,z1) = a and
A21: FD.(z1,z2) = (FD.(u,v)"\/"a)"/\"b and
A22: FD.(z2,v) = a by A2,Th33;
defpred P[set,object] means
($1 = 1 implies $2 = u) & ($1 = 2 implies $2 = z1)
& ($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = v);
A23: for m being Nat st m in Seg 4 ex w being object st P[m,w]
proof
let m be Nat;
assume
A24: m in Seg 4;
per cases by A24,Lm3;
suppose
A25: m = 1;
take x;
thus thesis by A25;
end;
suppose
A26: m = 2;
take z1;
thus thesis by A26;
end;
suppose
A27: m = 3;
take z2;
thus thesis by A27;
end;
suppose
A28: m = 4;
take y;
thus thesis by A28;
end;
end;
ex p being FinSequence st dom p = Seg 4 & for k being Nat st k in Seg 4
holds P[k,p.k] from FINSEQ_1:sch 1(A23);
then consider h being FinSequence such that
A29: dom h = Seg 4 and
A30: for m being Nat st m in Seg 4 holds (m = 1 implies h.m = u) & (m =
2 implies h.m = z1) & (m = 3 implies h.m = z2) & (m = 4 implies h.m = v);
A31: len h = 4 by A29,FINSEQ_1:def 3;
A32: 3 in Seg 4 by A17;
A33: 4 in Seg 4 by A17;
A34: 2 in Seg 4 by A17;
rng h c= FS
proof
let w be object;
assume w in rng h;
then consider j be object such that
A35: j in dom h and
A36: w = h.j by FUNCT_1:def 3;
per cases by A29,A35,Lm3;
suppose
j = 1;
then h.j = u by A30,A18;
hence thesis by A36;
end;
suppose
j = 2;
then h.j = z1 by A30,A34;
hence thesis by A36;
end;
suppose
j = 3;
then h.j = z2 by A30,A32;
hence thesis by A36;
end;
suppose
j = 4;
then h.j = v by A30,A33;
hence thesis by A36;
end;
end;
then reconsider h as FinSequence of FS by FINSEQ_1:def 4;
len h <> 0 by A29,FINSEQ_1:def 3;
then reconsider h as non empty FinSequence of FS;
A37: h.1 = x by A30,A18;
A38: for j being Element of NAT st 1 <= j & j < len h holds (j is odd
implies [h.j,h.(j+1)] in e1) & (j is even implies [h.j,h.(j+1)] in e2)
proof
let j be Element of NAT;
assume
A39: 1 <= j & j < len h;
per cases by A31,A39,Lm4;
suppose
A40: j = 1;
[u,z1] in e19 by A16,A20;
then [h.1,z1] in e19 by A30,A18;
hence thesis by A8,A15,A30,A34,A40;
end;
suppose
A41: j = 2;
FD.(u,v)"\/"a <= a"\/"b"\/"a by A19,WAYBEL_1:2;
then FD.(u,v)"\/"a <= b"\/"(a"\/"a) by LATTICE3:14;
then FD.(u,v)"\/"a <= b"\/"a by YELLOW_5:1;
then (FD.(u,v)"\/"a)"/\"b <= b"/\"(b"\/"a) by WAYBEL_1:1;
then (FD.(u,v)"\/"a)"/\"b <= b by LATTICE3:18;
then [z1,z2] in e29 by A14,A21;
then
A42: [h.2,z2] in e29 by A30,A34;
consider i being Element of NAT such that
A43: i = 1;
2*i = j by A41,A43;
hence thesis by A10,A13,A30,A32,A41,A42;
end;
suppose
A44: j = 3;
[z2,v] in e19 by A16,A22;
then
A45: [h.3,v] in e19 by A30,A32;
consider i being Element of NAT such that
A46: i = 1;
2*i+1 = j by A44,A46;
hence thesis by A8,A15,A30,A33,A44,A45;
end;
end;
take h;
thus len h = 2+2 by A29,FINSEQ_1:def 3;
h.(len h) = h.4 by A29,FINSEQ_1:def 3
.= y by A30,A33;
hence thesis by A37,A38;
end;
theorem Th35:
for L be lower-bounded modular LATTICE holds L
has_a_representation_of_type<= 2
proof
let L be lower-bounded modular LATTICE;
set A = the carrier of L, D = BasicDF(L);
set S = the ExtensionSeq2 of A,D;
set FS = union the set of all (S.i)`1 where i is Element of NAT;
A1: (S.0)`1 in the set of all (S.i)`1 where i is Element of NAT;
A2: S.0 = [A,D] by Def11;
A c= FS by A1,A2,ZFMISC_1:74;
then reconsider FS as non empty set;
reconsider FD = union the set of all (S.i)`2 where i is Element of NAT
as distance_function of FS,L by Th32;
alpha FD is join-preserving
proof
set f = alpha FD;
let a,b be Element of L;
A3: ex_sup_of f.:{a,b},EqRelLATT FS by YELLOW_0:17;
consider e2 being Equivalence_Relation of FS such that
A4: e2 = f.b and
A5: for x,y being Element of FS holds [x,y] in e2 iff FD.(x,y) <= b
by LATTICE5:def 8;
consider e1 being Equivalence_Relation of FS such that
A6: e1 = f.a and
A7: for x,y being Element of FS holds [x,y] in e1 iff FD.(x,y) <= a
by LATTICE5:def 8;
consider e3 being Equivalence_Relation of FS such that
A8: e3 = f.(a "\/" b) and
A9: for x,y being Element of FS holds [x,y] in e3 iff FD.(x,y) <= a
"\/"b by LATTICE5:def 8;
A10: field e2 = FS by ORDERS_1:12;
now
let x,y be object;
A11: b <= b "\/" a by YELLOW_0:22;
assume
A12: [x,y] in e2;
then reconsider x9 = x, y9 = y as Element of FS by A10,RELAT_1:15;
FD.(x9,y9) <= b by A5,A12;
then FD.(x9,y9) <= b "\/" a by A11,ORDERS_2:3;
hence [x,y] in e3 by A9;
end;
then
A13: e2 c= e3;
A14: field e3 = FS by ORDERS_1:12;
for u,v being object holds [u,v] in e3 implies [u,v] in e1 "\/" e2
proof
let u,v be object;
A15: Seg 4 = { n where n is Nat: 1 <= n & n <= 4 } by FINSEQ_1:def 1;
then
A16: 3 in Seg 4;
assume
A17: [u,v] in e3;
then reconsider x = u, y = v as Element of FS by A14,RELAT_1:15;
A18: FD.(x,y) <= a"\/"b by A9,A17;
then consider z1,z2 being Element of FS such that
A19: FD.(x,z1) = a and
A20: FD.(z1,z2) = (FD.(x,y)"\/"a)"/\"b and
A21: FD.(z2,y) = a by Th33;
A22: u in FS by A14,A17,RELAT_1:15;
defpred P[set,object] means
($1 = 1 implies $2 = x) & ($1 = 2 implies $2 =
z1) & ($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = y);
A23: for m being Nat st m in Seg 4 ex w being object st P[m,w]
proof
let m be Nat;
assume
A24: m in Seg 4;
per cases by A24,Lm3;
suppose
A25: m = 1;
take x;
thus thesis by A25;
end;
suppose
A26: m = 2;
take z1;
thus thesis by A26;
end;
suppose
A27: m = 3;
take z2;
thus thesis by A27;
end;
suppose
A28: m = 4;
take y;
thus thesis by A28;
end;
end;
ex p being FinSequence st dom p = Seg 4 & for k being Nat st k in
Seg 4 holds P[k,p.k] from FINSEQ_1:sch 1(A23);
then consider h being FinSequence such that
A29: dom h = Seg 4 and
A30: for m being Nat st m in Seg 4 holds (m = 1 implies h.m = x) & (
m = 2 implies h.m = z1) & (m = 3 implies h.m = z2) & (m = 4 implies h.m = y);
A31: len h = 4 by A29,FINSEQ_1:def 3;
A32: 4 in Seg 4 by A15;
A33: 1 in Seg 4 by A15;
then
A34: u = h.1 by A30;
A35: 2 in Seg 4 by A15;
A36: for j being Nat st 1 <= j & j < len h holds [h.j,h.(j+1)
] in e1 \/ e2
proof
let j be Nat;
assume
A37: 1 <= j & j < len h;
per cases by A31,A37,Lm4;
suppose
A38: j = 1;
[x,z1] in e1 by A7,A19;
then [h.1,z1] in e1 by A30,A33;
then [h.1,h.2] in e1 by A30,A35;
hence thesis by A38,XBOOLE_0:def 3;
end;
suppose
A39: j = 2;
FD.(x,y)"\/"a <= a"\/"b"\/"a by A18,WAYBEL_1:2;
then FD.(x,y)"\/"a <= b"\/"(a"\/"a) by LATTICE3:14;
then FD.(x,y)"\/"a <= b"\/"a by YELLOW_5:1;
then (FD.(x,y)"\/"a)"/\"b <= b"/\"(b"\/"a) by WAYBEL_1:1;
then (FD.(x,y)"\/"a)"/\"b <= b by LATTICE3:18;
then [z1,z2] in e2 by A5,A20;
then [h.2,z2] in e2 by A30,A35;
then [h.2,h.3] in e2 by A30,A16;
hence thesis by A39,XBOOLE_0:def 3;
end;
suppose
A40: j = 3;
[z2,y] in e1 by A7,A21;
then [h.3,y] in e1 by A30,A16;
then [h.3,h.4] in e1 by A30,A32;
hence thesis by A40,XBOOLE_0:def 3;
end;
end;
v = h.4 by A30,A32
.= h.(len h) by A29,FINSEQ_1:def 3;
hence thesis by A22,A31,A34,A36,EQREL_1:28;
end;
then
A41: e3 c= e1 "\/" e2;
A42: field e1 = FS by ORDERS_1:12;
now
let x,y be object;
A43: a <= a "\/" b by YELLOW_0:22;
assume
A44: [x,y] in e1;
then reconsider x9 = x, y9 = y as Element of FS by A42,RELAT_1:15;
FD.(x9,y9) <= a by A7,A44;
then FD.(x9,y9) <= a "\/" b by A43,ORDERS_2:3;
hence [x,y] in e3 by A9;
end;
then e1 c= e3;
then e1 \/ e2 c= e3 by A13,XBOOLE_1:8;
then
A45: e1 "\/" e2 c= e3 by EQREL_1:def 2;
dom f = the carrier of L by FUNCT_2:def 1;
then sup (f.:{a,b}) = sup {f.a,f.b} by FUNCT_1:60
.= f.a "\/" f.b by YELLOW_0:41
.= e1 "\/" e2 by A6,A4,LATTICE5:10
.= f.(a "\/" b) by A8,A45,A41
.= f.sup {a,b} by YELLOW_0:41;
hence thesis by A3;
end;
then reconsider f = alpha FD as Homomorphism of L,EqRelLATT FS by LATTICE5:14
;
A46: dom f = the carrier of L by FUNCT_2:def 1;
A47: ex e being Equivalence_Relation of FS st e in the carrier of Image f &
e <> id FS
proof
A48: {A} <> {{A}}
proof
assume {A} = {{A}};
then {A} in {A} by TARSKI:def 1;
hence contradiction;
end;
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
A49: Aq9, dq9 is_extension2_of A9,d9 and
A50: S.0 = [A9,d9] and
A51: S.(0+1) = [Aq9,dq9] by Def11;
A9 = A & d9 = D by A2,A50,XTUPLE_0:1;
then consider q being QuadrSeq of D such that
A52: Aq9 = NextSet2(D) and
A53: dq9 = NextDelta2(q) by A49;
ConsecutiveSet2(A,{}) = A by Th14;
then reconsider Q = Quadr2(q,{}) as Element of [:A,A,the carrier of L,the
carrier of L:];
A54: (S.1)`2 in the set of all (S.i)`2 where i is Element of NAT;
succ {} c= DistEsti(D) by Th1;
then {} in DistEsti(D) by ORDINAL1:21;
then
A55: {} in dom q by LATTICE5:25;
then q.{} in rng q by FUNCT_1:def 3;
then q.{} in {[u,v,a9,b9] where u is Element of A, v is Element of A, a9
is Element of L, b9 is Element of L: D.(u,v) <= a9"\/"b9} by
LATTICE5:def 13;
then consider u,v be Element of A, a,b be Element of L such that
A56: q.{} = [u,v,a,b] and
D.(u,v) <= a"\/"b;
consider e being Equivalence_Relation of FS such that
A57: e = f.b and
A58: for x,y being Element of FS holds [x,y] in e iff FD.(x,y) <= b
by LATTICE5:def 8;
Quadr2(q,{}) = [u,v,a,b] by A55,A56,Def6;
then
A59: b = Q`4_4;
[Aq9,dq9]`2 = NextDelta2(q) by A53;
then
A60: NextDelta2(q) c= FD by A54,A51,ZFMISC_1:74;
A61: {{A}} in {{A}, {{A}} } by TARSKI:def 2;
then
A62: {{A}} in A \/ {{A}, {{A}} } by XBOOLE_0:def 3;
take e;
e in rng f by A46,A57,FUNCT_1:def 3;
hence e in the carrier of Image f by YELLOW_0:def 15;
A63: (S.1)`1 in the set of all (S.i)`1 where i is Element of NAT;
[Aq9,dq9]`1 = NextSet2(D) by A52;
then
A64: NextSet2(D) c= FS by A63,A51,ZFMISC_1:74;
new_set2 A = new_set2 ConsecutiveSet2(A,{}) by Th14
.= ConsecutiveSet2(A,succ {}) by Th15;
then new_set2 A c= NextSet2(D) by Th1,Th21;
then
A65: new_set2 A c= FS by A64;
A66: {{A}} in new_set2 A by A61,XBOOLE_0:def 3;
A67: {A} in {{A}, {{A}} } by TARSKI:def 2;
then {A} in A \/ {{A}, {{A}} } by XBOOLE_0:def 3;
then reconsider W = {A}, V = {{A}} as Element of FS by A65,A66;
A68: ConsecutiveSet2(A,{}) = A & ConsecutiveDelta2(q,{}) = D by Th14,Th18;
ConsecutiveDelta2(q,succ {}) = new_bi_fun2(BiFun(ConsecutiveDelta2(q
,{}), ConsecutiveSet2(A,{}),L),Quadr2(q,{})) by Th19
.= new_bi_fun2(D,Q) by A68,LATTICE5:def 15;
then new_bi_fun2(D,Q) c= NextDelta2(q) by Th1,Th24;
then
A69: new_bi_fun2(D,Q) c= FD by A60;
dom new_bi_fun2(D,Q) = [:new_set2 A,new_set2 A:] & {A} in new_set2 A
by A67,FUNCT_2:def 1,XBOOLE_0:def 3;
then [{A},{{A}}] in dom new_bi_fun2(D,Q) by A62,ZFMISC_1:87;
then FD.(W,V) = new_bi_fun2(D,Q).({A},{{A}}) by A69,GRFUNC_1:2
.= (D.(Q`1_4,Q`2_4)"\/"(Q`3_4))"/\"(Q`4_4) by Def4;
then FD.(W,V) <= b by A59,YELLOW_0:23;
then [{A},{{A}}] in e by A58;
hence thesis by A48,RELAT_1:def 10;
end;
A70: now
consider e being Equivalence_Relation of FS such that
e in the carrier of Image f and
A71: e <> id FS by A47;
assume FS is trivial;
then consider x being object such that
A72: FS = {x} by ZFMISC_1:131;
A73: [:{x},{x}:] = {[x,x]} & id({x}) = {[x,x]} by SYSREL:13,ZFMISC_1:29;
field e = {x} by A72,EQREL_1:9;
then id FS c= e by A72,RELAT_2:1;
hence contradiction by A72,A71,A73;
end;
D is onto by LATTICE5:40;
then
A74: rng D = A by FUNCT_2:def 3;
for w being object st w in A
ex z being object st z in [:FS,FS:] & w = FD . z
proof
let w be object;
A75: (S.0)`1 in the set of all (S.i)`1 where i is Element of NAT;
A76: (S.0)`2 in the set of all (S.i)`2 where i is Element of NAT;
A77: S.0 = [A,D] by Def11;
A78: D c= FD by A76,A77,ZFMISC_1:74;
assume w in A;
then consider z being object such that
A79: z in [:A,A:] and
A80: D.z = w by A74,FUNCT_2:11;
take z;
A c= FS by A75,A77,ZFMISC_1:74;
then [:A,A:] c= [:FS,FS:] by ZFMISC_1:96;
hence z in [:FS,FS:] by A79;
z in dom D by A79,FUNCT_2:def 1;
hence thesis by A80,A78,GRFUNC_1:2;
end;
then rng FD = A by FUNCT_2:10;
then
A81: FD is onto by FUNCT_2:def 3;
reconsider FS as non trivial set by A70;
take FS;
reconsider f as Homomorphism of L,EqRelLATT FS;
take f;
thus f is one-to-one by A81,LATTICE5:15;
reconsider FD as distance_function of FS,L;
thus Image f is finitely_typed
proof
take FS;
thus for e being object st e in the carrier of Image f holds e is
Equivalence_Relation of FS
proof
let e be object;
assume e in the carrier of Image f;
then e in rng f by YELLOW_0:def 15;
then consider x being object such that
A82: x in dom f and
A83: e = f.x by FUNCT_1:def 3;
reconsider x as Element of L by A82;
ex E being Equivalence_Relation of FS st E = f.x & for u,v being
Element of FS holds [u,v] in E iff FD.(u,v) <= x by LATTICE5:def 8;
hence thesis by A83;
end;
take 2+2;
thus thesis by Th34;
end;
thus ex e being Equivalence_Relation of FS st e in the carrier of Image f &
e <> id FS
proof
A84: {A} <> {{A}}
proof
assume {A} = {{A}};
then {A} in {A} by TARSKI:def 1;
hence contradiction;
end;
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
A85: Aq9, dq9 is_extension2_of A9,d9 and
A86: S.0 = [A9,d9] and
A87: S.(0+1) = [Aq9,dq9] by Def11;
A9 = A & d9 = D by A2,A86,XTUPLE_0:1;
then consider q being QuadrSeq of D such that
A88: Aq9 = NextSet2(D) and
A89: dq9 = NextDelta2(q) by A85;
ConsecutiveSet2(A,{}) = A by Th14;
then reconsider Q = Quadr2(q,{}) as Element of [:A,A,the carrier of L,the
carrier of L:];
A90: (S.1)`2 in the set of all (S.i)`2 where i is Element of NAT;
succ {} c= DistEsti(D) by Th1;
then {} in DistEsti(D) by ORDINAL1:21;
then
A91: {} in dom q by LATTICE5:25;
then q.{} in rng q by FUNCT_1:def 3;
then q.{} in {[u,v,a9,b9] where u is Element of A, v is Element of A, a9
is Element of L, b9 is Element of L: D.(u,v) <= a9"\/"b9} by
LATTICE5:def 13;
then consider u,v be Element of A, a,b be Element of L such that
A92: q.{} = [u,v,a,b] and
D.(u,v) <= a"\/"b;
consider e being Equivalence_Relation of FS such that
A93: e = f.b and
A94: for x,y being Element of FS holds [x,y] in e iff FD.(x,y) <= b
by LATTICE5:def 8;
Quadr2(q,{}) = [u,v,a,b] by A91,A92,Def6;
then
A95: b = Q`4_4;
[Aq9,dq9]`2 = NextDelta2(q) by A89;
then
A96: NextDelta2(q) c= FD by A90,A87,ZFMISC_1:74;
A97: {{A}} in {{A}, {{A}} } by TARSKI:def 2;
then
A98: {{A}} in A \/ {{A}, {{A}} } by XBOOLE_0:def 3;
take e;
e in rng f by A46,A93,FUNCT_1:def 3;
hence e in the carrier of Image f by YELLOW_0:def 15;
A99: (S.1)`1 in the set of all (S.i)`1 where i is Element of NAT;
[Aq9,dq9]`1 = NextSet2(D) by A88;
then
A100: NextSet2(D) c= FS by A99,A87,ZFMISC_1:74;
new_set2 A = new_set2 ConsecutiveSet2(A,{}) by Th14
.= ConsecutiveSet2(A,succ {}) by Th15;
then new_set2 A c= NextSet2(D) by Th1,Th21;
then
A101: new_set2 A c= FS by A100;
A102: {{A}} in new_set2 A by A97,XBOOLE_0:def 3;
A103: {A} in {{A}, {{A}} } by TARSKI:def 2;
then {A} in A \/ {{A}, {{A}} } by XBOOLE_0:def 3;
then reconsider W = {A}, V = {{A}} as Element of FS by A101,A102;
A104: ConsecutiveSet2(A,{}) = A & ConsecutiveDelta2(q,{}) = D by Th14,Th18;
ConsecutiveDelta2(q,succ {}) = new_bi_fun2(BiFun(ConsecutiveDelta2(q
,{}), ConsecutiveSet2(A,{}),L),Quadr2(q,{})) by Th19
.= new_bi_fun2(D,Q) by A104,LATTICE5:def 15;
then new_bi_fun2(D,Q) c= NextDelta2(q) by Th1,Th24;
then
A105: new_bi_fun2(D,Q) c= FD by A96;
dom new_bi_fun2(D,Q) = [:new_set2 A,new_set2 A:] & {A} in new_set2 A
by A103,FUNCT_2:def 1,XBOOLE_0:def 3;
then [{A},{{A}}] in dom new_bi_fun2(D,Q) by A98,ZFMISC_1:87;
then FD.(W,V) = new_bi_fun2(D,Q).({A},{{A}}) by A105,GRFUNC_1:2
.= (D.(Q`1_4,Q`2_4)"\/"(Q`3_4))"/\"(Q`4_4) by Def4;
then FD.(W,V) <= b by A95,YELLOW_0:23;
then [{A},{{A}}] in e by A94;
hence thesis by A84,RELAT_1:def 10;
end;
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 ex
F being non empty FinSequence of FS st len F = 2+2 & x,y are_joint_by F,e1,e2
by Th34;
hence thesis by A47,LATTICE5:13;
end;
:: <=> :: L has_a_representation_of_type<= 2 iff L is modular
::$N Jonsson Theorem for modular lattices
theorem
for L be lower-bounded LATTICE holds L has_a_representation_of_type<=
2 iff L is modular by Th9,Th35;