let L be complete continuous LATTICE; :: thesis: for p being projection Function of L,L st p is directed-sups-preserving holds

Image p is continuous LATTICE

let p be projection Function of L,L; :: thesis: ( p is directed-sups-preserving implies Image p is continuous LATTICE )

assume A1: p is directed-sups-preserving ; :: thesis: Image p is continuous LATTICE

reconsider Lk = { k where k is Element of L : p . k <= k } as non empty Subset of L by WAYBEL_1:43;

A2: subrelstr Lk is infs-inheriting by WAYBEL_1:50;

reconsider pk = p | Lk as Function of (subrelstr Lk),(subrelstr Lk) by WAYBEL_1:46;

A3: pk is kernel by WAYBEL_1:48;

subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:52;

then A11: subrelstr Lk is continuous LATTICE by A2, WAYBEL_5:28;

A12: the carrier of (subrelstr (rng p)) = rng p by YELLOW_0:def 15

.= rng pk by WAYBEL_1:44

.= the carrier of (subrelstr (rng pk)) by YELLOW_0:def 15 ;

subrelstr (rng pk) is full SubRelStr of L by Th1;

then A13: Image p = Image pk by A12, YELLOW_0:57;

subrelstr Lk is complete by A2, YELLOW_2:30;

hence Image p is continuous LATTICE by A11, A3, A13, A10, Th14; :: thesis: verum

Image p is continuous LATTICE

let p be projection Function of L,L; :: thesis: ( p is directed-sups-preserving implies Image p is continuous LATTICE )

assume A1: p is directed-sups-preserving ; :: thesis: Image p is continuous LATTICE

reconsider Lk = { k where k is Element of L : p . k <= k } as non empty Subset of L by WAYBEL_1:43;

A2: subrelstr Lk is infs-inheriting by WAYBEL_1:50;

reconsider pk = p | Lk as Function of (subrelstr Lk),(subrelstr Lk) by WAYBEL_1:46;

A3: pk is kernel by WAYBEL_1:48;

now :: thesis: for X being Subset of (subrelstr Lk) st not X is empty & X is directed holds

pk preserves_sup_of X

then A10:
pk is directed-sups-preserving
by WAYBEL_0:def 37;pk preserves_sup_of X

let X be Subset of (subrelstr Lk); :: thesis: ( not X is empty & X is directed implies pk preserves_sup_of X )

reconsider X9 = X as Subset of L by WAYBEL13:3;

assume A4: ( not X is empty & X is directed ) ; :: thesis: pk preserves_sup_of X

then reconsider X9 = X9 as non empty directed Subset of L by YELLOW_2:7;

A5: p preserves_sup_of X9 by A1, WAYBEL_0:def 37;

end;reconsider X9 = X as Subset of L by WAYBEL13:3;

assume A4: ( not X is empty & X is directed ) ; :: thesis: pk preserves_sup_of X

then reconsider X9 = X9 as non empty directed Subset of L by YELLOW_2:7;

A5: p preserves_sup_of X9 by A1, WAYBEL_0:def 37;

now :: thesis: ( ex_sup_of X, subrelstr Lk implies ( ex_sup_of pk .: X, subrelstr Lk & sup (pk .: X) = pk . (sup X) ) )

hence
pk preserves_sup_of X
by WAYBEL_0:def 31; :: thesis: verum
X c= the carrier of (subrelstr Lk)
;

then X c= Lk by YELLOW_0:def 15;

then A6: pk .: X = p .: X by RELAT_1:129;

assume ex_sup_of X, subrelstr Lk ; :: thesis: ( ex_sup_of pk .: X, subrelstr Lk & sup (pk .: X) = pk . (sup X) )

subrelstr Lk is infs-inheriting by WAYBEL_1:50;

then subrelstr Lk is complete LATTICE by YELLOW_2:30;

hence ex_sup_of pk .: X, subrelstr Lk by YELLOW_0:17; :: thesis: sup (pk .: X) = pk . (sup X)

A7: ex_sup_of X,L by YELLOW_0:17;

A8: subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:52;

then A9: ( dom pk = the carrier of (subrelstr Lk) & sup X9 = sup X ) by A4, A7, FUNCT_2:def 1, WAYBEL_0:7;

( ex_sup_of p .: X,L & pk .: X is directed Subset of (subrelstr Lk) ) by A3, A4, YELLOW_0:17, YELLOW_2:15;

hence sup (pk .: X) = sup (p .: X) by A4, A8, A6, WAYBEL_0:7

.= p . (sup X9) by A5, A7, WAYBEL_0:def 31

.= pk . (sup X) by A9, FUNCT_1:47 ;

:: thesis: verum

end;then X c= Lk by YELLOW_0:def 15;

then A6: pk .: X = p .: X by RELAT_1:129;

assume ex_sup_of X, subrelstr Lk ; :: thesis: ( ex_sup_of pk .: X, subrelstr Lk & sup (pk .: X) = pk . (sup X) )

subrelstr Lk is infs-inheriting by WAYBEL_1:50;

then subrelstr Lk is complete LATTICE by YELLOW_2:30;

hence ex_sup_of pk .: X, subrelstr Lk by YELLOW_0:17; :: thesis: sup (pk .: X) = pk . (sup X)

A7: ex_sup_of X,L by YELLOW_0:17;

A8: subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:52;

then A9: ( dom pk = the carrier of (subrelstr Lk) & sup X9 = sup X ) by A4, A7, FUNCT_2:def 1, WAYBEL_0:7;

( ex_sup_of p .: X,L & pk .: X is directed Subset of (subrelstr Lk) ) by A3, A4, YELLOW_0:17, YELLOW_2:15;

hence sup (pk .: X) = sup (p .: X) by A4, A8, A6, WAYBEL_0:7

.= p . (sup X9) by A5, A7, WAYBEL_0:def 31

.= pk . (sup X) by A9, FUNCT_1:47 ;

:: thesis: verum

subrelstr Lk is directed-sups-inheriting by A1, WAYBEL_1:52;

then A11: subrelstr Lk is continuous LATTICE by A2, WAYBEL_5:28;

A12: the carrier of (subrelstr (rng p)) = rng p by YELLOW_0:def 15

.= rng pk by WAYBEL_1:44

.= the carrier of (subrelstr (rng pk)) by YELLOW_0:def 15 ;

subrelstr (rng pk) is full SubRelStr of L by Th1;

then A13: Image p = Image pk by A12, YELLOW_0:57;

subrelstr Lk is complete by A2, YELLOW_2:30;

hence Image p is continuous LATTICE by A11, A3, A13, A10, Th14; :: thesis: verum