let L be complete LATTICE; ( L is completely-distributive iff for J being non empty set
for K being V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf )
thus
( L is completely-distributive implies for J being non empty set
for K being V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf )
( ( for J being non empty set
for K being V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf ) implies L is completely-distributive )proof
assume that
L is
complete
and A1:
for
J being non
empty set for
K being
V8()
ManySortedSet of
J for
F being
DoubleIndexedSet of
K,
L holds
Inf = Sup
;
WAYBEL_5:def 3 for J being non empty set
for K being V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf
let J be non
empty set ;
for K being V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf let K be
V8()
ManySortedSet of
J;
for F being DoubleIndexedSet of K,L holds Sup = Inf let F be
DoubleIndexedSet of
K,
L;
Sup = Inf
A2:
Inf = Sup
by A1;
A3:
dom K = J
by PARTFUN1:def 2;
A4:
doms (Frege F) = (product (doms F)) --> J
by Th45;
A6:
doms F = K
by Th45;
rng (Infs ) is_<=_than Sup
proof
reconsider J9 =
product (doms (Frege F)) as non
empty set ;
let a be
Element of
L;
LATTICE3:def 9 ( not a in rng (Infs ) or a <= Sup )
reconsider K9 =
J9 --> (product (doms F)) as
ManySortedSet of
J9 ;
reconsider G =
Frege (Frege F) as
DoubleIndexedSet of
K9,
L ;
assume
a in rng (Infs )
;
a <= Sup
then consider g being
Element of
J9 such that A8:
a = Inf
by WAYBEL_5:14;
reconsider g9 =
g as
Function ;
deffunc H1(
object )
-> set =
{ (f . (g9 . f)) where f is Element of product (doms F) : g9 . f = $1 } ;
A9:
dom ((product (doms F)) --> J) = product (doms F)
;
then consider j being
Element of
J such that A13:
(K . j) \ H1(
j)
= {}
;
A14:
rng (F . j) c= rng (G . g)
proof
let z be
object ;
TARSKI:def 3 ( not z in rng (F . j) or z in rng (G . g) )
assume
z in rng (F . j)
;
z in rng (G . g)
then consider u being
object such that A15:
u in dom (F . j)
and A16:
z = (F . j) . u
by FUNCT_1:def 3;
reconsider u =
u as
Element of
K . j by A15;
u in H1(
j)
by A13, XBOOLE_0:def 5;
then consider f being
Element of
product (doms F) such that A17:
u = f . (g9 . f)
and A18:
g9 . f = j
;
A:
(
G . g = (Frege F) .. g9 &
(Frege F) . f = F .. f )
by PRALG_2:def 2;
consider gg being
Function such that BB:
(
f = gg &
dom gg = dom (doms F) & ( for
y being
object st
y in dom (doms F) holds
gg . y in (doms F) . y ) )
by CARD_3:def 5;
A25:
dom F = J
by PARTFUN1:def 2;
BC:
dom f = dom F
by FUNCT_6:def 2, BB;
j in (dom F) /\ (dom f)
by A25, BC;
then
j in dom (F .. f)
by PRALG_1:def 19;
then WW:
(F .. f) . j = (F . j) . (f . j)
by PRALG_1:def 19;
A27:
dom (Frege F) = product (doms F)
by PARTFUN1:def 2;
consider gg1 being
Function such that BB:
(
g = gg1 &
dom gg1 = dom (doms (Frege F)) & ( for
y being
object st
y in dom (doms (Frege F)) holds
gg1 . y in (doms (Frege F)) . y ) )
by CARD_3:def 5;
f in dom (Frege F)
by A27;
then
f in dom (doms (Frege F))
by FUNCT_6:def 2;
then
f in (dom (Frege F)) /\ (dom g9)
by A27, BB, XBOOLE_0:def 4;
then
f in dom ((Frege F) .. g9)
by PRALG_1:def 19;
then
(G . g) . f = (F .. f) . j
by A18, PRALG_1:def 19, A;
then A19:
(G . g) . f = z
by A16, A17, A18, WW;
(
dom (G . g) = K9 . g &
K9 . g = product (doms F) )
by FUNCT_2:def 1;
hence
z in rng (G . g)
by A19, FUNCT_1:def 3;
verum
end;
(
ex_inf_of rng (G . g),
L &
ex_inf_of rng (F . j),
L )
by YELLOW_0:17;
then
inf (rng (G . g)) <= inf (rng (F . j))
by A14, YELLOW_0:35;
then
a <= inf (rng (F . j))
by A8, YELLOW_2:def 6;
then A20:
a <= Inf
by YELLOW_2:def 6;
Inf in rng (Infs )
by WAYBEL_5:14;
then
Inf <= sup (rng (Infs ))
by YELLOW_2:22;
then
a <= sup (rng (Infs ))
by A20, ORDERS_2:3;
hence
a <= Sup
by YELLOW_2:def 5;
verum
end;
then
sup (rng (Infs )) <= Sup
by YELLOW_0:32;
then A21:
Sup <= Sup
by YELLOW_2:def 5;
Sup <= Inf
by Th47;
hence
Sup = Inf
by A2, A21, ORDERS_2:2;
verum
end;
assume A22:
for J being non empty set
for K being V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf
; L is completely-distributive
thus
L is complete
; WAYBEL_5:def 3 for b1 being set
for b2 being set
for b3 being ManySortedFunction of b2,b1 --> the carrier of L holds //\ ((\// (b3,L)),L) = \\/ ((/\\ ((Frege b3),L)),L)
let J be non empty set ; for b1 being set
for b2 being ManySortedFunction of b1,J --> the carrier of L holds //\ ((\// (b2,L)),L) = \\/ ((/\\ ((Frege b2),L)),L)
let K be V8() ManySortedSet of J; for b1 being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b1,L)),L) = \\/ ((/\\ ((Frege b1),L)),L)
let F be DoubleIndexedSet of K,L; //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L)
A23:
dom K = J
by PARTFUN1:def 2;
A24:
doms (Frege F) = (product (doms F)) --> J
by Th45;
A25:
dom F = J
by PARTFUN1:def 2;
A26:
doms F = K
by Th45;
A27:
dom (Frege F) = product (doms F)
by PARTFUN1:def 2;
rng (Sups ) is_>=_than Inf
proof
reconsider J9 =
product (doms (Frege F)) as non
empty set ;
let a be
Element of
L;
LATTICE3:def 8 ( not a in rng (Sups ) or Inf <= a )
reconsider K9 =
J9 --> (product (doms F)) as
ManySortedSet of
J9 ;
reconsider G =
Frege (Frege F) as
DoubleIndexedSet of
K9,
L ;
assume
a in rng (Sups )
;
Inf <= a
then consider g being
Element of
J9 such that A28:
a = Sup
by WAYBEL_5:14;
reconsider g9 =
g as
Function ;
deffunc H1(
object )
-> set =
{ (f . (g9 . f)) where f is Element of product (doms F) : g9 . f = $1 } ;
A29:
dom ((product (doms F)) --> J) = product (doms F)
;
then consider j being
Element of
J such that A33:
(K . j) \ H1(
j)
= {}
;
A34:
rng (F . j) c= rng (G . g)
proof
let z be
object ;
TARSKI:def 3 ( not z in rng (F . j) or z in rng (G . g) )
assume
z in rng (F . j)
;
z in rng (G . g)
then consider u being
object such that A35:
u in dom (F . j)
and A36:
z = (F . j) . u
by FUNCT_1:def 3;
reconsider u =
u as
Element of
K . j by A35;
u in H1(
j)
by A33, XBOOLE_0:def 5;
then consider f being
Element of
product (doms F) such that A37:
u = f . (g9 . f)
and A38:
g9 . f = j
;
a37:
(
G . g = (Frege F) .. g9 &
(Frege F) . f = F .. f )
by PRALG_2:def 2;
consider gg being
Function such that BB:
(
f = gg &
dom gg = dom (doms F) & ( for
y being
object st
y in dom (doms F) holds
gg . y in (doms F) . y ) )
by CARD_3:def 5;
dom F = dom f
by BB, FUNCT_6:def 2;
then
j in (dom F) /\ (dom f)
by A25;
then Z1:
j in dom (F .. f)
by PRALG_1:def 19;
consider gg1 being
Function such that BB:
(
g = gg1 &
dom gg1 = dom (doms (Frege F)) & ( for
y being
object st
y in dom (doms (Frege F)) holds
gg1 . y in (doms (Frege F)) . y ) )
by CARD_3:def 5;
f in dom (Frege F)
by A27;
then
f in dom g9
by BB, FUNCT_6:def 2;
then
f in (dom (Frege F)) /\ (dom g9)
by A27, XBOOLE_0:def 4;
then a38:
f in dom ((Frege F) .. g9)
by PRALG_1:def 19;
(G . g) . f = ((Frege F) . f) . (g9 . f)
by a37, a38, PRALG_1:def 19;
then A39:
(G . g) . f = z
by Z1, A36, a37, A37, A38, PRALG_1:def 19;
(
dom (G . g) = K9 . g &
K9 . g = product (doms F) )
by FUNCT_2:def 1;
hence
z in rng (G . g)
by A39, FUNCT_1:def 3;
verum
end;
(
ex_sup_of rng (G . g),
L &
ex_sup_of rng (F . j),
L )
by YELLOW_0:17;
then
sup (rng (G . g)) >= sup (rng (F . j))
by A34, YELLOW_0:34;
then
a >= sup (rng (F . j))
by A28, YELLOW_2:def 5;
then A40:
a >= Sup
by YELLOW_2:def 5;
Sup in rng (Sups )
by WAYBEL_5:14;
then
Sup >= inf (rng (Sups ))
by YELLOW_2:22;
then
a >= inf (rng (Sups ))
by A40, ORDERS_2:3;
hence
Inf <= a
by YELLOW_2:def 6;
verum
end;
then
inf (rng (Sups )) >= Inf
by YELLOW_0:33;
then A41:
Inf >= Inf
by YELLOW_2:def 6;
( Inf >= Sup & Sup = Inf )
by A22, WAYBEL_5:16;
hence
//\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L)
by A41, ORDERS_2:2; verum