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