let L be complete continuous LATTICE; :: thesis: for p being projection Function of L,L st p is infs-preserving holds
( Image p is continuous LATTICE & Image p is infs-inheriting )
let p be projection Function of L,L; :: thesis: ( p is infs-preserving implies ( Image p is continuous LATTICE & Image p is infs-inheriting ) )
assume A1:
p is infs-preserving
; :: thesis: ( Image p is continuous LATTICE & Image p is infs-inheriting )
reconsider Lc = { c where c is Element of L : c <= p . c } as non empty Subset of L by WAYBEL_1:46;
A2:
subrelstr Lc is sups-inheriting SubRelStr of L
by WAYBEL_1:52;
A3:
subrelstr Lc is infs-inheriting
by A1, WAYBEL_1:54;
then A4:
subrelstr Lc is continuous LATTICE
by A2, WAYBEL_5:28;
A5:
subrelstr Lc is complete
by A3, YELLOW_2:32;
reconsider pc = p | Lc as Function of (subrelstr Lc),(subrelstr Lc) by WAYBEL_1:48;
A6:
pc is closure
by WAYBEL_1:50;
A7:
subrelstr (rng pc) is full SubRelStr of L
by WAYBEL15:1;
the carrier of (subrelstr (rng p)) =
rng p
by YELLOW_0:def 15
.=
rng pc
by WAYBEL_1:47
.=
the carrier of (subrelstr (rng pc))
by YELLOW_0:def 15
;
then A8:
Image p = Image pc
by A7, YELLOW_0:58;
reconsider cpc = corestr pc as Function of (subrelstr Lc),(Image pc) ;
A9:
pc is infs-preserving
proof
let X be
Subset of
(subrelstr Lc);
:: according to WAYBEL_0:def 32 :: thesis: pc preserves_inf_of X
assume
ex_inf_of X,
subrelstr Lc
;
:: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of pc .: X, subrelstr Lc & "/\" (pc .: X),(subrelstr Lc) = pc . ("/\" X,(subrelstr Lc)) )
thus
ex_inf_of pc .: X,
subrelstr Lc
by A5, YELLOW_0:17;
:: thesis: "/\" (pc .: X),(subrelstr Lc) = pc . ("/\" X,(subrelstr Lc))
the
carrier of
(subrelstr Lc) = Lc
by YELLOW_0:def 15;
then reconsider X' =
X as
Subset of
L by XBOOLE_1:1;
A10:
dom pc = the
carrier of
(subrelstr Lc)
by FUNCT_2:def 1;
A11:
ex_inf_of X,
L
by YELLOW_0:17;
then
"/\" X',
L in the
carrier of
(subrelstr Lc)
by A3, YELLOW_0:def 18;
then A12:
inf X' = inf X
by A11, YELLOW_0:64;
A13:
ex_inf_of X',
L
by YELLOW_0:17;
A14:
p preserves_inf_of X'
by A1, WAYBEL_0:def 32;
A15:
ex_inf_of p .: X,
L
by YELLOW_0:17;
ex_inf_of pc .: X,
L
by YELLOW_0:17;
then A16:
"/\" (pc .: X),
L in the
carrier of
(subrelstr Lc)
by A3, YELLOW_0:def 18;
X c= the
carrier of
(subrelstr Lc)
;
then
X c= Lc
by YELLOW_0:def 15;
then
pc .: X = p .: X
by RELAT_1:162;
hence inf (pc .: X) =
inf (p .: X)
by A15, A16, YELLOW_0:64
.=
p . (inf X')
by A13, A14, WAYBEL_0:def 30
.=
pc . (inf X)
by A10, A12, FUNCT_1:70
;
:: thesis: verum
end;
A17:
cpc is sups-preserving
by A6, WAYBEL_1:58;
cpc is directed-sups-preserving
by A17;
hence
Image p is continuous LATTICE
by A4, A5, A8, A9, Th19, WAYBEL_5:33; :: thesis: Image p is infs-inheriting
thus
Image p is infs-inheriting
by A1, A3, WAYBEL_1:54; :: thesis: verum