let T, S be non empty Poset; for f being monotone Function of T,S
for g being monotone Function of S,T st f * g = id S holds
ex h being projection Function of T,T st
( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
let f be monotone Function of T,S; for g being monotone Function of S,T st f * g = id S holds
ex h being projection Function of T,T st
( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
let g be monotone Function of S,T; ( f * g = id S implies ex h being projection Function of T,T st
( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic ) )
assume A1:
f * g = id S
; ex h being projection Function of T,T st
( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
set h = g * f;
(g * f) * (g * f) =
((g * f) * g) * f
by RELAT_1:36
.=
(g * (id S)) * f
by A1, RELAT_1:36
.=
g * f
by FUNCT_2:17
;
then
g * f is idempotent monotone Function of T,T
by QUANTAL1:def 9, YELLOW_2:12;
then reconsider h = g * f as projection Function of T,T by WAYBEL_1:def 13;
A2:
dom g = the carrier of S
by FUNCT_2:def 1;
f is onto
by A1, FUNCT_2:23;
then A3:
rng f = the carrier of S
by FUNCT_2:def 3;
then reconsider gg = corestr g as Function of S,(Image h) by A2, RELAT_1:28;
A4:
gg = g
by WAYBEL_1:30;
A5:
now for x, y being Element of S holds
( ( x <= y implies gg . x <= gg . y ) & ( gg . x <= gg . y implies x <= y ) )end;
rng h = rng g
by A3, A2, RELAT_1:28;
then A8:
rng gg = the carrier of (Image h)
by A4, YELLOW_0:def 15;
take
h
; ( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
thus
h = g * f
; ( h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
thus h | the carrier of (Image h) =
h * (inclusion h)
by RELAT_1:65
.=
(corestr h) * (inclusion h)
by WAYBEL_1:30
.=
id (Image h)
by WAYBEL_1:33
; S, Image h are_isomorphic
take
gg
; WAYBEL_1:def 8 gg is isomorphic
gg is V7()
by A1, A4, FUNCT_2:23;
hence
gg is isomorphic
by A8, A5, WAYBEL_0:66; verum