let S, T be complete algebraic LATTICE; :: thesis: UPS (S,T) is algebraic
consider X being non empty set , p being closure Function of (BoolePoset X),(BoolePoset X) such that
A1: p is directed-sups-preserving and
A2: T, Image p are_isomorphic by WAYBEL13:35;
now :: thesis: for i being Element of (UPS (S,(BoolePoset X))) holds (id (UPS (S,(BoolePoset X)))) . i <= (UPS ((id S),p)) . i
let i be Element of (UPS (S,(BoolePoset X))); :: thesis: (id (UPS (S,(BoolePoset X)))) . i <= (UPS ((id S),p)) . i
reconsider f = i as directed-sups-preserving Function of S,(BoolePoset X) by Def4;
A3: (UPS ((id S),p)) . f = (p * f) * (id the carrier of S) by A1, Def5
.= p * f by FUNCT_2:17 ;
A4: now :: thesis: for s being Element of S holds i . s <= ((UPS ((id S),p)) . i) . s
let s be Element of S; :: thesis: i . s <= ((UPS ((id S),p)) . i) . s
A5: id (BoolePoset X) <= p by WAYBEL_1:def 14;
A6: (id (BoolePoset X)) . (i . s) = i . s ;
(p * f) . s = p . (f . s) by FUNCT_2:15;
hence i . s <= ((UPS ((id S),p)) . i) . s by A5, A6, A3, YELLOW_2:9; :: thesis: verum
end;
thus (id (UPS (S,(BoolePoset X)))) . i <= (UPS ((id S),p)) . i by A4, Th23; :: thesis: verum
end;
then A7: id (UPS (S,(BoolePoset X))) <= UPS ((id S),p) by YELLOW_2:9;
A8: (id S) * (id S) = id S by QUANTAL1:def 9;
p * p = p by QUANTAL1:def 9;
then (UPS ((id S),p)) * (UPS ((id S),p)) = UPS ((id S),p) by A8, A1, Th28;
then UPS ((id S),p) is idempotent directed-sups-preserving Function of (UPS (S,(BoolePoset X))),(UPS (S,(BoolePoset X))) by A1, Th30, QUANTAL1:def 9;
then UPS ((id S),p) is projection ;
then reconsider Sp = UPS ((id S),p) as directed-sups-preserving closure Function of (UPS (S,(BoolePoset X))),(UPS (S,(BoolePoset X))) by A7, A1, Th30, WAYBEL_1:def 14;
Image p is non empty complete Poset by A2, WAYBEL20:18;
then UPS (S,T), UPS (S,(Image p)) are_isomorphic by A2, Th36;
then A9: UPS (S,T), Image Sp are_isomorphic by A1, Th37;
BoolePoset X,(BoolePoset {0}) |^ X are_isomorphic by Th18;
then A10: UPS (S,(BoolePoset X)), UPS (S,((BoolePoset {0}) |^ X)) are_isomorphic by Th36;
set L = the Scott TopAugmentation of S;
A11: InclPoset (sigma S) = InclPoset the topology of the Scott TopAugmentation of S by YELLOW_9:51;
A12: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
then the Scott TopAugmentation of S is algebraic by WAYBEL13:26, WAYBEL13:32;
then ex B being Basis of the Scott TopAugmentation of S st B = { (uparrow x) where x is Element of the Scott TopAugmentation of S : x in the carrier of (CompactSublatt the Scott TopAugmentation of S) } by WAYBEL14:42;
then InclPoset (sigma the Scott TopAugmentation of S) is algebraic by WAYBEL14:43;
then A13: InclPoset (sigma S) is algebraic by A12, YELLOW_9:52;
UPS (S,(BoolePoset {0})), InclPoset (sigma S) are_isomorphic by Th34;
then ( UPS (S,(BoolePoset {0})) is algebraic & UPS (S,(BoolePoset {0})) is lower-bounded ) by A13, A11, WAYBEL13:32, WAYBEL_1:6;
then ( X -POS_prod (X --> (UPS (S,(BoolePoset {0})))) is lower-bounded & X -POS_prod (X --> (UPS (S,(BoolePoset {0})))) is algebraic ) ;
then A14: ( (UPS (S,(BoolePoset {0}))) |^ X is algebraic & (UPS (S,(BoolePoset {0}))) |^ X is lower-bounded ) by YELLOW_1:def 5;
UPS (S,((BoolePoset {0}) |^ X)),(UPS (S,(BoolePoset {0}))) |^ X are_isomorphic by Th42;
then UPS (S,(BoolePoset X)),(UPS (S,(BoolePoset {0}))) |^ X are_isomorphic by A10, WAYBEL_1:7;
then UPS (S,(BoolePoset X)) is lower-bounded algebraic LATTICE by A14, WAYBEL13:32, WAYBEL_1:6;
then A15: Image Sp is algebraic by WAYBEL_8:24;
Image Sp is complete LATTICE by YELLOW_2:30;
hence UPS (S,T) is algebraic by A9, A15, WAYBEL13:32, WAYBEL_1:6; :: thesis: verum