let S, T be non empty Poset; :: thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois & g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}
let g be Function of S,T; :: thesis: for d being Function of T,S st [g,d] is Galois & g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}
let d be Function of T,S; :: thesis: ( [g,d] is Galois & g is onto implies for t being Element of T holds d . t is_minimum_of g " {t} )
assume that
A1: [g,d] is Galois and
A2: g is onto ; :: thesis: for t being Element of T holds d . t is_minimum_of g " {t}
A3: g is monotone by A1, Th8;
let t be Element of T; :: thesis: d . t is_minimum_of g " {t}
A4: rng g = the carrier of T by A2, FUNCT_2:def 3;
then A5: g .: (g " (uparrow t)) = uparrow t by FUNCT_1:77;
A6: d . t is_minimum_of g " (uparrow t) by A1, Th10;
then A7: d . t = inf (g " (uparrow t)) ;
d . t in g " (uparrow t) by A6;
then g . (d . t) in g .: (g " (uparrow t)) by FUNCT_2:35;
then A8: t <= g . (d . t) by A5, WAYBEL_0:18;
ex_inf_of g " (uparrow t),S by A6;
then A9: d . t is_<=_than g " (uparrow t) by A7, YELLOW_0:31;
consider s being object such that
A10: s in the carrier of S and
A11: g . s = t by A4, FUNCT_2:11;
reconsider s = s as Element of S by A10;
A12: t in {t} by TARSKI:def 1;
A13: {t} c= uparrow {t} by WAYBEL_0:16;
then s in g " (uparrow t) by A11, A12, FUNCT_2:38;
then d . t <= s by A9;
then g . (d . t) <= t by A11, A3;
then A14: g . (d . t) = t by A8, ORDERS_2:2;
then A15: d . t in g " {t} by A12, FUNCT_2:38;
A16: g " {t} c= g " (uparrow t) by RELAT_1:143, WAYBEL_0:16;
thus A17: ex_inf_of g " {t},S :: according to WAYBEL_1:def 6 :: thesis: ( d . t = "/\" ((g " {t}),S) & "/\" ((g " {t}),S) in g " {t} )
proof
take d . t ; :: according to YELLOW_0:def 8 :: thesis: ( d . t is_<=_than g " {t} & ( for b1 being M3( the carrier of S) holds
( not b1 is_<=_than g " {t} or b1 <= d . t ) ) & ( for b1 being M3( the carrier of S) holds
( not b1 is_<=_than g " {t} or ex b2 being M3( the carrier of S) st
( b2 is_<=_than g " {t} & not b2 <= b1 ) or b1 = d . t ) ) )
thus g " {t} is_>=_than d . t by A9, A16; :: thesis: ( ( for b1 being M3( the carrier of S) holds
( not b1 is_<=_than g " {t} or b1 <= d . t ) ) & ( for b1 being M3( the carrier of S) holds
( not b1 is_<=_than g " {t} or ex b2 being M3( the carrier of S) st
( b2 is_<=_than g " {t} & not b2 <= b1 ) or b1 = d . t ) ) )
thus for b being Element of S st g " {t} is_>=_than b holds
b <= d . t by A15; :: thesis: for b1 being M3( the carrier of S) holds
( not b1 is_<=_than g " {t} or ex b2 being M3( the carrier of S) st
( b2 is_<=_than g " {t} & not b2 <= b1 ) or b1 = d . t )
let c be Element of S; :: thesis: ( not c is_<=_than g " {t} or ex b1 being M3( the carrier of S) st
( b1 is_<=_than g " {t} & not b1 <= c ) or c = d . t )
assume g " {t} is_>=_than c ; :: thesis: ( ex b1 being M3( the carrier of S) st
( b1 is_<=_than g " {t} & not b1 <= c ) or c = d . t )
then A18: c <= d . t by A15;
assume for b being Element of S st g " {t} is_>=_than b holds
b <= c ; :: thesis: c = d . t
then d . t <= c by A9, A16, YELLOW_0:9;
hence c = d . t by A18, ORDERS_2:2; :: thesis: verum
end;
then inf (g " {t}) is_<=_than g " {t} by YELLOW_0:31;
then A19: inf (g " {t}) <= d . t by A15;
ex_inf_of g " (uparrow t),S by A6;
then inf (g " {t}) >= d . t by A7, A13, A17, RELAT_1:143, YELLOW_0:35;
hence d . t = inf (g " {t}) by A19, ORDERS_2:2; :: thesis: "/\" ((g " {t}),S) in g " {t}
hence "/\" ((g " {t}),S) in g " {t} by A12, A14, FUNCT_2:38; :: thesis: verum