let A be non empty set ; for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i.
let L be lower-bounded LATTICE; ( L is modular implies for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i. )
assume A1:
L is modular
; for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i.
let d be BiFunction of A,L; ( d is symmetric & d is u.t.i. implies for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i. )
assume that
A2:
d is symmetric
and
A3:
d is 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.
let O be Ordinal; for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i.
let q be QuadrSeq of d; ( O c= DistEsti d implies ConsecutiveDelta2 (q,O) is u.t.i. )
defpred S1[ Ordinal] means ( $1 c= DistEsti d implies ConsecutiveDelta2 (q,$1) is u.t.i. );
A4:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
( S1[O1] implies S1[ succ O1] )
assume that A5:
(
O1 c= DistEsti d implies
ConsecutiveDelta2 (
q,
O1) is
u.t.i. )
and A6:
succ O1 c= DistEsti d
;
ConsecutiveDelta2 (q,(succ O1)) is u.t.i.
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, v is Element of A, a9, 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));
LATTICE5:def 7 (ConsecutiveDelta2 (q,(succ O1))) . (x,z) <= ((ConsecutiveDelta2 (q,(succ O1))) . (x,y)) "\/" ((ConsecutiveDelta2 (q,(succ O1))) . (y,z))
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 ;
set 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 being
Element of
A,
a9,
b9 being
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 = (Quadr2 (q,O1)) `1_4 &
v = (Quadr2 (q,O1)) `2_4 )
;
A16:
(
a9 = a &
b9 = b )
by A14;
d . (
u,
v) =
d . [u,v]
.=
(ConsecutiveDelta2 (q,O1)) . (
((Quadr2 (q,O1)) `1_4),
((Quadr2 (q,O1)) `2_4))
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:
(new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)))) . (
x9,
z9)
<= ((new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)))) . (x9,y9)) "\/" ((new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)))) . (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;
verum
end;
A18:
for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) holds
S1[O1]
proof
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet2 (A,$1)),
L =
ConsecutiveDelta2 (
q,$1);
let O2 be
Ordinal;
( O2 <> 0 & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S1[O2] ) implies S1[O2] )
assume that A19:
(
O2 <> 0 &
O2 is
limit_ordinal )
and A20:
for
O1 being
Ordinal st
O1 in O2 &
O1 c= DistEsti d holds
ConsecutiveDelta2 (
q,
O1) is
u.t.i.
and A21:
O2 c= DistEsti d
;
ConsecutiveDelta2 (q,O2) is u.t.i.
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 = H1(
O1) ) )
from ORDINAL2:sch 2();
ConsecutiveDelta2 (
q,
O2)
= union (rng Ls)
by A19, A22, Th20;
then reconsider f =
union (rng Ls) as
BiFunction of
(ConsecutiveSet2 (A,O2)),
L ;
deffunc H2(
Ordinal)
-> set =
ConsecutiveSet2 (
A,$1);
consider Ts being
Sequence such that A23:
(
dom Ts = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ts . O1 = H2(
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
ConsecutiveSet2 (
A,
O2);
LATTICE5:def 7 f . (x,z) <= (f . (x,y)) "\/" (f . (y,z))
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 =
o1,
o2 =
o2,
o3 =
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);
LATTICE5:def 7 h3 . (x,z) <= (h3 . (x,y)) "\/" (h3 . (y,z))
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;
verum
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);
LATTICE5:def 7 h2 . (x,z) <= (h2 . (x,y)) "\/" (h2 . (y,z))
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;
verum
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);
LATTICE5:def 7 h1 . (x,z) <= (h1 . (x,y)) "\/" (h1 . (y,z))
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;
verum
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
( o1 c= o3 or o3 c= o1 )
;
suppose A52:
o1 c= o3
;
f . (x,z) <= (f . (x,y)) "\/" (f . (y,z))then A53:
ConsecutiveSet2 (
A,
o1)
c= ConsecutiveSet2 (
A,
o3)
by Th21;
thus
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
verumproof
per cases
( o2 c= o3 or o3 c= o2 )
;
suppose A54:
o2 c= o3
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)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
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
by A39, A57, A58;
verum end; suppose A59:
o3 c= o2
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)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
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
by A44, A64, A62;
verum end;
end; end; suppose A65:
o3 c= o1
;
f . (x,z) <= (f . (x,y)) "\/" (f . (y,z))then A66:
ConsecutiveSet2 (
A,
o3)
c= ConsecutiveSet2 (
A,
o1)
by Th21;
thus
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
verumproof
per cases
( o1 c= o2 or o2 c= o1 )
;
suppose A67:
o1 c= o2
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)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
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
by A44, A70, A72;
verum end; suppose A73:
o2 c= o1
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)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
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
by A48, A76, A77;
verum end;
end; end;
end;
hence
ConsecutiveDelta2 (
q,
O2) is
u.t.i.
by A19, A22, Th20;
verum
end;
A78:
S1[ 0 ]
proof
assume
0 c= DistEsti d
;
ConsecutiveDelta2 (q,0) is u.t.i.
let x,
y,
z be
Element of
ConsecutiveSet2 (
A,
0);
LATTICE5:def 7 (ConsecutiveDelta2 (q,0)) . (x,z) <= ((ConsecutiveDelta2 (q,0)) . (x,y)) "\/" ((ConsecutiveDelta2 (q,0)) . (y,z))
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))
;
verum
end;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A78, A4, A18);
hence
( O c= DistEsti d implies ConsecutiveDelta2 (q,O) is u.t.i. )
; verum