let L be complete LATTICE; :: thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds
( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )
let R be non empty Subset of [:L,L:]; :: thesis: ( R is CLCongruence implies ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) )
set k = kernel_op R;
set cL = the carrier of L;
A1: dom (kernel_op R) = the carrier of L by FUNCT_2:def 1;
assume A2: R is CLCongruence ; :: thesis: ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )
then A3: R is Equivalence_Relation of the carrier of L ;
then A4: EqRel R = R by Def1;
A5: subrelstr R is CLSubFrame of [:L,L:] by A2;
thus kernel_op R is directed-sups-preserving :: thesis: R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L)
proof
let D be Subset of L; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or kernel_op R preserves_sup_of D )
assume that
A6: ( not D is empty & D is directed ) and
ex_sup_of D,L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (kernel_op R) .: D,L & "\/" (((kernel_op R) .: D),L) = (kernel_op R) . ("\/" (D,L)) )
consider e being object such that
A7: e in D by A6, XBOOLE_0:def 1;
set S = { [((kernel_op R) . x),x] where x is Element of L : x in D } ;
A8: { [((kernel_op R) . x),x] where x is Element of L : x in D } c= R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [((kernel_op R) . x),x] where x is Element of L : x in D } or x in R )
assume x in { [((kernel_op R) . x),x] where x is Element of L : x in D } ; :: thesis: x in R
then consider a being Element of L such that
A9: x = [((kernel_op R) . a),a] and
a in D ;
(kernel_op R) . a = inf (Class ((EqRel R),a)) by A2, Def3;
hence x in R by A2, A9, Th35; :: thesis: verum
end;
then reconsider S9 = { [((kernel_op R) . x),x] where x is Element of L : x in D } as Subset of (subrelstr R) by YELLOW_0:def 15;
reconsider S = { [((kernel_op R) . x),x] where x is Element of L : x in D } as Subset of [:L,L:] by A8, XBOOLE_1:1;
thus ex_sup_of (kernel_op R) .: D,L by YELLOW_0:17; :: thesis: "\/" (((kernel_op R) .: D),L) = (kernel_op R) . ("\/" (D,L))
set d = sup D;
set ds = sup ((kernel_op R) .: D);
A10: ( the carrier of (subrelstr R) = R & ex_sup_of S,[:L,L:] ) by YELLOW_0:17, YELLOW_0:def 15;
reconsider e = e as Element of L by A7;
A11: [((kernel_op R) . e),e] in S by A7;
A12: S9 is directed
proof
let x, y be Element of (subrelstr R); :: according to WAYBEL_0:def 1 :: thesis: ( not x in S9 or not y in S9 or ex b1 being Element of the carrier of (subrelstr R) st
( b1 in S9 & x <= b1 & y <= b1 ) )
assume that
A13: x in S9 and
A14: y in S9 ; :: thesis: ex b1 being Element of the carrier of (subrelstr R) st
( b1 in S9 & x <= b1 & y <= b1 )
consider a being Element of L such that
A15: x = [((kernel_op R) . a),a] and
A16: a in D by A13;
consider b being Element of L such that
A17: y = [((kernel_op R) . b),b] and
A18: b in D by A14;
consider c being Element of L such that
A19: c in D and
A20: a <= c and
A21: b <= c by A6, A16, A18;
set z = [((kernel_op R) . c),c];
[((kernel_op R) . c),c] in S9 by A19;
then reconsider z = [((kernel_op R) . c),c] as Element of (subrelstr R) ;
take z ; :: thesis: ( z in S9 & x <= z & y <= z )
thus z in S9 by A19; :: thesis: ( x <= z & y <= z )
(kernel_op R) . a <= (kernel_op R) . c by A20, WAYBEL_1:def 2;
then [((kernel_op R) . a),a] <= [((kernel_op R) . c),c] by A20, YELLOW_3:11;
hence x <= z by A15, YELLOW_0:60; :: thesis: y <= z
(kernel_op R) . b <= (kernel_op R) . c by A21, WAYBEL_1:def 2;
then [((kernel_op R) . b),b] <= [((kernel_op R) . c),c] by A21, YELLOW_3:11;
hence y <= z by A17, YELLOW_0:60; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in proj1 S implies x in (kernel_op R) .: D ) & ( x in (kernel_op R) .: D implies x in proj1 S ) )
let x be object ; :: thesis: ( ( x in proj1 S implies x in (kernel_op R) .: D ) & ( x in (kernel_op R) .: D implies x in proj1 S ) )
hereby :: thesis: ( x in (kernel_op R) .: D implies x in proj1 S )
assume x in proj1 S ; :: thesis: x in (kernel_op R) .: D
then consider y being object such that
A22: [x,y] in S by XTUPLE_0:def 12;
consider a being Element of L such that
A23: [x,y] = [((kernel_op R) . a),a] and
A24: a in D by A22;
x = (kernel_op R) . a by A23, XTUPLE_0:1;
hence x in (kernel_op R) .: D by A1, A24, FUNCT_1:def 6; :: thesis: verum
end;
assume x in (kernel_op R) .: D ; :: thesis: x in proj1 S
then consider y being object such that
A25: y in dom (kernel_op R) and
A26: y in D and
A27: x = (kernel_op R) . y by FUNCT_1:def 6;
reconsider y = y as Element of L by A25;
[((kernel_op R) . y),y] in S by A26;
hence x in proj1 S by A27, XTUPLE_0:def 12; :: thesis: verum
end;
then A28: proj1 S = (kernel_op R) .: D by TARSKI:2;
now :: thesis: for x being object holds
( ( x in proj2 S implies x in D ) & ( x in D implies x in proj2 S ) )
let x be object ; :: thesis: ( ( x in proj2 S implies x in D ) & ( x in D implies x in proj2 S ) )
hereby :: thesis: ( x in D implies x in proj2 S )
assume x in proj2 S ; :: thesis: x in D
then consider y being object such that
A29: [y,x] in S by XTUPLE_0:def 13;
ex a being Element of L st
( [y,x] = [((kernel_op R) . a),a] & a in D ) by A29;
hence x in D by XTUPLE_0:1; :: thesis: verum
end;
assume A30: x in D ; :: thesis: x in proj2 S
then reconsider x9 = x as Element of L ;
[((kernel_op R) . x9),x9] in S by A30;
hence x in proj2 S by XTUPLE_0:def 13; :: thesis: verum
end;
then proj2 S = D by TARSKI:2;
then sup S = [(sup ((kernel_op R) .: D)),(sup D)] by A28, Th8, YELLOW_0:17;
then [(sup ((kernel_op R) .: D)),(sup D)] in R by A5, A10, A11, A12, WAYBEL_0:def 4;
then A31: sup ((kernel_op R) .: D) in Class ((EqRel R),(sup D)) by A4, EQREL_1:19;
(kernel_op R) .: D is_<=_than (kernel_op R) . (sup D)
proof
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in (kernel_op R) .: D or b <= (kernel_op R) . (sup D) )
assume b in (kernel_op R) .: D ; :: thesis: b <= (kernel_op R) . (sup D)
then consider a being object such that
A32: a in dom (kernel_op R) and
A33: a in D and
A34: b = (kernel_op R) . a by FUNCT_1:def 6;
reconsider a = a as Element of L by A32;
D is_<=_than sup D by YELLOW_0:32;
then a <= sup D by A33;
hence b <= (kernel_op R) . (sup D) by A34, WAYBEL_1:def 2; :: thesis: verum
end;
then A35: sup ((kernel_op R) .: D) <= (kernel_op R) . (sup D) by YELLOW_0:32;
(kernel_op R) . (sup D) = inf (Class ((EqRel R),(sup D))) by A2, Def3;
then (kernel_op R) . (sup D) <= sup ((kernel_op R) .: D) by A31, YELLOW_2:22;
hence "\/" (((kernel_op R) .: D),L) = (kernel_op R) . ("\/" (D,L)) by A35, YELLOW_0:def 3; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in R implies x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) & ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R ) )
let x be object ; :: thesis: ( ( x in R implies x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) & ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R ) )
hereby :: thesis: ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R )
assume A36: x in R ; :: thesis: x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L)
then x in the carrier of [:L,L:] ;
then x in [: the carrier of L, the carrier of L:] by YELLOW_3:def 2;
then consider x1, x2 being object such that
A37: ( x1 in the carrier of L & x2 in the carrier of L ) and
A38: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of L by A37;
A39: ( (kernel_op R) . x1 = inf (Class ((EqRel R),x1)) & (kernel_op R) . x2 = inf (Class ((EqRel R),x2)) ) by A2, Def3;
x1 in Class ((EqRel R),x2) by A4, A36, A38, EQREL_1:19;
then (kernel_op R) . x1 = (kernel_op R) . x2 by A39, EQREL_1:23;
then A40: [((kernel_op R) . x1),((kernel_op R) . x2)] in id the carrier of L by RELAT_1:def 10;
dom [:(kernel_op R),(kernel_op R):] = [:(dom (kernel_op R)),(dom (kernel_op R)):] by FUNCT_3:def 8;
then A41: [x1,x2] in dom [:(kernel_op R),(kernel_op R):] by A1, ZFMISC_1:87;
[:(kernel_op R),(kernel_op R):] . (x1,x2) = [((kernel_op R) . x1),((kernel_op R) . x2)] by A1, FUNCT_3:def 8;
hence x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) by A38, A40, A41, FUNCT_1:def 7; :: thesis: verum
end;
assume A42: x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ; :: thesis: x in R
then A43: [:(kernel_op R),(kernel_op R):] . x in id the carrier of L by FUNCT_1:def 7;
x in dom [:(kernel_op R),(kernel_op R):] by A42, FUNCT_1:def 7;
then x in [:(dom (kernel_op R)),(dom (kernel_op R)):] by FUNCT_3:def 8;
then consider x1, x2 being object such that
A44: ( x1 in dom (kernel_op R) & x2 in dom (kernel_op R) ) and
A45: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of L by A44;
[:(kernel_op R),(kernel_op R):] . (x1,x2) = [((kernel_op R) . x1),((kernel_op R) . x2)] by A44, FUNCT_3:def 8;
then A46: (kernel_op R) . x1 = (kernel_op R) . x2 by A43, A45, RELAT_1:def 10;
(kernel_op R) . x1 = inf (Class ((EqRel R),x1)) by A2, Def3;
then [((kernel_op R) . x1),x1] in R by A2, Th35;
then A47: [x1,((kernel_op R) . x1)] in R by A3, EQREL_1:6;
(kernel_op R) . x2 = inf (Class ((EqRel R),x2)) by A2, Def3;
then [((kernel_op R) . x2),x2] in R by A2, Th35;
hence x in R by A3, A45, A46, A47, EQREL_1:7; :: thesis: verum
end;
hence R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) by TARSKI:2; :: thesis: verum