let L be complete LATTICE; ( S7[L] implies S8[L] )
assume A1:
S7[L]
; S8[L]
let SL be Scott TopAugmentation of L; for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let S be complete LATTICE; for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SS be Scott TopAugmentation of S; sigma [:S,L:] = the topology of [:SS,SL:]
A2:
RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_9:def 4;
UPS (L,(BoolePoset {0})) is non empty full SubRelStr of (BoolePoset {0}) |^ the carrier of L
by WAYBEL27:def 4;
then A3:
(UPS (L,(BoolePoset {0}))) |^ the carrier of S is non empty full SubRelStr of ((BoolePoset {0}) |^ the carrier of L) |^ the carrier of S
by YELLOW16:39;
UPS (S,(UPS (L,(BoolePoset {0})))) is non empty full SubRelStr of (UPS (L,(BoolePoset {0}))) |^ the carrier of S
by WAYBEL27:def 4;
then A4:
UPS (S,(UPS (L,(BoolePoset {0})))) is non empty full SubRelStr of ((BoolePoset {0}) |^ the carrier of L) |^ the carrier of S
by A3, WAYBEL15:1;
consider f5 being Function of (UPS (L,(BoolePoset {0}))),(InclPoset (sigma L)) such that
A5:
f5 is isomorphic
and
A6:
for f being directed-sups-preserving Function of L,(BoolePoset {0}) holds f5 . f = f " {1}
by WAYBEL27:33;
set f6 = UPS ((id S),f5);
consider f3 being Function of (UPS (S,(UPS (L,(BoolePoset {0}))))),(UPS ([:S,L:],(BoolePoset {0}))) such that
A7:
( f3 is uncurrying & f3 is isomorphic )
by WAYBEL27:47;
set f4 = f3 " ;
set T = Sigma (InclPoset the topology of SL);
consider f1 being Function of (UPS ([:S,L:],(BoolePoset {0}))),(InclPoset (sigma [:S,L:])) such that
A8:
f1 is isomorphic
and
A9:
for f being directed-sups-preserving Function of [:S,L:],(BoolePoset {0}) holds f1 . f = f " {1}
by WAYBEL27:33;
A10:
f3 " is isomorphic
by A7, YELLOW14:10;
set f2 = f1 " ;
set G = ((UPS ((id S),f5)) * (f3 ")) * (f1 ");
A11:
the topology of SL = sigma L
by YELLOW_9:51;
then A12:
RelStr(# the carrier of (Sigma (InclPoset the topology of SL)), the InternalRel of (Sigma (InclPoset the topology of SL)) #) = RelStr(# the carrier of (InclPoset (sigma L)), the InternalRel of (InclPoset (sigma L)) #)
by YELLOW_9:def 4;
A13:
the carrier of (UPS (S,(InclPoset (sigma L)))) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))
proof
thus
the
carrier of
(UPS (S,(InclPoset (sigma L)))) c= the
carrier of
(ContMaps (SS,(Sigma (InclPoset the topology of SL))))
XBOOLE_0:def 10 the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) c= the carrier of (UPS (S,(InclPoset (sigma L))))proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (UPS (S,(InclPoset (sigma L)))) or x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) )
assume A14:
x in the
carrier of
(UPS (S,(InclPoset (sigma L))))
;
x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))
then reconsider x1 =
x as
Function of
SS,
(Sigma (InclPoset the topology of SL)) by A2, A12, WAYBEL27:def 4;
x is
directed-sups-preserving Function of
S,
(InclPoset (sigma L))
by A14, WAYBEL27:def 4;
then
x1 is
directed-sups-preserving
by A2, A12, WAYBEL21:6;
then
x1 is
continuous
by WAYBEL17:22;
hence
x in the
carrier of
(ContMaps (SS,(Sigma (InclPoset the topology of SL))))
by WAYBEL24:def 3;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) or x in the carrier of (UPS (S,(InclPoset (sigma L)))) )
assume
x in the
carrier of
(ContMaps (SS,(Sigma (InclPoset the topology of SL))))
;
x in the carrier of (UPS (S,(InclPoset (sigma L))))
then consider x1 being
Function of
SS,
(Sigma (InclPoset the topology of SL)) such that A15:
x1 = x
and A16:
x1 is
continuous
by WAYBEL24:def 3;
reconsider x2 =
x1 as
Function of
S,
(InclPoset (sigma L)) by A2, A12;
x1 is
directed-sups-preserving
by A16, WAYBEL17:22;
then
x2 is
directed-sups-preserving
by A2, A12, WAYBEL21:6;
hence
x in the
carrier of
(UPS (S,(InclPoset (sigma L))))
by A15, WAYBEL27:def 4;
verum
end;
then reconsider G = ((UPS ((id S),f5)) * (f3 ")) * (f1 ") as Function of (InclPoset (sigma [:S,L:])),(ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ;
set F = Theta (SS,SL);
A17:
RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #)
by YELLOW_9:def 4;
( (BoolePoset {0}) |^ the carrier of [:S,L:] = (BoolePoset {0}) |^ [: the carrier of S, the carrier of L:] & UPS ([:S,L:],(BoolePoset {0})) is non empty full SubRelStr of (BoolePoset {0}) |^ the carrier of [:S,L:] )
by WAYBEL27:def 4, YELLOW_3:def 2;
then A18:
f3 " is currying
by A7, A4, Th2;
A19:
for V being Element of (InclPoset (sigma [:S,L:]))
for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V }
proof
let V be
Element of
(InclPoset (sigma [:S,L:]));
for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V } let s be
Element of
S;
(G . V) . s = { y where y is Element of L : [s,y] in V }
reconsider fff =
(f3 ") . ((f1 ") . V) as
directed-sups-preserving Function of
S,
(UPS (L,(BoolePoset {0}))) by WAYBEL27:def 4;
reconsider f2V =
(f1 ") . V as
directed-sups-preserving Function of
[:S,L:],
(BoolePoset {0}) by WAYBEL27:def 4;
A20:
(
f5 is
sups-preserving &
(f5 * fff) * (id the carrier of S) = f5 * fff )
by A5, FUNCT_2:17, WAYBEL13:20;
A21:
((f3 ") . ((f1 ") . V)) . s is
directed-sups-preserving Function of
L,
(BoolePoset {0})
by WAYBEL27:def 4;
then A22:
dom (((f3 ") . ((f1 ") . V)) . s) = the
carrier of
L
by FUNCT_2:def 1;
G . V =
((UPS ((id S),f5)) * (f3 ")) . ((f1 ") . V)
by FUNCT_2:15
.=
(UPS ((id S),f5)) . ((f3 ") . ((f1 ") . V))
by FUNCT_2:15
.=
f5 * fff
by A20, WAYBEL27:def 5
;
then A23:
(G . V) . s =
f5 . (fff . s)
by FUNCT_2:15
.=
(((f3 ") . ((f1 ") . V)) . s) " {1}
by A6, A21
;
A24:
rng f1 = [#] (InclPoset (sigma [:S,L:]))
by A8, FUNCT_2:def 3;
dom (f3 ") = the
carrier of
(UPS ([:S,L:],(BoolePoset {0})))
by FUNCT_2:def 1;
then A25:
(f3 ") . ((f1 ") . V) = curry ((f1 ") . V)
by A18;
rng f1 = the
carrier of
(InclPoset (sigma [:S,L:]))
by A8, FUNCT_2:def 3;
then A26:
V =
(id (rng f1)) . V
.=
(f1 * (f1 ")) . V
by A8, A24, TOPS_2:52
.=
f1 . ((f1 ") . V)
by FUNCT_2:15
.=
f2V " {1}
by A9
;
thus
(G . V) . s c= { y where y is Element of L : [s,y] in V }
XBOOLE_0:def 10 { y where y is Element of L : [s,y] in V } c= (G . V) . sproof
let x be
object ;
TARSKI:def 3 ( not x in (G . V) . s or x in { y where y is Element of L : [s,y] in V } )
assume A27:
x in (G . V) . s
;
x in { y where y is Element of L : [s,y] in V }
then
x in dom (((f3 ") . ((f1 ") . V)) . s)
by A23, FUNCT_1:def 7;
then reconsider y =
x as
Element of
L by A21, FUNCT_2:def 1;
(((f3 ") . ((f1 ") . V)) . s) . x in {1}
by A23, A27, FUNCT_1:def 7;
then A28:
(((f3 ") . ((f1 ") . V)) . s) . y = 1
by TARSKI:def 1;
A29:
dom f2V = the
carrier of
[:S,L:]
by FUNCT_2:def 1;
then
[s,y] in dom ((f1 ") . V)
;
then
((f1 ") . V) . (
s,
y)
= 1
by A25, A28, FUNCT_5:20;
then
((f1 ") . V) . (
s,
y)
in {1}
by TARSKI:def 1;
then
[s,y] in ((f1 ") . V) " {1}
by A29, FUNCT_1:def 7;
hence
x in { y where y is Element of L : [s,y] in V }
by A26;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in { y where y is Element of L : [s,y] in V } or x in (G . V) . s )
assume
x in { y where y is Element of L : [s,y] in V }
;
x in (G . V) . s
then consider y being
Element of
L such that A30:
y = x
and A31:
[s,y] in V
;
dom f2V = the
carrier of
[:S,L:]
by FUNCT_2:def 1;
then A32:
[s,y] in dom ((f1 ") . V)
;
reconsider cs =
(curry ((f1 ") . V)) . s as
Function ;
((f1 ") . V) . (
s,
y)
in {1}
by A26, A31, FUNCT_1:def 7;
then
((f1 ") . V) . (
s,
y)
= 1
by TARSKI:def 1;
then
cs . y = 1
by A32, FUNCT_5:20;
then
(((f3 ") . ((f1 ") . V)) . s) . y in {1}
by A25, TARSKI:def 1;
hence
x in (G . V) . s
by A23, A30, A22, FUNCT_1:def 7;
verum
end;
S6[SL]
by A1, A11, Lm8;
then
S4[SL]
by Lm6;
then A33:
Theta (SS,SL) is isomorphic
by Lm3;
A34:
the carrier of (InclPoset (sigma [:S,L:])) c= the carrier of (InclPoset the topology of [:SS,SL:])
proof
let V be
object ;
TARSKI:def 3 ( not V in the carrier of (InclPoset (sigma [:S,L:])) or V in the carrier of (InclPoset the topology of [:SS,SL:]) )
assume
V in the
carrier of
(InclPoset (sigma [:S,L:]))
;
V in the carrier of (InclPoset the topology of [:SS,SL:])
then reconsider V1 =
V as
Element of
(InclPoset (sigma [:S,L:])) ;
rng (Theta (SS,SL)) = the
carrier of
(ContMaps (SS,(Sigma (InclPoset the topology of SL))))
by A33, FUNCT_2:def 3;
then consider W being
object such that A35:
W in dom (Theta (SS,SL))
and A36:
(Theta (SS,SL)) . W = G . V1
by FUNCT_1:def 3;
reconsider W2 =
W as
Element of
(InclPoset the topology of [:SS,SL:]) by A35;
dom (Theta (SS,SL)) = the
carrier of
(InclPoset the topology of [:SS,SL:])
by FUNCT_2:def 1;
then
W in the
topology of
[:SS,SL:]
by A35, YELLOW_1:1;
then reconsider W1 =
W2 as
open Subset of
[:SS,SL:] by PRE_TOPC:def 2;
A37:
V1 c= W1
proof
let v be
object ;
TARSKI:def 3 ( not v in V1 or v in W1 )
assume A38:
v in V1
;
v in W1
V1 in the
carrier of
(InclPoset (sigma [:S,L:]))
;
then
V in sigma [:S,L:]
by YELLOW_1:1;
then
V1 c= the
carrier of
[:S,L:]
;
then
V1 c= [: the carrier of S, the carrier of L:]
by YELLOW_3:def 2;
then consider v1,
v2 being
object such that A39:
v1 in the
carrier of
S
and A40:
v2 in the
carrier of
L
and A41:
v = [v1,v2]
by A38, ZFMISC_1:84;
reconsider v2 =
v2 as
Element of
L by A40;
reconsider v1 =
v1 as
Element of
S by A39;
v2 in { y where y is Element of L : [v1,y] in V1 }
by A38, A41;
then
v2 in (G . V1) . v1
by A19;
then
v2 in ((W1, the carrier of S) *graph) . v1
by A2, A36, Def3;
then
v2 in Im (
W1,
v1)
by WAYBEL26:def 5;
then
ex
v19 being
object st
(
[v19,v2] in W1 &
v19 in {v1} )
by RELAT_1:def 13;
hence
v in W1
by A41, TARSKI:def 1;
verum
end;
W2 c= V1
proof
let w be
object ;
TARSKI:def 3 ( not w in W2 or w in V1 )
assume A42:
w in W2
;
w in V1
W1 c= the
carrier of
[:SS,SL:]
;
then
W1 c= [: the carrier of SS, the carrier of SL:]
by BORSUK_1:def 2;
then consider w1,
w2 being
object such that A43:
w1 in the
carrier of
S
and A44:
w2 in the
carrier of
L
and A45:
w = [w1,w2]
by A2, A17, A42, ZFMISC_1:84;
reconsider w2 =
w2 as
Element of
L by A44;
reconsider w1 =
w1 as
Element of
S by A43;
w1 in {w1}
by TARSKI:def 1;
then
w2 in Im (
W1,
w1)
by A42, A45, RELAT_1:def 13;
then
w2 in ((W1, the carrier of S) *graph) . w1
by WAYBEL26:def 5;
then
w2 in ((Theta (SS,SL)) . W2) . w1
by A2, Def3;
then
w2 in { y where y is Element of L : [w1,y] in V1 }
by A19, A36;
then
ex
w29 being
Element of
L st
(
w29 = w2 &
[w1,w29] in V1 )
;
hence
w in V1
by A45;
verum
end;
then
W2 = V
by A37, XBOOLE_0:def 10;
hence
V in the
carrier of
(InclPoset the topology of [:SS,SL:])
;
verum
end;
InclPoset (sigma L) = InclPoset the topology of SL
by YELLOW_9:51;
then
UPS ((id S),f5) is isomorphic
by A5, WAYBEL27:35;
then A46:
(UPS ((id S),f5)) * (f3 ") is isomorphic
by A10, Th6;
A47:
f1 " is isomorphic
by A8, YELLOW14:10;
the carrier of (InclPoset the topology of [:SS,SL:]) c= the carrier of (InclPoset (sigma [:S,L:]))
proof
let W be
object ;
TARSKI:def 3 ( not W in the carrier of (InclPoset the topology of [:SS,SL:]) or W in the carrier of (InclPoset (sigma [:S,L:])) )
assume A48:
W in the
carrier of
(InclPoset the topology of [:SS,SL:])
;
W in the carrier of (InclPoset (sigma [:S,L:]))
then reconsider W2 =
W as
Element of
(InclPoset the topology of [:SS,SL:]) ;
W in the
topology of
[:SS,SL:]
by A48, YELLOW_1:1;
then reconsider W1 =
W2 as
open Subset of
[:SS,SL:] by PRE_TOPC:def 2;
G is
onto
by A47, A46, A13, Th6, YELLOW14:9;
then
rng G = the
carrier of
(ContMaps (SS,(Sigma (InclPoset the topology of SL))))
by FUNCT_2:def 3;
then consider V being
object such that A49:
V in dom G
and A50:
G . V = (Theta (SS,SL)) . W2
by FUNCT_1:def 3;
reconsider V =
V as
Element of
(InclPoset (sigma [:S,L:])) by A49;
A51:
V c= W2
proof
let v be
object ;
TARSKI:def 3 ( not v in V or v in W2 )
assume A52:
v in V
;
v in W2
V in the
carrier of
(InclPoset (sigma [:S,L:]))
;
then
V in sigma [:S,L:]
by YELLOW_1:1;
then
V c= the
carrier of
[:S,L:]
;
then
V c= [: the carrier of S, the carrier of L:]
by YELLOW_3:def 2;
then consider v1,
v2 being
object such that A53:
v1 in the
carrier of
S
and A54:
v2 in the
carrier of
L
and A55:
v = [v1,v2]
by A52, ZFMISC_1:84;
reconsider v2 =
v2 as
Element of
L by A54;
reconsider v1 =
v1 as
Element of
S by A53;
v2 in { y where y is Element of L : [v1,y] in V }
by A52, A55;
then
v2 in (G . V) . v1
by A19;
then
v2 in ((W1, the carrier of S) *graph) . v1
by A2, A50, Def3;
then
v2 in Im (
W1,
v1)
by WAYBEL26:def 5;
then
ex
v19 being
object st
(
[v19,v2] in W2 &
v19 in {v1} )
by RELAT_1:def 13;
hence
v in W2
by A55, TARSKI:def 1;
verum
end;
W2 c= V
proof
let w be
object ;
TARSKI:def 3 ( not w in W2 or w in V )
assume A56:
w in W2
;
w in V
W1 c= the
carrier of
[:SS,SL:]
;
then
W1 c= [: the carrier of SS, the carrier of SL:]
by BORSUK_1:def 2;
then consider w1,
w2 being
object such that A57:
w1 in the
carrier of
S
and A58:
w2 in the
carrier of
L
and A59:
w = [w1,w2]
by A2, A17, A56, ZFMISC_1:84;
reconsider w2 =
w2 as
Element of
L by A58;
reconsider w1 =
w1 as
Element of
S by A57;
w1 in {w1}
by TARSKI:def 1;
then
w2 in Im (
W1,
w1)
by A56, A59, RELAT_1:def 13;
then
w2 in ((W1, the carrier of S) *graph) . w1
by WAYBEL26:def 5;
then
w2 in ((Theta (SS,SL)) . W2) . w1
by A2, Def3;
then
w2 in { y where y is Element of L : [w1,y] in V }
by A19, A50;
then
ex
w29 being
Element of
L st
(
w29 = w2 &
[w1,w29] in V )
;
hence
w in V
by A59;
verum
end;
then
W = V
by A51, XBOOLE_0:def 10;
hence
W in the
carrier of
(InclPoset (sigma [:S,L:]))
;
verum
end;
then
the carrier of (InclPoset (sigma [:S,L:])) = the carrier of (InclPoset the topology of [:SS,SL:])
by A34;
hence sigma [:S,L:] =
the carrier of (InclPoset the topology of [:SS,SL:])
by YELLOW_1:1
.=
the topology of [:SS,SL:]
by YELLOW_1:1
;
verum