let L be complete LATTICE; 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:]; ( 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
; ( 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
R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L)proof
let D be
Subset of
L;
WAYBEL_0:def 37 ( 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
;
WAYBEL_0:def 31 ( 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
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;
"\/" (((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);
WAYBEL_0:def 1 ( 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
;
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
;
( z in S9 & x <= z & y <= z )
thus
z in S9
by A19;
( 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;
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;
verum
end;
then A28:
proj1 S = (kernel_op R) .: D
by TARSKI:2;
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)
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;
verum
end;
now 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 ;
( ( 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 ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R )
assume A36:
x in R
;
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;
verum
end; assume A42:
x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L)
;
x in Rthen 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;
verum end;
hence
R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L)
by TARSKI:2; verum