let A be non empty set ; for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let L be lower-bounded LATTICE; for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let d be distance_function of A,L; for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let Aq be non empty set ; for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let dq be distance_function of Aq,L; ( Aq,dq is_extension2_of A,d implies for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a ) )
assume
Aq,dq is_extension2_of A,d
; for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
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; for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let a, b be Element of L; ( d . (x,y) <= a "\/" b implies ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a ) )
A3:
rng q = { [x9,y9,a9,b9] where x9, y9 is Element of A, a9, b9 is Element of L : d . (x9,y9) <= a9 "\/" b9 }
by LATTICE5:def 13;
assume
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 )
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 = 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
; ex z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
take
z2
; ( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
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
;
( dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
[{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
;
dq . (z2,y) = a
{{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
;
verum