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:59;
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 reconsider BB =
B as
directed Subset of
(product (the carrier of S2 --> T1)) by A4;
let s be
set ;
( 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
by FUNCOP_1:13;
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:21;
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,xproof
let a be
set ;
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
set 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 12;
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:21;
a =
((g * G) * f) . x
by A12, A15, Def5
.=
(g * (G * f)) . x
by RELAT_1:55
.=
g . ((G * f) . x)
by A18, FUNCT_1:23
.=
g . (G . (f . x))
by A17, FUNCT_1:23
;
hence
a in g .: (pi A,(f . x))
by A10, A16, FUNCT_1:def 12;
verum
end;
let a be
set ;
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
set such that
F in dom g
and A20:
F in pi A,
(f . x)
and A21:
a = g . F
by FUNCT_1:def 12;
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 12;
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:21;
a =
g . ((G * f) . x)
by A21, A23, A25, FUNCT_1:23
.=
(g * (G * f)) . x
by A26, FUNCT_1:23
.=
((g * G) * f) . x
by RELAT_1:55
;
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:37;
(the carrier of S2 --> T1) . (f . x) = T1
by FUNCOP_1:13;
then A29:
g preserves_sup_of pi B,
(f . x)
by A28, WAYBEL_0:def 37;
(the carrier of S1 --> T2) . x = T2
by FUNCOP_1:13;
hence (sup fgA) . s =
sup (pi fgA,x)
by YELLOW_0:17, A2, YELLOW16:35
.=
g . (sup (pi B,(f . x)))
by A9, A29, A27, WAYBEL_0:def 31
.=
g . ((sup B) . (f . x))
by YELLOW_0:17, A4, A7, YELLOW16:35
.=
g . (sH . (f . x))
by Th27
.=
g . ((sH * f) . x)
by A6, FUNCT_1:23
.=
(g * (sH * f)) . x
by A8, FUNCT_1:23
.=
((g * sH) * f) . s
by RELAT_1:55
.=
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, FUNCT_1:9
; verum