let X be set ; :: thesis: 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; :: thesis: 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; :: thesis: (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;
A2: the carrier of (BoolePoset X) =
the carrier of (LattPOSet (BooleLatt X))
by YELLOW_1:def 2
.=
bool X
by LATTICE3:def 1
;
set F = f -extension_to_hom ;
now A3:
dom (f -extension_to_hom ) = the
carrier of
(InclPoset (Filt (BoolePoset X)))
by FUNCT_2:def 1;
then A4:
FixedUltraFilters X c= dom (f -extension_to_hom )
by A1, Th9;
thus
FixedUltraFilters X = dom ((f -extension_to_hom ) | (FixedUltraFilters X))
by A1, A3, Th9, RELAT_1:91;
:: thesis: ( FixedUltraFilters X = dom f & ( for xf being set 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;
:: thesis: for xf being set st xf in FixedUltraFilters X holds
((f -extension_to_hom ) | (FixedUltraFilters X)) . xf = f . xflet xf be
set ;
:: thesis: ( xf in FixedUltraFilters X implies ((f -extension_to_hom ) | (FixedUltraFilters X)) . xf = f . xf )assume A5:
xf in FixedUltraFilters X
;
:: thesis: ((f -extension_to_hom ) | (FixedUltraFilters X)) . xf = f . xfthen consider xx being
Element of
(BoolePoset X) such that A6:
xf = uparrow xx
and A7:
ex
y being
Element of
X st
xx = {y}
;
A8:
((f -extension_to_hom ) | (FixedUltraFilters X)) . xf = (f -extension_to_hom ) . xf
by A5, FUNCT_1:72;
reconsider x' =
xf as
Element of
(InclPoset (Filt (BoolePoset X))) by A4, A5, FUNCT_2:def 1;
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 x' } ;
A9:
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 x' } ,
L
by YELLOW_0:17;
reconsider FUF' =
FixedUltraFilters X as non
empty Subset-Family of
(BoolePoset X) by A5;
reconsider xf' =
xf as
Element of
FUF' by A5;
reconsider f' =
f as
Function of
FUF',the
carrier of
L ;
f' . xf' is
Element of
L
;
then reconsider fxf =
f . xf' as
Element of
L ;
A10:
{ ("/\" { (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 x' } is_<=_than fxf
proof
let b be
Element of
L;
:: according to LATTICE3:def 9 :: thesis: ( 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 x' } 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 x' }
;
:: thesis: b <= fxf
then consider Y being
Subset of
X such that A11:
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 A12:
Y in x'
;
set Xsi =
{ (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
consider y being
Element of
X such that A13:
xx = {y}
by A7;
reconsider Y =
Y as
Element of
(BoolePoset X) by A6, A12;
xx <= Y
by A6, A12, WAYBEL_0:18;
then
xx c= Y
by YELLOW_1:2;
then
y in Y
by A13, ZFMISC_1:37;
then A14:
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, A13;
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
{ (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 A11, YELLOW_0:def 10;
hence
b <= fxf
by A14, LATTICE3:def 8;
:: thesis: verum
end;
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 x' } is_<=_than a holds
fxf <= a
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 x' } ,
L
by A9, A10, YELLOW_0:def 9;
hence
((f -extension_to_hom ) | (FixedUltraFilters X)) . xf = f . xf
by A8, Def3;
:: thesis: verum end;
hence
(f -extension_to_hom ) | (FixedUltraFilters X) = f
by FUNCT_1:9; :: thesis: verum