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