let L be lower-bounded continuous sup-Semilattice; :: thesis: SupMap L is upper_adjoint

set P = InclPoset (Ids L);

set r = SupMap L;

deffunc H_{1}( Element of L) -> Element of the carrier of (InclPoset (Ids L)) = inf ((SupMap L) " (uparrow {$1}));

ex d being Function of L,(InclPoset (Ids L)) st

for t being Element of L holds d . t = H_{1}(t)
from FUNCT_2:sch 4();

then consider d being Function of L,(InclPoset (Ids L)) such that

A1: for t being Element of L holds d . t = inf ((SupMap L) " (uparrow {t})) ;

for t being Element of L holds d . t is_minimum_of (SupMap L) " (uparrow t)

hence SupMap L is upper_adjoint by WAYBEL_1:def 11; :: thesis: verum

set P = InclPoset (Ids L);

set r = SupMap L;

deffunc H

ex d being Function of L,(InclPoset (Ids L)) st

for t being Element of L holds d . t = H

then consider d being Function of L,(InclPoset (Ids L)) such that

A1: for t being Element of L holds d . t = inf ((SupMap L) " (uparrow {t})) ;

for t being Element of L holds d . t is_minimum_of (SupMap L) " (uparrow t)

proof

then
[(SupMap L),d] is Galois
by WAYBEL_1:10;
let t be Element of L; :: thesis: d . t is_minimum_of (SupMap L) " (uparrow t)

set I = inf ((SupMap L) " (uparrow t));

reconsider I9 = inf ((SupMap L) " (uparrow t)) as Ideal of L by YELLOW_2:41;

A2: d . t = inf ((SupMap L) " (uparrow {t})) by A1

.= inf ((SupMap L) " (uparrow t)) by WAYBEL_0:def 18 ;

inf ((SupMap L) " (uparrow t)) in the carrier of (InclPoset (Ids L)) ;

then inf ((SupMap L) " (uparrow t)) in Ids L by YELLOW_1:1;

then A3: inf ((SupMap L) " (uparrow t)) in dom (SupMap L) by YELLOW_2:49;

consider J being Ideal of L such that

A4: t <= sup J and

A5: for K being Ideal of L st t <= sup K holds

J c= K by Lm3;

reconsider J9 = J as Element of (InclPoset (Ids L)) by YELLOW_2:41;

A6: for K being Element of (InclPoset (Ids L)) st (SupMap L) " (uparrow t) is_>=_than K holds

K <= J9

then t <= (SupMap L) . (inf ((SupMap L) " (uparrow t))) by YELLOW_2:def 3;

then (SupMap L) . (inf ((SupMap L) " (uparrow t))) in uparrow t by WAYBEL_0:18;

then ( ex_inf_of (SupMap L) " (uparrow t), InclPoset (Ids L) & inf ((SupMap L) " (uparrow t)) in (SupMap L) " (uparrow t) ) by A3, FUNCT_1:def 7, YELLOW_0:17;

hence d . t is_minimum_of (SupMap L) " (uparrow t) by A2, WAYBEL_1:def 6; :: thesis: verum

end;set I = inf ((SupMap L) " (uparrow t));

reconsider I9 = inf ((SupMap L) " (uparrow t)) as Ideal of L by YELLOW_2:41;

A2: d . t = inf ((SupMap L) " (uparrow {t})) by A1

.= inf ((SupMap L) " (uparrow t)) by WAYBEL_0:def 18 ;

inf ((SupMap L) " (uparrow t)) in the carrier of (InclPoset (Ids L)) ;

then inf ((SupMap L) " (uparrow t)) in Ids L by YELLOW_1:1;

then A3: inf ((SupMap L) " (uparrow t)) in dom (SupMap L) by YELLOW_2:49;

consider J being Ideal of L such that

A4: t <= sup J and

A5: for K being Ideal of L st t <= sup K holds

J c= K by Lm3;

reconsider J9 = J as Element of (InclPoset (Ids L)) by YELLOW_2:41;

A6: for K being Element of (InclPoset (Ids L)) st (SupMap L) " (uparrow t) is_>=_than K holds

K <= J9

proof

(SupMap L) " (uparrow t) is_>=_than J9
J9 in the carrier of (InclPoset (Ids L))
;

then J9 in Ids L by YELLOW_1:1;

then A7: J in dom (SupMap L) by YELLOW_2:49;

let K be Element of (InclPoset (Ids L)); :: thesis: ( (SupMap L) " (uparrow t) is_>=_than K implies K <= J9 )

assume A8: (SupMap L) " (uparrow t) is_>=_than K ; :: thesis: K <= J9

t <= (SupMap L) . J9 by A4, YELLOW_2:def 3;

then (SupMap L) . J in uparrow t by WAYBEL_0:18;

then J in (SupMap L) " (uparrow t) by A7, FUNCT_1:def 7;

hence K <= J9 by A8; :: thesis: verum

end;then J9 in Ids L by YELLOW_1:1;

then A7: J in dom (SupMap L) by YELLOW_2:49;

let K be Element of (InclPoset (Ids L)); :: thesis: ( (SupMap L) " (uparrow t) is_>=_than K implies K <= J9 )

assume A8: (SupMap L) " (uparrow t) is_>=_than K ; :: thesis: K <= J9

t <= (SupMap L) . J9 by A4, YELLOW_2:def 3;

then (SupMap L) . J in uparrow t by WAYBEL_0:18;

then J in (SupMap L) " (uparrow t) by A7, FUNCT_1:def 7;

hence K <= J9 by A8; :: thesis: verum

proof

then
t <= sup I9
by A4, A6, YELLOW_0:31;
let K be Element of (InclPoset (Ids L)); :: according to LATTICE3:def 8 :: thesis: ( not K in (SupMap L) " (uparrow t) or J9 <= K )

reconsider K9 = K as Ideal of L by YELLOW_2:41;

assume K in (SupMap L) " (uparrow t) ; :: thesis: J9 <= K

then (SupMap L) . K in uparrow t by FUNCT_1:def 7;

then t <= (SupMap L) . K by WAYBEL_0:18;

then t <= sup K9 by YELLOW_2:def 3;

then J9 c= K9 by A5;

hence J9 <= K by YELLOW_1:3; :: thesis: verum

end;reconsider K9 = K as Ideal of L by YELLOW_2:41;

assume K in (SupMap L) " (uparrow t) ; :: thesis: J9 <= K

then (SupMap L) . K in uparrow t by FUNCT_1:def 7;

then t <= (SupMap L) . K by WAYBEL_0:18;

then t <= sup K9 by YELLOW_2:def 3;

then J9 c= K9 by A5;

hence J9 <= K by YELLOW_1:3; :: thesis: verum

then t <= (SupMap L) . (inf ((SupMap L) " (uparrow t))) by YELLOW_2:def 3;

then (SupMap L) . (inf ((SupMap L) " (uparrow t))) in uparrow t by WAYBEL_0:18;

then ( ex_inf_of (SupMap L) " (uparrow t), InclPoset (Ids L) & inf ((SupMap L) " (uparrow t)) in (SupMap L) " (uparrow t) ) by A3, FUNCT_1:def 7, YELLOW_0:17;

hence d . t is_minimum_of (SupMap L) " (uparrow t) by A2, WAYBEL_1:def 6; :: thesis: verum

hence SupMap L is upper_adjoint by WAYBEL_1:def 11; :: thesis: verum