let L be complete continuous LATTICE; :: thesis: for R being Subset of [:L,L:]
for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds
ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
let R be Subset of [:L,L:]; :: thesis: for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds
ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
let k be kernel Function of L,L; :: thesis: ( k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) implies ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) ) )
assume that
A1: k is directed-sups-preserving and
A2: R = [:k,k:] " (id the carrier of L) ; :: thesis: ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
set ER = EqRel R;
R is Equivalence_Relation of the carrier of L by A2, Th2;
then A3: EqRel R = R by Def1;
reconsider rngk = rng k as non empty set ;
defpred S1[ set , set ] means ex x, y being Element of L st
( $1 = Class ((EqRel R),x) & $2 = Class ((EqRel R),y) & k . x <= k . y );
set xx = the Element of L;
set cL = the carrier of L;
Class ((EqRel R), the Element of L) in Class (EqRel R) by EQREL_1:def 3;
then reconsider CER = Class (EqRel R) as non empty Subset-Family of the carrier of L ;
consider LR being non empty strict RelStr such that
A4: the carrier of LR = CER and
A5: for a, b being Element of LR holds
( a <= b iff S1[a,b] ) from YELLOW_0:sch 1();
 defpred S2[ set , set ] means ex a being Element of the carrier of L st
( $1 = Class ((EqRel R),a) & $2 = k . a );
A6: dom k = the carrier of L by FUNCT_2:def 1;
A7: for x being Element of CER ex y being Element of rngk st S2[x,y]
proof
let x be Element of CER; :: thesis: ex y being Element of rngk st S2[x,y]
consider y being object such that
A8: y in the carrier of L and
A9: x = Class ((EqRel R),y) by EQREL_1:def 3;
reconsider y = y as Element of L by A8;
reconsider ky = k . y as Element of rngk by A6, FUNCT_1:def 3;
take ky ; :: thesis: S2[x,ky]
thus S2[x,ky] by A9; :: thesis: verum
end;
consider f being Function of CER,rngk such that
A10: for x being Element of CER holds S2[x,f . x] from FUNCT_2:sch 3(A7);
 A11: dom [:k,k:] = [: the carrier of L, the carrier of L:] by A6, FUNCT_3:def 8;
