let R, S, T be LATTICE; for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
let f be Function of [:R,S:],T; for a being Element of R
for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
let a be Element of R; for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
let b be Element of S; ( f is directed-sups-preserving implies ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) )
assume A1:
f is directed-sups-preserving
; ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
A2:
for X being Subset of S st not X is empty & X is directed holds
Proj (f,a) preserves_sup_of X
proof
reconsider Y9 =
{a} as non
empty directed Subset of
R by WAYBEL_0:5;
let X be
Subset of
S;
( not X is empty & X is directed implies Proj (f,a) preserves_sup_of X )
assume
( not
X is
empty &
X is
directed )
;
Proj (f,a) preserves_sup_of X
then reconsider X9 =
X as non
empty directed Subset of
S ;
Proj (
f,
a)
preserves_sup_of X
proof
A3:
sup Y9 = a
by YELLOW_0:39;
A4:
f preserves_sup_of [:Y9,X9:]
by A1;
A5:
(Proj (f,a)) .: X = f .: [:Y9,X9:]
by Th15;
A6:
ex_sup_of Y9,
R
by YELLOW_0:38;
assume A7:
ex_sup_of X,
S
;
WAYBEL_0:def 31 ( ex_sup_of (Proj (f,a)) .: X,T & "\/" (((Proj (f,a)) .: X),T) = (Proj (f,a)) . ("\/" (X,S)) )
then A8:
ex_sup_of [:Y9,X9:],
[:R,S:]
by A6, YELLOW_3:39;
sup ((Proj (f,a)) .: X) =
sup (f .: [:Y9,X9:])
by Th15
.=
f . (sup [:Y9,X9:])
by A8, A4
.=
f . (
(sup Y9),
(sup X9))
by A7, A6, YELLOW_3:43
.=
(Proj (f,a)) . (sup X)
by A3, Th7
;
hence
(
ex_sup_of (Proj (f,a)) .: X,
T &
"\/" (
((Proj (f,a)) .: X),
T)
= (Proj (f,a)) . ("\/" (X,S)) )
by A8, A4, A5;
verum
end;
hence
Proj (
f,
a)
preserves_sup_of X
;
verum
end;
for X being Subset of R st not X is empty & X is directed holds
Proj (f,b) preserves_sup_of X
proof
reconsider Y9 =
{b} as non
empty directed Subset of
S by WAYBEL_0:5;
let X be
Subset of
R;
( not X is empty & X is directed implies Proj (f,b) preserves_sup_of X )
assume
( not
X is
empty &
X is
directed )
;
Proj (f,b) preserves_sup_of X
then reconsider X9 =
X as non
empty directed Subset of
R ;
Proj (
f,
b)
preserves_sup_of X
proof
A9:
sup Y9 = b
by YELLOW_0:39;
A10:
f preserves_sup_of [:X9,Y9:]
by A1;
A11:
(Proj (f,b)) .: X = f .: [:X9,Y9:]
by Th14;
A12:
ex_sup_of Y9,
S
by YELLOW_0:38;
assume A13:
ex_sup_of X,
R
;
WAYBEL_0:def 31 ( ex_sup_of (Proj (f,b)) .: X,T & "\/" (((Proj (f,b)) .: X),T) = (Proj (f,b)) . ("\/" (X,R)) )
then A14:
ex_sup_of [:X9,Y9:],
[:R,S:]
by A12, YELLOW_3:39;
sup ((Proj (f,b)) .: X) =
sup (f .: [:X9,Y9:])
by Th14
.=
f . (sup [:X9,Y9:])
by A14, A10
.=
f . (
(sup X9),
(sup Y9))
by A13, A12, YELLOW_3:43
.=
(Proj (f,b)) . (sup X)
by A9, Th8
;
hence
(
ex_sup_of (Proj (f,b)) .: X,
T &
"\/" (
((Proj (f,b)) .: X),
T)
= (Proj (f,b)) . ("\/" (X,R)) )
by A14, A10, A11;
verum
end;
hence
Proj (
f,
b)
preserves_sup_of X
;
verum
end;
hence
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
by A2; verum