let S1, S2, T1, T2 be complete LATTICE; for f being directed-sups-preserving Function of S1,S2
for g being directed-sups-preserving Function of T1,T2 holds UPS (f,g) is directed-sups-preserving
let f be directed-sups-preserving Function of S1,S2; for g being directed-sups-preserving Function of T1,T2 holds UPS (f,g) is directed-sups-preserving
let g be directed-sups-preserving Function of T1,T2; UPS (f,g) is directed-sups-preserving
let A be Subset of (UPS (S2,T1)); WAYBEL_0:def 37 ( A is empty or not A is directed or UPS (f,g) preserves_sup_of A )
assume
( not A is empty & A is directed )
; UPS (f,g) preserves_sup_of A
then reconsider H = A as non empty directed Subset of (UPS (S2,T1)) ;
assume
ex_sup_of A, UPS (S2,T1)
; WAYBEL_0:def 31 ( ex_sup_of (UPS (f,g)) .: A, UPS (S1,T2) & "\/" (((UPS (f,g)) .: A),(UPS (S1,T2))) = (UPS (f,g)) . ("\/" (A,(UPS (S2,T1)))) )
thus
ex_sup_of (UPS (f,g)) .: A, UPS (S1,T2)
by YELLOW_0:17; "\/" (((UPS (f,g)) .: A),(UPS (S1,T2))) = (UPS (f,g)) . ("\/" (A,(UPS (S2,T1))))
UPS (S2,T1) is full SubRelStr of T1 |^ the carrier of S2
by Def4;
then reconsider B = H as non empty directed Subset of (T1 |^ the carrier of S2) by YELLOW_2:7;
A1:
UPS (S1,T2) is full SubRelStr of T2 |^ the carrier of S1
by Def4;
then reconsider fgsA = (UPS (f,g)) . (sup H) as Element of (T2 |^ the carrier of S1) by YELLOW_0:58;
the carrier of (UPS (S1,T2)) c= the carrier of (T2 |^ the carrier of S1)
by A1, YELLOW_0:def 13;
then reconsider fgA = (UPS (f,g)) .: H as non empty Subset of (T2 |^ the carrier of S1) by XBOOLE_1:1;
A2:
T2 |^ the carrier of S1 = product ( the carrier of S1 --> T2)
by YELLOW_1:def 5;
then A3:
dom (sup fgA) = the carrier of S1
by WAYBEL_3:27;
A4:
T1 |^ the carrier of S2 = product ( the carrier of S2 --> T1)
by YELLOW_1:def 5;
A5:
now for s being object st s in the carrier of S1 holds
(sup fgA) . s = fgsA . sreconsider BB =
B as
directed Subset of
(product ( the carrier of S2 --> T1)) by A4;
let s be
object ;
( s in the carrier of S1 implies (sup fgA) . s = fgsA . s )A6:
dom f = the
carrier of
S1
by FUNCT_2:def 1;
assume
s in the
carrier of
S1
;
(sup fgA) . s = fgsA . sthen reconsider x =
s as
Element of
S1 ;
reconsider sH =
sup H as
directed-sups-preserving Function of
S2,
T1 by Def4;
A7:
( the carrier of S2 --> T1) . (f . x) = T1
;
dom sH = the
carrier of
S2
by FUNCT_2:def 1;
then
f . x in dom sH
;
then A8:
x in dom (sH * f)
by A6, FUNCT_1:11;
A9:
pi (
fgA,
x)
= g .: (pi (A,(f . x)))
proof
thus
pi (
fgA,
x)
c= g .: (pi (A,(f . x)))
XBOOLE_0:def 10 g .: (pi (A,(f . x))) c= pi (fgA,x)proof
let a be
object ;
TARSKI:def 3 ( not a in pi (fgA,x) or a in g .: (pi (A,(f . x))) )
A10:
dom g = the
carrier of
T1
by FUNCT_2:def 1;
assume
a in pi (
fgA,
x)
;
a in g .: (pi (A,(f . x)))
then consider F being
Function such that A11:
F in fgA
and A12:
a = F . x
by CARD_3:def 6;
consider G being
object such that A13:
G in dom (UPS (f,g))
and A14:
G in H
and A15:
F = (UPS (f,g)) . G
by A11, FUNCT_1:def 6;
reconsider G =
G as
directed-sups-preserving Function of
S2,
T1 by A13, Def4;
A16:
G . (f . x) in pi (
A,
(f . x))
by A14, CARD_3:def 6;
A17:
dom f = the
carrier of
S1
by FUNCT_2:def 1;
dom G = the
carrier of
S2
by FUNCT_2:def 1;
then
f . x in dom G
;
then A18:
x in dom (G * f)
by A17, FUNCT_1:11;
a =
((g * G) * f) . x
by A12, A15, Def5
.=
(g * (G * f)) . x
by RELAT_1:36
.=
g . ((G * f) . x)
by A18, FUNCT_1:13
.=
g . (G . (f . x))
by A17, FUNCT_1:13
;
hence
a in g .: (pi (A,(f . x)))
by A10, A16, FUNCT_1:def 6;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in g .: (pi (A,(f . x))) or a in pi (fgA,x) )
A19:
dom (UPS (f,g)) = the
carrier of
(UPS (S2,T1))
by FUNCT_2:def 1;
assume
a in g .: (pi (A,(f . x)))
;
a in pi (fgA,x)
then consider F being
object such that
F in dom g
and A20:
F in pi (
A,
(f . x))
and A21:
a = g . F
by FUNCT_1:def 6;
consider G being
Function such that A22:
G in A
and A23:
F = G . (f . x)
by A20, CARD_3:def 6;
reconsider G =
G as
directed-sups-preserving Function of
S2,
T1 by A22, Def4;
(g * G) * f = (UPS (f,g)) . G
by Def5;
then A24:
(g * G) * f in fgA
by A22, A19, FUNCT_1:def 6;
A25:
dom f = the
carrier of
S1
by FUNCT_2:def 1;
dom G = the
carrier of
S2
by FUNCT_2:def 1;
then
f . x in dom G
;
then A26:
x in dom (G * f)
by A25, FUNCT_1:11;
a =
g . ((G * f) . x)
by A21, A23, A25, FUNCT_1:13
.=
(g * (G * f)) . x
by A26, FUNCT_1:13
.=
((g * G) * f) . x
by RELAT_1:36
;
hence
a in pi (
fgA,
x)
by A24, CARD_3:def 6;
verum
end; A27:
ex_sup_of pi (
B,
(f . x)),
T1
by YELLOW_0:17;
A28:
pi (
BB,
(f . x)) is
directed
by YELLOW16:35;
A29:
g preserves_sup_of pi (
B,
(f . x))
by A28, WAYBEL_0:def 37;
( the carrier of S1 --> T2) . x = T2
;
hence (sup fgA) . s =
sup (pi (fgA,x))
by A2, YELLOW16:33, YELLOW_0:17
.=
g . (sup (pi (B,(f . x))))
by A9, A29, A27
.=
g . ((sup B) . (f . x))
by A4, A7, YELLOW16:33, YELLOW_0:17
.=
g . (sH . (f . x))
by Th27
.=
g . ((sH * f) . x)
by A6, FUNCT_1:13
.=
(g * (sH * f)) . x
by A8, FUNCT_1:13
.=
((g * sH) * f) . s
by RELAT_1:36
.=
fgsA . s
by Def5
;
verum end;
A30:
dom fgsA = the carrier of S1
by A2, WAYBEL_3:27;
thus sup ((UPS (f,g)) .: A) =
sup fgA
by Th27
.=
(UPS (f,g)) . (sup A)
by A3, A30, A5
; verum