A12: for a, b being Element of the carrier of L holds
( Class ((EqRel R),a) = Class ((EqRel R),b) iff k . a = k . b )
proof
let a, b be Element of the carrier of L; :: thesis: ( Class ((EqRel R),a) = Class ((EqRel R),b) iff k . a = k . b )
hereby :: thesis: ( k . a = k . b implies Class ((EqRel R),a) = Class ((EqRel R),b) )
assume Class ((EqRel R),a) = Class ((EqRel R),b) ; :: thesis: k . a = k . b
then a in Class ((EqRel R),b) by EQREL_1:23;
then [a,b] in R by A3, EQREL_1:19;
then [:k,k:] . (a,b) in id the carrier of L by A2, FUNCT_1:def 7;
then [(k . a),(k . b)] in id the carrier of L by A6, FUNCT_3:def 8;
hence k . a = k . b by RELAT_1:def 10; :: thesis: verum
end;
assume k . a = k . b ; :: thesis: Class ((EqRel R),a) = Class ((EqRel R),b)
then [(k . a),(k . b)] in id the carrier of L by RELAT_1:def 10;
then ( [a,b] in [: the carrier of L, the carrier of L:] & [:k,k:] . (a,b) in id the carrier of L ) by A6, FUNCT_3:def 8, ZFMISC_1:def 2;
then [a,b] in EqRel R by A2, A3, A11, FUNCT_1:def 7;
then a in Class ((EqRel R),b) by EQREL_1:19;
hence Class ((EqRel R),a) = Class ((EqRel R),b) by EQREL_1:23; :: thesis: verum
end;
A13: for x being Element of L holds f . (Class ((EqRel R),x)) = k . x
proof
let x be Element of L; :: thesis: f . (Class ((EqRel R),x)) = k . x
reconsider CERx = Class ((EqRel R),x) as Element of CER by EQREL_1:def 3;
ex a being Element of the carrier of L st
( CERx = Class ((EqRel R),a) & f . CERx = k . a ) by A10;
hence f . (Class ((EqRel R),x)) = k . x by A12; :: thesis: verum
end;
A14: for x being Element of LR ex a being Element of L st x = Class ((EqRel R),a)
proof
let x be Element of LR; :: thesis: ex a being Element of L st x = Class ((EqRel R),a)
x in CER by A4;
then consider a being object such that
A15: a in the carrier of L and
A16: x = Class ((EqRel R),a) by EQREL_1:def 3;
reconsider a = a as Element of L by A15;
take a ; :: thesis: x = Class ((EqRel R),a)
thus x = Class ((EqRel R),a) by A16; :: thesis: verum
end;
now :: thesis: for x1, x2 being object st x1 in CER & x2 in CER & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in CER & x2 in CER & f . x1 = f . x2 implies x1 = x2 )
assume that
A17: x1 in CER and
A18: x2 in CER and
A19: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x19 = x1 as Element of LR by A4, A17;
consider a being Element of L such that
A20: x19 = Class ((EqRel R),a) by A14;
reconsider x29 = x2 as Element of LR by A4, A18;
consider b being Element of L such that
A21: x29 = Class ((EqRel R),b) by A14;
A22: f . x29 = k . b by A13, A21;
f . x19 = k . a by A13, A20;
hence x1 = x2 by A12, A19, A20, A21, A22; :: thesis: verum
end;
then A23: f is one-to-one by FUNCT_2:19;
set tIR = the InternalRel of LR;
A24: dom f = CER by FUNCT_2:def 1;
reconsider f = f as Function of LR,(Image k) by A4, YELLOW_0:def 15;
now :: thesis: for y being object holds
( ( y in rng f implies y in rngk ) & ( y in rngk implies y in rng f ) )
let y be object ; :: thesis: ( ( y in rng f implies y in rngk ) & ( y in rngk implies y in rng f ) )
hereby :: thesis: ( y in rngk implies y in rng f )
assume y in rng f ; :: thesis: y in rngk
then consider x being object such that
A25: x in dom f and
A26: y = f . x by FUNCT_1:def 3;
reconsider x = x as Element of LR by A25;
consider a being Element of L such that
A27: x = Class ((EqRel R),a) by A14;
f . x = k . a by A13, A27;
hence y in rngk by A6, A26, FUNCT_1:def 3; :: thesis: verum
end;
assume y in rngk ; :: thesis: y in rng f
then consider x being object such that
A28: x in dom k and
A29: y = k . x by FUNCT_1:def 3;
reconsider x = x as Element of L by A28;
( Class ((EqRel R),x) in CER & f . (Class ((EqRel R),x)) = k . x ) by A13, EQREL_1:def 3;
hence y in rng f by A24, A29, FUNCT_1:def 3; :: thesis: verum
end;
then A30: ( the carrier of (Image k) = rngk & rng f = rngk ) by TARSKI:2, YELLOW_0:def 15;
for x, y being Element of LR holds
( x <= y iff f . x <= f . y )
proof
let x, y be Element of LR; :: thesis: ( x <= y iff f . x <= f . y )
x in CER by A4;
then consider a being object such that
A31: a in the carrier of L and
A32: x = Class ((EqRel R),a) by EQREL_1:def 3;
hereby :: thesis: ( f . x <= f . y implies x <= y )
assume x <= y ; :: thesis: f . x <= f . y
then consider c, d being Element of L such that
A33: ( x = Class ((EqRel R),c) & y = Class ((EqRel R),d) ) and
A34: k . c <= k . d by A5;
( f . x = k . c & f . y = k . d ) by A13, A33;
hence f . x <= f . y by A34, YELLOW_0:60; :: thesis: verum
end;
reconsider a = a as Element of L by A31;
assume A35: f . x <= f . y ; :: thesis: x <= y
y in CER by A4;
then consider b being object such that
A36: b in the carrier of L and
A37: y = Class ((EqRel R),b) by EQREL_1:def 3;
reconsider b = b as Element of L by A36;
A38: f . y = k . b by A13, A37;
f . x = k . a by A13, A32;
then k . a <= k . b by A38, A35, YELLOW_0:59;
hence x <= y by A5, A32, A37; :: thesis: verum
end;
then A39: f is isomorphic by A23, A30, WAYBEL_0:66;
then A40: LR, Image k are_isomorphic ;
then Image k,LR are_isomorphic by WAYBEL_1:6;
then reconsider LR = LR as non empty strict Poset by Th15, Th16, Th17;
Image k is complete by WAYBEL_1:54;
then reconsider LR = LR as non empty strict complete Poset by A40, Th18, WAYBEL_1:6;
reconsider LR = LR as strict complete LATTICE ;
Image k is continuous LATTICE by A1, WAYBEL15:14;
then reconsider LR = LR as strict complete continuous LATTICE by A40, WAYBEL15:9, WAYBEL_1:6;
reconsider f9 = f " as Function of (Image k),LR by A23, A30, FUNCT_2:25;
set IR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ;
A41: f9 is isomorphic by A39, WAYBEL_0:68;
then A42: ( corestr k is infs-preserving & f9 is infs-preserving ) by WAYBEL13:20, WAYBEL_1:56;
take LR ; :: thesis: ( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
thus the carrier of LR = Class (EqRel R) by A4; :: thesis: ( the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
now :: thesis: for z being object holds
( ( z in the InternalRel of LR implies z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ) & ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR ) )
let z be object ; :: thesis: ( ( z in the InternalRel of LR implies z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ) & ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR ) )
hereby :: thesis: ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR )
assume A43: z in the InternalRel of LR ; :: thesis: z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y }
then consider a, b being object such that
A44: ( a in CER & b in CER ) and
A45: z = [a,b] by A4, ZFMISC_1:def 2;
reconsider a = a, b = b as Element of LR by A4, A44;
a <= b by A43, A45, ORDERS_2:def 5;
then ex x, y being Element of L st
( a = Class ((EqRel R),x) & b = Class ((EqRel R),y) & k . x <= k . y ) by A5;
hence z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } by A45; :: thesis: verum
end;
assume z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ; :: thesis: z in the InternalRel of LR
then consider x, y being Element of L such that
A46: z = [(Class ((EqRel R),x)),(Class ((EqRel R),y))] and
A47: k . x <= k . y ;
reconsider b = Class ((EqRel R),y) as Element of LR by A4, EQREL_1:def 3;
reconsider a = Class ((EqRel R),x) as Element of LR by A4, EQREL_1:def 3;
a <= b by A5, A47;
hence z in the InternalRel of LR by A46, ORDERS_2:def 5; :: thesis: verum
end;
hence the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } by TARSKI:2; :: thesis: for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR
let g be Function of L,LR; :: thesis: ( ( for x being Element of L holds g . x = Class ((EqRel R),x) ) implies g is CLHomomorphism of L,LR )
assume A48: for x being Element of L holds g . x = Class ((EqRel R),x) ; :: thesis: g is CLHomomorphism of L,LR
now :: thesis: for x being object st x in the carrier of L holds
(f9 * (corestr k)) . x = g . x
let x be object ; :: thesis: ( x in the carrier of L implies (f9 * (corestr k)) . x = g . x )
assume A49: x in the carrier of L ; :: thesis: (f9 * (corestr k)) . x = g . x
then reconsider x9 = x as Element of L ;
A50: ( f . (Class ((EqRel R),x9)) = k . x9 & Class ((EqRel R),x9) in CER ) by A13, EQREL_1:def 3;
dom (corestr k) = the carrier of L by FUNCT_2:def 1;
hence (f9 * (corestr k)) . x = f9 . ((corestr k) . x) by A49, FUNCT_1:13
.= f9 . (k . x) by WAYBEL_1:30
.= Class ((EqRel R),x9) by A24, A23, A50, FUNCT_1:32
.= g . x by A48 ;
:: thesis: verum
end;
then A51: g = f9 * (corestr k) by FUNCT_2:12;
A52: corestr k is directed-sups-preserving by A1, Th22;
reconsider f9 = f9 as sups-preserving Function of (Image k),LR by A41, WAYBEL13:20;
f9 is directed-sups-preserving ;
then A53: g is directed-sups-preserving by A51, A52, WAYBEL15:11;
g is infs-preserving by A51, A42, Th25;
hence g is CLHomomorphism of L,LR by A53, WAYBEL16:def 1; :: thesis: verum