let L be non empty Poset; :: thesis: for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
let p be Function of L,L; :: thesis: ( p is projection implies for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel )
assume that
A1: p is idempotent and
A2: p is monotone ; :: according to WAYBEL_1:def 13 :: thesis: for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
let Lk be non empty Subset of L; :: thesis: ( Lk = { k where k is Element of L : p . k <= k } implies for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel )
assume A3: Lk = { k where k is Element of L : p . k <= k } ; :: thesis: for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
let pk be Function of (subrelstr Lk),(subrelstr Lk); :: thesis: ( pk = p | Lk implies pk is kernel )
assume A4: pk = p | Lk ; :: thesis: pk is kernel
A5: dom pk = the carrier of (subrelstr Lk) by FUNCT_2:def 1;
hereby :: according to QUANTAL1:def 9,WAYBEL_1:def 13,WAYBEL_1:def 15 :: thesis: pk <= id (subrelstr Lk)
now :: thesis: for x being Element of (subrelstr Lk) holds (pk * pk) . x = pk . x
let x be Element of (subrelstr Lk); :: thesis: (pk * pk) . x = pk . x
A6: x is Element of L by YELLOW_0:58;
A7: pk . x = p . x by A4, A5, FUNCT_1:47;
then p . (p . x) = pk . (pk . x) by A4, A5, FUNCT_1:47
.= (pk * pk) . x by A5, FUNCT_1:13 ;
hence (pk * pk) . x = pk . x by A1, A7, A6, YELLOW_2:18; :: thesis: verum
end;
hence pk * pk = pk by FUNCT_2:63; :: thesis: pk is monotone
thus pk is monotone :: thesis: verum
proof
let x1, x2 be Element of (subrelstr Lk); :: according to WAYBEL_1:def 2 :: thesis: ( x1 <= x2 implies pk . x1 <= pk . x2 )
reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58;
assume x1 <= x2 ; :: thesis: pk . x1 <= pk . x2
then x19 <= x29 by YELLOW_0:59;
then A8: p . x19 <= p . x29 by A2;
( pk . x1 = p . x19 & pk . x2 = p . x29 ) by A4, A5, FUNCT_1:47;
hence pk . x1 <= pk . x2 by A8, YELLOW_0:60; :: thesis: verum
end;
end;
now :: thesis: for x being Element of (subrelstr Lk) holds pk . x <= (id (subrelstr Lk)) . x
let x be Element of (subrelstr Lk); :: thesis: pk . x <= (id (subrelstr Lk)) . x
reconsider x9 = x as Element of L by YELLOW_0:58;
x in the carrier of (subrelstr Lk) ;
then x in Lk by YELLOW_0:def 15;
then A9: ex c being Element of L st
( x = c & p . c <= c ) by A3;
pk . x = p . x9 by A4, A5, FUNCT_1:47;
then pk . x <= x by A9, YELLOW_0:60;
hence pk . x <= (id (subrelstr Lk)) . x ; :: thesis: verum
end;
hence pk <= id (subrelstr Lk) by YELLOW_2:9; :: thesis: verum