let L be complete continuous LATTICE; for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k)
let k be directed-sups-preserving kernel Function of L,L; k = kernel_op (kernel_congruence k)
set kc = kernel_congruence k;
set cL = the carrier of L;
set km = kernel_op (kernel_congruence k);
A1:
dom k = the carrier of L
by FUNCT_2:def 1;
A2:
kernel_op (kernel_congruence k) <= id L
by WAYBEL_1:def 15;
A3:
k <= id L
by WAYBEL_1:def 15;
A4:
kernel_congruence k is CLCongruence
by Th40;
then A5:
kernel_congruence k = [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] " (id the carrier of L)
by Th36;
reconsider kc9 = kernel_congruence k as Equivalence_Relation of the carrier of L by A4;
field kc9 = the carrier of L
by ORDERS_1:12;
then A6:
kc9 is_transitive_in the carrier of L
by RELAT_2:def 16;
A7:
dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] = [:(dom (kernel_op (kernel_congruence k))),(dom (kernel_op (kernel_congruence k))):]
by FUNCT_3:def 8;
A8:
dom (kernel_op (kernel_congruence k)) = the carrier of L
by FUNCT_2:def 1;
A9:
dom [:k,k:] = [:(dom k),(dom k):]
by FUNCT_3:def 8;
now for x being object st x in the carrier of L holds
k . x = (kernel_op (kernel_congruence k)) . xlet x be
object ;
( x in the carrier of L implies k . x = (kernel_op (kernel_congruence k)) . x )assume
x in the
carrier of
L
;
k . x = (kernel_op (kernel_congruence k)) . xthen reconsider x9 =
x as
Element of
L ;
A10:
k . (k . x9) =
(k * k) . x9
by A1, FUNCT_1:13
.=
k . x9
by QUANTAL1:def 9
;
A11:
(
[(k . x9),(k . x9)] in id the
carrier of
L &
[:k,k:] . (
(k . x9),
x9)
= [(k . (k . x9)),(k . x9)] )
by A1, FUNCT_3:def 8, RELAT_1:def 10;
[(k . x9),x9] in dom [:k,k:]
by A1, A9, ZFMISC_1:def 2;
then A12:
[(k . x9),x9] in kernel_congruence k
by A10, A11, FUNCT_1:def 7;
A13:
(kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9) =
((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x9
by A8, FUNCT_1:13
.=
(kernel_op (kernel_congruence k)) . x9
by QUANTAL1:def 9
;
(kernel_op (kernel_congruence k)) . (k . x9) <= (id L) . (k . x9)
by A2, YELLOW_2:9;
then A14:
(kernel_op (kernel_congruence k)) . (k . x9) <= k . x9
by FUNCT_1:18;
A15:
(
[((kernel_op (kernel_congruence k)) . x9),((kernel_op (kernel_congruence k)) . x9)] in id the
carrier of
L &
[:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . (
x9,
((kernel_op (kernel_congruence k)) . x9))
= [((kernel_op (kernel_congruence k)) . x9),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9))] )
by A8, FUNCT_3:def 8, RELAT_1:def 10;
[x9,((kernel_op (kernel_congruence k)) . x9)] in dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):]
by A8, A7, ZFMISC_1:def 2;
then
[x9,((kernel_op (kernel_congruence k)) . x9)] in kernel_congruence k
by A5, A13, A15, FUNCT_1:def 7;
then A16:
[(k . x9),((kernel_op (kernel_congruence k)) . x9)] in kernel_congruence k
by A6, A12;
then
[:k,k:] . (
(k . x9),
((kernel_op (kernel_congruence k)) . x9))
in id the
carrier of
L
by FUNCT_1:def 7;
then
[(k . (k . x9)),(k . ((kernel_op (kernel_congruence k)) . x9))] in id the
carrier of
L
by A1, FUNCT_3:def 8;
then A17:
k . ((kernel_op (kernel_congruence k)) . x9) =
k . (k . x9)
by RELAT_1:def 10
.=
(k * k) . x9
by A1, FUNCT_1:13
.=
k . x9
by QUANTAL1:def 9
;
[:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . (
(k . x9),
((kernel_op (kernel_congruence k)) . x9))
in id the
carrier of
L
by A5, A16, FUNCT_1:def 7;
then
[((kernel_op (kernel_congruence k)) . (k . x9)),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9))] in id the
carrier of
L
by A8, FUNCT_3:def 8;
then A18:
(kernel_op (kernel_congruence k)) . (k . x9) =
(kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9)
by RELAT_1:def 10
.=
((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x9
by A8, FUNCT_1:13
.=
(kernel_op (kernel_congruence k)) . x9
by QUANTAL1:def 9
;
k . ((kernel_op (kernel_congruence k)) . x9) <= (id L) . ((kernel_op (kernel_congruence k)) . x9)
by A3, YELLOW_2:9;
then
k . ((kernel_op (kernel_congruence k)) . x9) <= (kernel_op (kernel_congruence k)) . x9
by FUNCT_1:18;
hence
k . x = (kernel_op (kernel_congruence k)) . x
by A17, A18, A14, YELLOW_0:def 3;
verum end;
hence
k = kernel_op (kernel_congruence k)
by FUNCT_2:12; verum