let L be lower-bounded algebraic LATTICE; :: thesis: ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )
deffunc H1( Element of L) -> Element of K32( the carrier of L) = compactbelow $1;
A1: for y being Element of L holds H1(y) is Element of (InclPoset (Ids (CompactSublatt L)))
proof
let y be Element of L; :: thesis: H1(y) is Element of (InclPoset (Ids (CompactSublatt L)))
reconsider comy = compactbelow y as non empty directed Subset of L by WAYBEL_8:def 4;
reconsider comy = comy as non empty Subset of (CompactSublatt L) by Th2;
reconsider comy = comy as non empty directed Subset of (CompactSublatt L) by WAYBEL10:23;
now :: thesis: for x1, z1 being Element of (CompactSublatt L) st x1 in comy & z1 <= x1 holds
z1 in comy
let x1, z1 be Element of (CompactSublatt L); :: thesis: ( x1 in comy & z1 <= x1 implies z1 in comy )
reconsider x2 = x1, z2 = z1 as Element of L by YELLOW_0:58;
assume ( x1 in comy & z1 <= x1 ) ; :: thesis: z1 in comy
then ( x2 <= y & z2 <= x2 ) by WAYBEL_8:4, YELLOW_0:59;
then A2: z2 <= y by ORDERS_2:3;
z2 is compact by WAYBEL_8:def 1;
hence z1 in comy by A2, WAYBEL_8:4; :: thesis: verum
end;
then comy is lower by WAYBEL_0:def 19;
hence H1(y) is Element of (InclPoset (Ids (CompactSublatt L))) by YELLOW_2:41; :: thesis: verum
end;
consider g1 being Function of L,(InclPoset (Ids (CompactSublatt L))) such that
A3: for y being Element of L holds g1 . y = H1(y) from FUNCT_2:sch 9(A1);
now :: thesis: for k being object st k in the carrier of (InclPoset (Ids (CompactSublatt L))) holds
k in the carrier of (BoolePoset the carrier of (CompactSublatt L))
let k be object ; :: thesis: ( k in the carrier of (InclPoset (Ids (CompactSublatt L))) implies k in the carrier of (BoolePoset the carrier of (CompactSublatt L)) )
assume k in the carrier of (InclPoset (Ids (CompactSublatt L))) ; :: thesis: k in the carrier of (BoolePoset the carrier of (CompactSublatt L))
then k is Ideal of (CompactSublatt L) by YELLOW_2:41;
then k is Element of (BoolePoset the carrier of (CompactSublatt L)) by WAYBEL_8:26;
hence k in the carrier of (BoolePoset the carrier of (CompactSublatt L)) ; :: thesis: verum
end;
then the carrier of (InclPoset (Ids (CompactSublatt L))) c= the carrier of (BoolePoset the carrier of (CompactSublatt L)) ;
then reconsider g = g1 as Function of L,(BoolePoset the carrier of (CompactSublatt L)) by FUNCT_2:7;
take g ; :: thesis: ( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )
A4: g1 is isomorphic by A3, Th16;
A5: InclPoset (Ids (CompactSublatt L)) is full infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset the carrier of (CompactSublatt L) by Th23;
then ex g2 being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g1 = g2 & g2 is infs-preserving ) by A4, Th21;
hence g is infs-preserving ; :: thesis: ( g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )
ex g3 being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g1 = g3 & g3 is directed-sups-preserving ) by A4, A5, Th22;
hence g is directed-sups-preserving ; :: thesis: ( g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )
thus g is V13() by A4; :: thesis: for x being Element of L holds g . x = compactbelow x
let x be Element of L; :: thesis: g . x = compactbelow x
thus g . x = compactbelow x by A3; :: thesis: verum