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