let X be non empty TopSpace; :: thesis: for Y being T_0-TopSpace
for N being net of ContMaps X,(Omega Y) st ( for x being Point of X holds ex_sup_of commute N,x,(Omega Y) ) holds
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
let Y be T_0-TopSpace; :: thesis: for N being net of ContMaps X,(Omega Y) st ( for x being Point of X holds ex_sup_of commute N,x,(Omega Y) ) holds
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
let N be net of ContMaps X,(Omega Y); :: thesis: ( ( for x being Point of X holds ex_sup_of commute N,x,(Omega Y) ) implies ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X )
assume A1:
for x being Point of X holds ex_sup_of commute N,x,(Omega Y)
; :: thesis: ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
set n = the mapping of N;
set L = (Omega Y) |^ the carrier of X;
deffunc H1( Element of X) -> Element of the carrier of (Omega Y) = sup (commute N,$1,(Omega Y));
consider f being Function of the carrier of X,the carrier of (Omega Y) such that
A2:
for u being Element of X holds f . u = H1(u)
from FUNCT_2:sch 4();
reconsider a = f as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19;
ex a being Element of ((Omega Y) |^ the carrier of X) st
( rng the mapping of N is_<=_than a & ( for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds
a <= b ) )
proof
A3:
dom the
mapping of
N = the
carrier of
N
by FUNCT_2:def 1;
A4:
(Omega Y) |^ the
carrier of
X = product (the carrier of X --> (Omega Y))
by YELLOW_1:def 5;
take
a
;
:: thesis: ( rng the mapping of N is_<=_than a & ( for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds
a <= b ) )
thus
rng the
mapping of
N is_<=_than a
:: thesis: for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds
a <= bproof
let k be
Element of
((Omega Y) |^ the carrier of X);
:: according to LATTICE3:def 9 :: thesis: ( not k in rng the mapping of N or k <= a )
assume
k in rng the
mapping of
N
;
:: thesis: k <= a
then consider i being
set such that A5:
i in dom the
mapping of
N
and A6:
k = the
mapping of
N . i
by FUNCT_1:def 5;
reconsider i =
i as
Point of
N by A5;
reconsider k' =
k,
a' =
a as
Element of
(product (the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
for
u being
Element of
X holds
k' . u <= a' . u
proof
let u be
Element of
X;
:: thesis: k' . u <= a' . u
A7:
Omega Y = (the carrier of X --> (Omega Y)) . u
by FUNCOP_1:13;
ex_sup_of commute N,
u,
(Omega Y)
by A1;
then A8:
ex_sup_of rng the
mapping of
(commute N,u,(Omega Y)),
Omega Y
by WAYBEL_9:def 3;
A9:
dom the
mapping of
(commute N,u,(Omega Y)) = the
carrier of
N
by A3, Lm6;
A10:
a' . u =
sup (commute N,u,(Omega Y))
by A2
.=
Sup
by WAYBEL_2:def 1
.=
sup (rng the mapping of (commute N,u,(Omega Y)))
;
k' . u = the
mapping of
(commute N,u,(Omega Y)) . i
by A6, Th24;
then
k' . u in rng the
mapping of
(commute N,u,(Omega Y))
by A9, FUNCT_1:def 5;
hence
k' . u <= a' . u
by A7, A8, A10, YELLOW_4:1;
:: thesis: verum
end;
hence
k <= a
by A4, WAYBEL_3:28;
:: thesis: verum
end;
let b be
Element of
((Omega Y) |^ the carrier of X);
:: thesis: ( rng the mapping of N is_<=_than b implies a <= b )
assume A11:
for
k being
Element of
((Omega Y) |^ the carrier of X) st
k in rng the
mapping of
N holds
k <= b
;
:: according to LATTICE3:def 9 :: thesis: a <= b
reconsider a' =
a,
b' =
b as
Element of
(product (the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
for
u being
Element of
X holds
a' . u <= b' . u
proof
let u be
Element of
X;
:: thesis: a' . u <= b' . u
A12:
Omega Y = (the carrier of X --> (Omega Y)) . u
by FUNCOP_1:13;
A13:
a' . u =
sup (commute N,u,(Omega Y))
by A2
.=
Sup
by WAYBEL_2:def 1
.=
sup (rng the mapping of (commute N,u,(Omega Y)))
;
ex_sup_of commute N,
u,
(Omega Y)
by A1;
then A14:
ex_sup_of rng the
mapping of
(commute N,u,(Omega Y)),
Omega Y
by WAYBEL_9:def 3;
rng the
mapping of
(commute N,u,(Omega Y)) is_<=_than b . u
proof
let s be
Element of
(Omega Y);
:: according to LATTICE3:def 9 :: thesis: ( not s in rng the mapping of (commute N,u,(Omega Y)) or s <= b . u )
assume
s in rng the
mapping of
(commute N,u,(Omega Y))
;
:: thesis: s <= b . u
then consider i being
set such that A15:
i in dom the
mapping of
(commute N,u,(Omega Y))
and A16:
the
mapping of
(commute N,u,(Omega Y)) . i = s
by FUNCT_1:def 5;
reconsider i =
i as
Point of
N by A3, A15, Lm6;
A17:
s = (the mapping of N . i) . u
by A16, Th24;
A18:
the
mapping of
N . i in rng the
mapping of
N
by A3, FUNCT_1:def 5;
the
mapping of
N . i is
Function of
X,
(Omega Y)
by WAYBEL24:21;
then reconsider k = the
mapping of
N . i as
Element of
((Omega Y) |^ the carrier of X) by WAYBEL24:19;
reconsider k' =
k as
Element of
(product (the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
k <= b
by A11, A18;
then
k' <= b'
by YELLOW_1:def 5;
hence
s <= b . u
by A12, A17, WAYBEL_3:28;
:: thesis: verum
end;
hence
a' . u <= b' . u
by A12, A13, A14, YELLOW_0:30;
:: thesis: verum
end;
hence
a <= b
by A4, WAYBEL_3:28;
:: thesis: verum
end;
hence
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
by YELLOW_0:15; :: thesis: verum