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, WAYBEL_0:def 37;
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, WAYBEL_0:def 31
.=
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, WAYBEL_0:def 31;
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, WAYBEL_0:def 37;
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, WAYBEL_0:def 31
.=
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, WAYBEL_0:def 31;
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, WAYBEL_0:def 37; verum