let A be non empty set ; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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; :: thesis: ( 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.
; :: thesis: 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; :: thesis: 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; :: thesis: ( 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:
S1[ {} ]
proof
assume
{} c= DistEsti d
;
:: thesis: ConsecutiveDelta2 q,{} is u.t.i.
let x,
y,
z be
Element of
ConsecutiveSet2 A,
{} ;
:: according to LATTICE5:def 8 :: thesis: (ConsecutiveDelta2 q,{} ) . x,z <= ((ConsecutiveDelta2 q,{} ) . x,y) "\/" ((ConsecutiveDelta2 q,{} ) . y,z)
reconsider x' =
x,
y' =
y,
z' =
z as
Element of
A by Th15;
A5:
ConsecutiveDelta2 q,
{} = d
by Th19;
d . x',
z' <= (d . x',y') "\/" (d . y',z')
by A3, LATTICE5:def 8;
hence
(ConsecutiveDelta2 q,{} ) . x,
z <= ((ConsecutiveDelta2 q,{} ) . x,y) "\/" ((ConsecutiveDelta2 q,{} ) . y,z)
by A5;
:: thesis: verum
end;
A6:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
:: thesis: ( S1[O1] implies S1[ succ O1] )
assume that A7:
(
O1 c= DistEsti d implies
ConsecutiveDelta2 q,
O1 is
u.t.i. )
and A8:
succ O1 c= DistEsti d
;
:: thesis: ConsecutiveDelta2 q,(succ O1) is u.t.i.
A9:
O1 in DistEsti d
by A8, ORDINAL1:33;
A10:
ConsecutiveDelta2 q,
O1 is
symmetric
by A2, Th27;
let x,
y,
z be
Element of
ConsecutiveSet2 A,
(succ O1);
:: according to LATTICE5:def 8 :: thesis: (ConsecutiveDelta2 q,(succ O1)) . x,z <= ((ConsecutiveDelta2 q,(succ O1)) . x,y) "\/" ((ConsecutiveDelta2 q,(succ O1)) . y,z)
set f =
new_bi_fun2 (ConsecutiveDelta2 q,O1),
(Quadr2 q,O1);
reconsider x' =
x,
y' =
y,
z' =
z as
Element of
new_set2 (ConsecutiveSet2 A,O1) by Th16;
A11:
O1 in dom q
by A9, LATTICE5:28;
then
q . O1 in rng q
by FUNCT_1:def 5;
then
q . O1 in { [u,v,a',b'] where u, v is Element of A, a', b' is Element of L : d . u,v <= a' "\/" b' }
by LATTICE5:def 14;
then consider u,
v being
Element of
A,
a',
b' being
Element of
L such that A12:
(
q . O1 = [u,v,a',b'] &
d . u,
v <= a' "\/" b' )
;
set X =
(Quadr2 q,O1) `1 ;
set Y =
(Quadr2 q,O1) `2 ;
reconsider a =
(Quadr2 q,O1) `3 ,
b =
(Quadr2 q,O1) `4 as
Element of
L ;
A13:
Quadr2 q,
O1 = [u,v,a',b']
by A11, A12, Def7;
then A14:
u = (Quadr2 q,O1) `1
by MCART_1:def 8;
A15:
v = (Quadr2 q,O1) `2
by A13, MCART_1:def 9;
A16:
a' = a
by A13, MCART_1:def 10;
A17:
b' = b
by A13, MCART_1:def 11;
A18:
dom d = [:A,A:]
by FUNCT_2:def 1;
A19:
d c= ConsecutiveDelta2 q,
O1
by Th24;
d . u,
v =
d . [u,v]
.=
(ConsecutiveDelta2 q,O1) . ((Quadr2 q,O1) `1 ),
((Quadr2 q,O1) `2 )
by A14, A15, A18, A19, GRFUNC_1:8
;
then A20:
new_bi_fun2 (ConsecutiveDelta2 q,O1),
(Quadr2 q,O1) is
u.t.i.
by A1, A7, A9, A10, A12, A16, A17, Th12, ORDINAL1:def 2;
A21:
ConsecutiveDelta2 q,
(succ O1) =
new_bi_fun2 (BiFun (ConsecutiveDelta2 q,O1),(ConsecutiveSet2 A,O1),L),
(Quadr2 q,O1)
by Th20
.=
new_bi_fun2 (ConsecutiveDelta2 q,O1),
(Quadr2 q,O1)
by LATTICE5:def 16
;
(new_bi_fun2 (ConsecutiveDelta2 q,O1),(Quadr2 q,O1)) . x',
z' <= ((new_bi_fun2 (ConsecutiveDelta2 q,O1),(Quadr2 q,O1)) . x',y') "\/" ((new_bi_fun2 (ConsecutiveDelta2 q,O1),(Quadr2 q,O1)) . y',z')
by A20, LATTICE5:def 8;
hence
(ConsecutiveDelta2 q,(succ O1)) . x,
z <= ((ConsecutiveDelta2 q,(succ O1)) . x,y) "\/" ((ConsecutiveDelta2 q,(succ O1)) . y,z)
by A21;
:: thesis: verum
end;
A22:
for O1 being Ordinal st O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) holds
S1[O1]
proof
let O2 be
Ordinal;
:: thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S1[O2] ) implies S1[O2] )
assume that A23:
(
O2 <> {} &
O2 is
limit_ordinal & ( for
O1 being
Ordinal st
O1 in O2 &
O1 c= DistEsti d holds
ConsecutiveDelta2 q,
O1 is
u.t.i. ) )
and A24:
O2 c= DistEsti d
;
:: thesis: ConsecutiveDelta2 q,O2 is u.t.i.
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet2 A,$1),
L =
ConsecutiveDelta2 q,$1;
consider Ls being
T-Sequence such that A25:
(
dom Ls = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ls . O1 = H1(
O1) ) )
from ORDINAL2:sch 2();
A26:
ConsecutiveDelta2 q,
O2 = union (rng Ls)
by A23, A25, Th21;
deffunc H2(
Ordinal)
-> set =
ConsecutiveSet2 A,$1;
consider Ts being
T-Sequence such that A27:
(
dom Ts = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ts . O1 = H2(
O1) ) )
from ORDINAL2:sch 2();
A28:
ConsecutiveSet2 A,
O2 = union (rng Ts)
by A23, A27, Th17;
set CS =
ConsecutiveSet2 A,
O2;
reconsider f =
union (rng Ls) as
BiFunction of
(ConsecutiveSet2 A,O2),
L by A26;
f is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet2 A,
O2;
:: according to LATTICE5:def 8 :: thesis: f . x,z <= (f . x,y) "\/" (f . y,z)
consider X being
set such that A29:
(
x in X &
X in rng Ts )
by A28, TARSKI:def 4;
consider o1 being
set such that A30:
(
o1 in dom Ts &
X = Ts . o1 )
by A29, FUNCT_1:def 5;
consider Y being
set such that A31:
(
y in Y &
Y in rng Ts )
by A28, TARSKI:def 4;
consider o2 being
set such that A32:
(
o2 in dom Ts &
Y = Ts . o2 )
by A31, FUNCT_1:def 5;
consider Z being
set such that A33:
(
z in Z &
Z in rng Ts )
by A28, TARSKI:def 4;
consider o3 being
set such that A34:
(
o3 in dom Ts &
Z = Ts . o3 )
by A33, FUNCT_1:def 5;
reconsider o1 =
o1,
o2 =
o2,
o3 =
o3 as
Ordinal by A30, A32, A34;
A35:
x in ConsecutiveSet2 A,
o1
by A27, A29, A30;
A36:
y in ConsecutiveSet2 A,
o2
by A27, A31, A32;
A37:
z in ConsecutiveSet2 A,
o3
by A27, A33, A34;
A38:
Ls . o1 = ConsecutiveDelta2 q,
o1
by A25, A27, A30;
then reconsider h1 =
Ls . o1 as
BiFunction of
(ConsecutiveSet2 A,o1),
L ;
A39:
h1 is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet2 A,
o1;
:: according to LATTICE5:def 8 :: thesis: h1 . x,z <= (h1 . x,y) "\/" (h1 . y,z)
A40:
ConsecutiveDelta2 q,
o1 = h1
by A25, A27, A30;
o1 c= DistEsti d
by A24, A27, A30, ORDINAL1:def 2;
then
ConsecutiveDelta2 q,
o1 is
u.t.i.
by A23, A27, A30;
hence
h1 . x,
z <= (h1 . x,y) "\/" (h1 . y,z)
by A40, LATTICE5:def 8;
:: thesis: verum
end;
A41:
dom h1 = [:(ConsecutiveSet2 A,o1),(ConsecutiveSet2 A,o1):]
by FUNCT_2:def 1;
A42:
Ls . o2 = ConsecutiveDelta2 q,
o2
by A25, A27, A32;
then reconsider h2 =
Ls . o2 as
BiFunction of
(ConsecutiveSet2 A,o2),
L ;
A43:
h2 is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet2 A,
o2;
:: according to LATTICE5:def 8 :: thesis: h2 . x,z <= (h2 . x,y) "\/" (h2 . y,z)
A44:
ConsecutiveDelta2 q,
o2 = h2
by A25, A27, A32;
o2 c= DistEsti d
by A24, A27, A32, ORDINAL1:def 2;
then
ConsecutiveDelta2 q,
o2 is
u.t.i.
by A23, A27, A32;
hence
h2 . x,
z <= (h2 . x,y) "\/" (h2 . y,z)
by A44, LATTICE5:def 8;
:: thesis: verum
end;
A45:
dom h2 = [:(ConsecutiveSet2 A,o2),(ConsecutiveSet2 A,o2):]
by FUNCT_2:def 1;
A46:
Ls . o3 = ConsecutiveDelta2 q,
o3
by A25, A27, A34;
then reconsider h3 =
Ls . o3 as
BiFunction of
(ConsecutiveSet2 A,o3),
L ;
A47:
h3 is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet2 A,
o3;
:: according to LATTICE5:def 8 :: thesis: h3 . x,z <= (h3 . x,y) "\/" (h3 . y,z)
A48:
ConsecutiveDelta2 q,
o3 = h3
by A25, A27, A34;
o3 c= DistEsti d
by A24, A27, A34, ORDINAL1:def 2;
then
ConsecutiveDelta2 q,
o3 is
u.t.i.
by A23, A27, A34;
hence
h3 . x,
z <= (h3 . x,y) "\/" (h3 . y,z)
by A48, LATTICE5:def 8;
:: thesis: verum
end;
A49:
dom h3 = [:(ConsecutiveSet2 A,o3),(ConsecutiveSet2 A,o3):]
by FUNCT_2:def 1;
per cases
( o1 c= o3 or o3 c= o1 )
;
suppose A50:
o1 c= o3
;
:: thesis: f . x,z <= (f . x,y) "\/" (f . y,z)then A51:
ConsecutiveSet2 A,
o1 c= ConsecutiveSet2 A,
o3
by Th22;
thus
(f . x,y) "\/" (f . y,z) >= f . x,
z
:: thesis: verumproof
per cases
( o2 c= o3 or o3 c= o2 )
;
suppose
o2 c= o3
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A52:
ConsecutiveSet2 A,
o2 c= ConsecutiveSet2 A,
o3
by Th22;
then reconsider y' =
y as
Element of
ConsecutiveSet2 A,
o3 by A36;
reconsider x' =
x as
Element of
ConsecutiveSet2 A,
o3 by A35, A51;
reconsider z' =
z as
Element of
ConsecutiveSet2 A,
o3 by A27, A33, A34;
ConsecutiveDelta2 q,
o3 in rng Ls
by A25, A27, A34, A46, FUNCT_1:def 5;
then A53:
h3 c= f
by A46, ZFMISC_1:92;
A54:
[x,y] in dom h3
by A35, A36, A49, A51, A52, ZFMISC_1:106;
A55:
[y,z] in dom h3
by A36, A37, A49, A52, ZFMISC_1:106;
A56:
[x,z] in dom h3
by A35, A37, A49, A51, ZFMISC_1:106;
A57:
f . x,
y = h3 . x',
y'
by A53, A54, GRFUNC_1:8;
A58:
f . y,
z = h3 . y',
z'
by A53, A55, GRFUNC_1:8;
f . x,
z = h3 . x',
z'
by A53, A56, GRFUNC_1:8;
hence
(f . x,y) "\/" (f . y,z) >= f . x,
z
by A47, A57, A58, LATTICE5:def 8;
:: thesis: verum end; suppose
o3 c= o2
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A59:
ConsecutiveSet2 A,
o3 c= ConsecutiveSet2 A,
o2
by Th22;
then reconsider z' =
z as
Element of
ConsecutiveSet2 A,
o2 by A37;
ConsecutiveSet2 A,
o1 c= ConsecutiveSet2 A,
o3
by A50, Th22;
then A60:
ConsecutiveSet2 A,
o1 c= ConsecutiveSet2 A,
o2
by A59, XBOOLE_1:1;
then reconsider x' =
x as
Element of
ConsecutiveSet2 A,
o2 by A35;
reconsider y' =
y as
Element of
ConsecutiveSet2 A,
o2 by A27, A31, A32;
ConsecutiveDelta2 q,
o2 in rng Ls
by A25, A27, A32, A42, FUNCT_1:def 5;
then A61:
h2 c= f
by A42, ZFMISC_1:92;
A62:
[x,y] in dom h2
by A35, A36, A45, A60, ZFMISC_1:106;
A63:
[y,z] in dom h2
by A36, A37, A45, A59, ZFMISC_1:106;
A64:
[x,z] in dom h2
by A35, A37, A45, A59, A60, ZFMISC_1:106;
A65:
f . x,
y = h2 . x',
y'
by A61, A62, GRFUNC_1:8;
A66:
f . y,
z = h2 . y',
z'
by A61, A63, GRFUNC_1:8;
f . x,
z = h2 . x',
z'
by A61, A64, GRFUNC_1:8;
hence
(f . x,y) "\/" (f . y,z) >= f . x,
z
by A43, A65, A66, LATTICE5:def 8;
:: thesis: verum end;
end; end; suppose A67:
o3 c= o1
;
:: thesis: f . x,z <= (f . x,y) "\/" (f . y,z)then A68:
ConsecutiveSet2 A,
o3 c= ConsecutiveSet2 A,
o1
by Th22;
thus
(f . x,y) "\/" (f . y,z) >= f . x,
z
:: thesis: verumproof
per cases
( o1 c= o2 or o2 c= o1 )
;
suppose
o1 c= o2
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A69:
ConsecutiveSet2 A,
o1 c= ConsecutiveSet2 A,
o2
by Th22;
then reconsider x' =
x as
Element of
ConsecutiveSet2 A,
o2 by A35;
ConsecutiveSet2 A,
o3 c= ConsecutiveSet2 A,
o1
by A67, Th22;
then A70:
ConsecutiveSet2 A,
o3 c= ConsecutiveSet2 A,
o2
by A69, XBOOLE_1:1;
then reconsider z' =
z as
Element of
ConsecutiveSet2 A,
o2 by A37;
reconsider y' =
y as
Element of
ConsecutiveSet2 A,
o2 by A27, A31, A32;
ConsecutiveDelta2 q,
o2 in rng Ls
by A25, A27, A32, A42, FUNCT_1:def 5;
then A71:
h2 c= f
by A42, ZFMISC_1:92;
A72:
[x,y] in dom h2
by A35, A36, A45, A69, ZFMISC_1:106;
A73:
[y,z] in dom h2
by A36, A37, A45, A70, ZFMISC_1:106;
A74:
[x,z] in dom h2
by A35, A37, A45, A69, A70, ZFMISC_1:106;
A75:
f . x,
y = h2 . x',
y'
by A71, A72, GRFUNC_1:8;
A76:
f . y,
z = h2 . y',
z'
by A71, A73, GRFUNC_1:8;
f . x,
z = h2 . x',
z'
by A71, A74, GRFUNC_1:8;
hence
(f . x,y) "\/" (f . y,z) >= f . x,
z
by A43, A75, A76, LATTICE5:def 8;
:: thesis: verum end; suppose
o2 c= o1
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A77:
ConsecutiveSet2 A,
o2 c= ConsecutiveSet2 A,
o1
by Th22;
then reconsider y' =
y as
Element of
ConsecutiveSet2 A,
o1 by A36;
reconsider z' =
z as
Element of
ConsecutiveSet2 A,
o1 by A37, A68;
reconsider x' =
x as
Element of
ConsecutiveSet2 A,
o1 by A27, A29, A30;
ConsecutiveDelta2 q,
o1 in rng Ls
by A25, A27, A30, A38, FUNCT_1:def 5;
then A78:
h1 c= f
by A38, ZFMISC_1:92;
A79:
[x,y] in dom h1
by A35, A36, A41, A77, ZFMISC_1:106;
A80:
[y,z] in dom h1
by A36, A37, A41, A68, A77, ZFMISC_1:106;
A81:
[x,z] in dom h1
by A35, A37, A41, A68, ZFMISC_1:106;
A82:
f . x,
y = h1 . x',
y'
by A78, A79, GRFUNC_1:8;
A83:
f . y,
z = h1 . y',
z'
by A78, A80, GRFUNC_1:8;
f . x,
z = h1 . x',
z'
by A78, A81, GRFUNC_1:8;
hence
(f . x,y) "\/" (f . y,z) >= f . x,
z
by A39, A82, A83, LATTICE5:def 8;
:: thesis: verum end;
end; end;
end;
hence
ConsecutiveDelta2 q,
O2 is
u.t.i.
by A23, A25, Th21;
:: thesis: verum
end;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A4, A6, A22);
hence
( O c= DistEsti d implies ConsecutiveDelta2 q,O is u.t.i. )
; :: thesis: verum