let L be complete continuous LATTICE; :: thesis: 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; :: thesis: 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 Th41;
then A5:
kernel_congruence k = [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] " (id the carrier of L)
by Th37;
reconsider kc' = kernel_congruence k as Equivalence_Relation of the carrier of L by A4, Def2;
field kc' = the carrier of L
by ORDERS_1:97;
then A6:
kc' 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 9;
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 9;
now let x be
set ;
:: thesis: ( x in the carrier of L implies k . x = (kernel_op (kernel_congruence k)) . x )assume
x in the
carrier of
L
;
:: thesis: k . x = (kernel_op (kernel_congruence k)) . xthen reconsider x' =
x as
Element of
L ;
A10:
k . (k . x') =
(k * k) . x'
by A1, FUNCT_1:23
.=
k . x'
by QUANTAL1:def 9
;
A11:
(
[(k . x'),(k . x')] in id the
carrier of
L &
[:k,k:] . (k . x'),
x' = [(k . (k . x')),(k . x')] )
by A1, FUNCT_3:def 9, RELAT_1:def 10;
[(k . x'),x'] in dom [:k,k:]
by A1, A9, ZFMISC_1:def 2;
then A12:
[(k . x'),x'] in kernel_congruence k
by A10, A11, FUNCT_1:def 13;
A13:
(kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x') =
((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x'
by A8, FUNCT_1:23
.=
(kernel_op (kernel_congruence k)) . x'
by QUANTAL1:def 9
;
(kernel_op (kernel_congruence k)) . (k . x') <= (id L) . (k . x')
by A2, YELLOW_2:10;
then A14:
(kernel_op (kernel_congruence k)) . (k . x') <= k . x'
by FUNCT_1:35;
A15:
(
[((kernel_op (kernel_congruence k)) . x'),((kernel_op (kernel_congruence k)) . x')] in id the
carrier of
L &
[:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . x',
((kernel_op (kernel_congruence k)) . x') = [((kernel_op (kernel_congruence k)) . x'),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x'))] )
by A8, FUNCT_3:def 9, RELAT_1:def 10;
[x',((kernel_op (kernel_congruence k)) . x')] in dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):]
by A8, A7, ZFMISC_1:def 2;
then
[x',((kernel_op (kernel_congruence k)) . x')] in kernel_congruence k
by A5, A13, A15, FUNCT_1:def 13;
then A16:
[(k . x'),((kernel_op (kernel_congruence k)) . x')] in kernel_congruence k
by A6, A12, RELAT_2:def 8;
then
[:k,k:] . (k . x'),
((kernel_op (kernel_congruence k)) . x') in id the
carrier of
L
by FUNCT_1:def 13;
then
[(k . (k . x')),(k . ((kernel_op (kernel_congruence k)) . x'))] in id the
carrier of
L
by A1, FUNCT_3:def 9;
then A17:
k . ((kernel_op (kernel_congruence k)) . x') =
k . (k . x')
by RELAT_1:def 10
.=
(k * k) . x'
by A1, FUNCT_1:23
.=
k . x'
by QUANTAL1:def 9
;
[:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . (k . x'),
((kernel_op (kernel_congruence k)) . x') in id the
carrier of
L
by A5, A16, FUNCT_1:def 13;
then
[((kernel_op (kernel_congruence k)) . (k . x')),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x'))] in id the
carrier of
L
by A8, FUNCT_3:def 9;
then A18:
(kernel_op (kernel_congruence k)) . (k . x') =
(kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x')
by RELAT_1:def 10
.=
((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x'
by A8, FUNCT_1:23
.=
(kernel_op (kernel_congruence k)) . x'
by QUANTAL1:def 9
;
k . ((kernel_op (kernel_congruence k)) . x') <= (id L) . ((kernel_op (kernel_congruence k)) . x')
by A3, YELLOW_2:10;
then
k . ((kernel_op (kernel_congruence k)) . x') <= (kernel_op (kernel_congruence k)) . x'
by FUNCT_1:35;
hence
k . x = (kernel_op (kernel_congruence k)) . x
by A17, A18, A14, YELLOW_0:def 3;
:: thesis: verum end;
hence
k = kernel_op (kernel_congruence k)
by FUNCT_2:18; :: thesis: verum