let L be complete continuous LATTICE; :: thesis: ( ( 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 ) ) ; :: thesis: L is completely-distributive
thus L is complete ; :: according to WAYBEL_5:def 3 :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: //\ ((\// (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
proof
let x be Element of L; :: thesis: ( x in X implies x is co-prime )
assume x in X ; :: thesis: x is co-prime
then x in PRIME (L ~) by XBOOLE_0:def 4;
then x ~ is prime by Def7;
hence x is co-prime ; :: thesis: verum
end;
A5: inf (rng (Sups )) = Inf by YELLOW_2:def 6;
X is_<=_than Sup
proof
let p be Element of L; :: according to LATTICE3:def 9 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( j1 in J implies ex k being object st S1[j1,k] )
assume j1 in J ; :: thesis: 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;
per cases ( a in A or a in {((F . j) . the Element of K . j)} ) by A13, XBOOLE_0:def 3;
suppose a in A ; :: thesis: ex k being object st S1[j1,k]
then consider k1 being object such that
A15: k1 in dom (F . j) and
A16: a = (F . j) . k1 by A10, FUNCT_1:def 3;
reconsider k1 = k1 as Element of K . j by A15;
[p,((F . j) . k1)] in the InternalRel of L by A14, A16, ORDERS_2:def 5;
hence ex k being object st S1[j1,k] ; :: thesis: verum
end;
suppose a in {((F . j) . the Element of K . j)} ; :: thesis: ex k being object st S1[j1,k]
then a = (F . j) . the Element of K . j by TARSKI:def 1;
then [p,((F . j) . the Element of K . j)] in the InternalRel of L by A14, ORDERS_2:def 5;
hence ex k being object st S1[j1,k] ; :: thesis: verum
end;
end;
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);
now :: thesis: for g being object st g in dom (doms F) holds
g in dom f1
let g be object ; :: thesis: ( g in dom (doms F) implies g in dom f1 )
assume g in dom (doms F) ; :: thesis: g in dom f1
then g in dom F by FUNCT_6:def 2;
hence g in dom f1 by A17; :: thesis: verum
end;
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 ; :: thesis: ( b in dom (doms F) implies f1 . b in (doms F) . b )
assume A22: b in dom (doms F) ; :: thesis: 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; :: thesis: 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)
proof
let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in rng ((Frege F) . f) or p <= b )
assume b in rng ((Frege F) . f) ; :: thesis: p <= b
then consider a being object such that
A25: a in dom ((Frege F) . f) and
A26: b = ((Frege F) . f) . a by FUNCT_1:def 3;
reconsider a = a as Element of J by A25;
f in dom (Frege F) by A24, PARTFUN1:def 2;
then ((Frege F) . f) . a = (F . a) . (f1 . a) by A3, WAYBEL_5:9;
then [p,(((Frege F) . f) . a)] in the InternalRel of L by A18;
hence p <= b by A26, ORDERS_2:def 5; :: thesis: verum
end;
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; :: thesis: 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; :: thesis: verum