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