let X be set ; for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f
let L be non empty complete continuous Poset; for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f
let f be Function of (FixedUltraFilters X), the carrier of L; (f -extension_to_hom) | (FixedUltraFilters X) = f
set FUF = FixedUltraFilters X;
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
A1:
InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #)
by YELLOW_1:def 1;
set F = f -extension_to_hom ;
A2: the carrier of (BoolePoset X) =
the carrier of (LattPOSet (BooleLatt X))
by YELLOW_1:def 2
.=
bool X
by LATTICE3:def 1
;
now ( FixedUltraFilters X = dom ((f -extension_to_hom) | (FixedUltraFilters X)) & FixedUltraFilters X = dom f & ( for xf being object st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )A3:
dom (f -extension_to_hom) = the
carrier of
(InclPoset (Filt (BoolePoset X)))
by FUNCT_2:def 1;
hence
FixedUltraFilters X = dom ((f -extension_to_hom) | (FixedUltraFilters X))
by A1, Th9, RELAT_1:62;
( FixedUltraFilters X = dom f & ( for xf being object st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )thus
FixedUltraFilters X = dom f
by FUNCT_2:def 1;
for xf being object st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xflet xf be
object ;
( xf in FixedUltraFilters X implies ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf )assume A4:
xf in FixedUltraFilters X
;
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xfthen reconsider FUF9 =
FixedUltraFilters X as non
empty Subset-Family of
(BoolePoset X) ;
A5:
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = (f -extension_to_hom) . xf
by A4, FUNCT_1:49;
FixedUltraFilters X c= dom (f -extension_to_hom)
by A1, A3, Th9;
then reconsider x9 =
xf as
Element of
(InclPoset (Filt (BoolePoset X))) by A4, FUNCT_2:def 1;
reconsider xf9 =
xf as
Element of
FUF9 by A4;
set Xs =
{ ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } ;
reconsider f9 =
f as
Function of
FUF9, the
carrier of
L ;
f9 . xf9 is
Element of
L
;
then reconsider fxf =
f . xf9 as
Element of
L ;
consider xx being
Element of
(BoolePoset X) such that A6:
xf = uparrow xx
and A7:
ex
y being
Element of
X st
xx = {y}
by A4;
A8:
{ ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } is_<=_than fxf
proof
let b be
Element of
L;
LATTICE3:def 9 ( not b in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } or b <= fxf )
assume
b in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 }
;
b <= fxf
then consider Y being
Subset of
X such that A9:
b = "/\" (
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,
L)
and A10:
Y in x9
;
set Xsi =
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,
L
by YELLOW_0:17;
then A11:
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is_>=_than b
by A9, YELLOW_0:def 10;
reconsider Y =
Y as
Element of
(BoolePoset X) by A6, A10;
consider y being
Element of
X such that A12:
xx = {y}
by A7;
xx <= Y
by A6, A10, WAYBEL_0:18;
then
xx c= Y
by YELLOW_1:2;
then
y in Y
by A12, ZFMISC_1:31;
then
fxf in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) }
by A6, A12;
hence
b <= fxf
by A11;
verum
end; A13:
for
a being
Element of
L st
{ ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } is_<=_than a holds
fxf <= a
ex_sup_of { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } ,
L
by YELLOW_0:17;
then
f . xf = "\/" (
{ ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } ,
L)
by A8, A13, YELLOW_0:def 9;
hence
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf
by A5, Def3;
verum end;
hence
(f -extension_to_hom) | (FixedUltraFilters X) = f
; verum