let S, T be complete LATTICE; :: thesis: for f being directed-sups-preserving projection Function of T,T holds Image (UPS (id S),f) = UPS S,(Image f)
let f be directed-sups-preserving projection Function of T,T; :: thesis: Image (UPS (id S),f) = UPS S,(Image f)
UPS S,T is full SubRelStr of T |^ the carrier of S
by Def4;
then reconsider IUPS = Image (UPS (id S),f) as full SubRelStr of T |^ the carrier of S by WAYBEL15:1;
reconsider If = Image f as complete LATTICE by YELLOW_2:37;
A1:
UPS S,If is full SubRelStr of (Image f) |^ the carrier of S
by Def4;
If |^ the carrier of S is full SubRelStr of T |^ the carrier of S
by YELLOW16:41;
then reconsider UPSIf = UPS S,If as full SubRelStr of T |^ the carrier of S by A1, WAYBEL15:1;
the carrier of UPSIf = the carrier of IUPS
proof
thus
the
carrier of
UPSIf c= the
carrier of
IUPS
:: according to XBOOLE_0:def 10 :: thesis: the carrier of IUPS c= the carrier of UPSIfproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the carrier of UPSIf or x in the carrier of IUPS )
assume
x in the
carrier of
UPSIf
;
:: thesis: x in the carrier of IUPS
then reconsider h =
x as
directed-sups-preserving Function of
S,
If by Def4;
A2:
the
carrier of
If c= the
carrier of
T
by YELLOW_0:def 13;
(
dom h = the
carrier of
S &
rng h c= the
carrier of
T )
by A2, FUNCT_2:def 1, XBOOLE_1:1;
then reconsider g =
h as
Function of
S,
T by RELSET_1:11;
A4:
g is
directed-sups-preserving
proof
let X be
Subset of
S;
:: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or g preserves_sup_of X )
assume A5:
( not
X is
empty &
X is
directed )
;
:: thesis: g preserves_sup_of X
thus
g preserves_sup_of X
:: thesis: verumproof
assume A6:
ex_sup_of X,
S
;
:: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: X,T & "\/" (g .: X),T = g . ("\/" X,S) )
reconsider hX =
h .: X as non
empty directed Subset of
If by A5, YELLOW_2:17;
h preserves_sup_of X
by A5, WAYBEL_0:def 37;
then A7:
(
ex_sup_of h .: X,
If &
sup hX = h . (sup X) )
by A6, WAYBEL_0:def 31;
thus A8:
ex_sup_of g .: X,
T
by YELLOW_0:17;
:: thesis: "\/" (g .: X),T = g . ("\/" X,S)
If is non
empty full directed-sups-inheriting SubRelStr of
T
by YELLOW_2:37;
hence
"\/" (g .: X),
T = g . ("\/" X,S)
by A7, A8, WAYBEL_0:7;
:: thesis: verum
end;
end;
then A9:
g in the
carrier of
(UPS S,T)
by Def4;
A10:
dom (UPS (id S),f) = the
carrier of
(UPS S,T)
by FUNCT_2:def 1;
(UPS (id S),f) . g =
(f * g) * (id S)
by A4, Def5
.=
h * (id S)
by Th10
.=
g
by FUNCT_2:23
;
then
x in rng (UPS (id S),f)
by A9, A10, FUNCT_1:def 5;
hence
x in the
carrier of
IUPS
by YELLOW_0:def 15;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the carrier of IUPS or x in the carrier of UPSIf )
assume
x in the
carrier of
IUPS
;
:: thesis: x in the carrier of UPSIf
then
x in rng (UPS (id S),f)
by YELLOW_0:def 15;
then consider a being
set such that A11:
(
a in dom (UPS (id S),f) &
x = (UPS (id S),f) . a )
by FUNCT_1:def 5;
reconsider a =
a as
directed-sups-preserving Function of
S,
T by A11, Def4;
A12:
x =
(f * a) * (id S)
by A11, Def5
.=
f * a
by FUNCT_2:23
;
then reconsider x0 =
x as
directed-sups-preserving Function of
S,
T by WAYBEL15:13;
A13:
(
dom x0 = the
carrier of
S &
rng x0 c= the
carrier of
T )
by FUNCT_2:def 1;
rng f = the
carrier of
(subrelstr (rng f))
by YELLOW_0:def 15;
then reconsider x1 =
x0 as
Function of
S,
If by A12, A13, FUNCT_2:4, RELAT_1:45;
x1 is
directed-sups-preserving
proof
let X be
Subset of
S;
:: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or x1 preserves_sup_of X )
assume A14:
( not
X is
empty &
X is
directed )
;
:: thesis: x1 preserves_sup_of X
thus
x1 preserves_sup_of X
:: thesis: verumproof
assume A15:
ex_sup_of X,
S
;
:: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of x1 .: X,If & "\/" (x1 .: X),If = x1 . ("\/" X,S) )
reconsider hX =
x0 .: X as non
empty directed Subset of
T by A14, YELLOW_2:17;
A16:
x0 preserves_sup_of X
by A14, WAYBEL_0:def 37;
then A17:
(
ex_sup_of x0 .: X,
T &
sup hX = x0 . (sup X) )
by A15, WAYBEL_0:def 31;
thus
ex_sup_of x1 .: X,
If
by YELLOW_0:17;
:: thesis: "\/" (x1 .: X),If = x1 . ("\/" X,S)
x1 is
monotone
by Th12;
then reconsider gX =
x1 .: X as non
empty directed Subset of
If by A14, YELLOW_2:17;
If is non
empty full directed-sups-inheriting SubRelStr of
T
by YELLOW_2:37;
then
sup gX = sup hX
by A17, WAYBEL_0:7;
hence
"\/" (x1 .: X),
If = x1 . ("\/" X,S)
by A15, A16, WAYBEL_0:def 31;
:: thesis: verum
end;
end;
hence
x in the
carrier of
UPSIf
by Def4;
:: thesis: verum
end;
hence
Image (UPS (id S),f) = UPS S,(Image f)
by YELLOW_0:58; :: thesis: verum