let L be complete continuous LATTICE; ( ( for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) ) ) implies L is completely-distributive )
assume A1:
for l being Element of L ex X being Subset of L st
( l = sup X & ( for x being Element of L st x in X holds
x is co-prime ) )
; 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 V11() 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)
set l = Inf ;
set X = (waybelow (Inf )) /\ (PRIME (L ~));
A2:
(waybelow (Inf )) /\ (PRIME (L ~)) c= waybelow (Inf )
by XBOOLE_1:17;
reconsider X = (waybelow (Inf )) /\ (PRIME (L ~)) as Subset of L ;
A3:
dom F = J
by PARTFUN1:def 2;
A4:
for x being Element of L st x in X holds
x is co-prime
A5:
inf (rng (Sups )) = Inf
by YELLOW_2:def 6;
X is_<=_than Sup
proof
let p be
Element of
L;
LATTICE3:def 9 ( not p in X or p <= Sup )
defpred S1[
object ,
object ]
means ( $2
in K . $1 &
[p,((F . $1) . $2)] in the
InternalRel of
L );
assume A6:
p in X
;
p <= Sup
A7:
for
j being
object st
j in J holds
ex
k being
object st
S1[
j,
k]
proof
let j1 be
object ;
( j1 in J implies ex k being object st S1[j1,k] )
assume
j1 in J
;
ex k being object st S1[j1,k]
then reconsider j =
j1 as
Element of
J ;
set k = the
Element of
K . j;
dom (Sups ) = J
by A3, FUNCT_2:def 1;
then A8:
(Sups ) . j in rng (Sups )
by FUNCT_1:def 3;
A9:
(
p << Inf &
Sup = sup (rng (F . j)) )
by A2, A6, WAYBEL_3:7, YELLOW_2:def 5;
Sup = (Sups ) . j
by A3, WAYBEL_5:def 1;
then
Inf <= Sup
by A5, A8, YELLOW_2:22;
then consider A being
finite Subset of
L such that A10:
A c= rng (F . j)
and A11:
p <= sup A
by A9, WAYBEL_3:18;
(
ex_sup_of A,
L &
ex_sup_of A \/ {((F . j) . the Element of K . j)},
L )
by YELLOW_0:17;
then
sup A <= sup (A \/ {((F . j) . the Element of K . j)})
by XBOOLE_1:7, YELLOW_0:34;
then A12:
p <= sup (A \/ {((F . j) . the Element of K . j)})
by A11, ORDERS_2:3;
p is
co-prime
by A4, A6;
then consider a being
Element of
L such that A13:
a in A \/ {((F . j) . the Element of K . j)}
and A14:
p <= a
by A12, Th23;
end;
consider f1 being
Function such that A17:
dom f1 = J
and A18:
for
j being
object st
j in J holds
S1[
j,
f1 . j]
from CLASSES1:sch 1(A7);
then A19:
dom (doms F) c= dom f1
;
for
g being
object st
g in dom f1 holds
g in dom (doms F)
by FUNCT_6:def 2, A3, A17;
then
dom f1 c= dom (doms F)
;
then A20:
dom f1 = dom (doms F)
by A19;
A21:
for
b being
object st
b in dom (doms F) holds
f1 . b in (doms F) . b
proof
let b be
object ;
( b in dom (doms F) implies f1 . b in (doms F) . b )
assume A22:
b in dom (doms F)
;
f1 . b in (doms F) . b
then A23:
F . b is
Function of
(K . b), the
carrier of
L
by A17, A19, WAYBEL_5:6;
(doms F) . b =
dom (F . b)
by A3, A17, A19, A22, FUNCT_6:22
.=
K . b
by A23, FUNCT_2:def 1
;
hence
f1 . b in (doms F) . b
by A17, A18, A19, A22;
verum
end;
then reconsider D =
product (doms F) as non
empty set by A20, CARD_3:9;
reconsider f =
f1 as
Element of
product (doms F) by A20, A21, CARD_3:9;
A24:
f1 in product (doms F)
by A20, A21, CARD_3:9;
p is_<=_than rng ((Frege F) . f)
then
p <= inf (rng ((Frege F) . f))
by YELLOW_0:33;
then A27:
p <= Inf
by YELLOW_2:def 6;
reconsider P =
D --> J as
ManySortedSet of
D ;
reconsider R =
Frege F as
DoubleIndexedSet of
P,
L ;
reconsider f2 =
f as
Element of
D ;
Inf in rng (Infs )
by WAYBEL_5:14;
then
Inf <= sup (rng (Infs ))
by YELLOW_2:22;
then
Inf <= Sup
by YELLOW_2:def 5;
hence
p <= Sup
by A27, ORDERS_2:3;
verum
end;
then A28:
sup X <= Sup
by YELLOW_0:32;
( Inf >= Sup & Inf = sup X )
by A1, Th37, WAYBEL_5:16;
hence
//\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L)
by A28, ORDERS_2:2; verum