let S, T be non empty Poset; :: thesis: for g being Function of S,T

for d being Function of T,S st g is onto & [g,d] is Galois holds

T, Image d are_isomorphic

let g be Function of S,T; :: thesis: for d being Function of T,S st g is onto & [g,d] is Galois holds

T, Image d are_isomorphic

let d be Function of T,S; :: thesis: ( g is onto & [g,d] is Galois implies T, Image d are_isomorphic )

assume that

A1: g is onto and

A2: [g,d] is Galois ; :: thesis: T, Image d are_isomorphic

d is V13() by A1, A2, WAYBEL_1:24;

then A3: the carrier of (Image d) |` d is one-to-one by FUNCT_1:58;

A4: d is monotone by A2, WAYBEL_1:8;

then corestr d is isomorphic by A3, A5, WAYBEL_0:66;

hence T, Image d are_isomorphic ; :: thesis: verum

for d being Function of T,S st g is onto & [g,d] is Galois holds

T, Image d are_isomorphic

let g be Function of S,T; :: thesis: for d being Function of T,S st g is onto & [g,d] is Galois holds

T, Image d are_isomorphic

let d be Function of T,S; :: thesis: ( g is onto & [g,d] is Galois implies T, Image d are_isomorphic )

assume that

A1: g is onto and

A2: [g,d] is Galois ; :: thesis: T, Image d are_isomorphic

d is V13() by A1, A2, WAYBEL_1:24;

then A3: the carrier of (Image d) |` d is one-to-one by FUNCT_1:58;

A4: d is monotone by A2, WAYBEL_1:8;

A5: now :: thesis: for x, y being Element of T holds

( ( x <= y implies (corestr d) . x <= (corestr d) . y ) & ( (corestr d) . x <= (corestr d) . y implies x <= y ) )

rng (corestr d) = the carrier of (Image d)
by FUNCT_2:def 3;( ( x <= y implies (corestr d) . x <= (corestr d) . y ) & ( (corestr d) . x <= (corestr d) . y implies x <= y ) )

let x, y be Element of T; :: thesis: ( ( x <= y implies (corestr d) . x <= (corestr d) . y ) & ( (corestr d) . x <= (corestr d) . y implies x <= y ) )

thus ( x <= y implies (corestr d) . x <= (corestr d) . y ) by A4, WAYBEL_1:def 2; :: thesis: ( (corestr d) . x <= (corestr d) . y implies x <= y )

thus ( (corestr d) . x <= (corestr d) . y implies x <= y ) :: thesis: verum

end;thus ( x <= y implies (corestr d) . x <= (corestr d) . y ) by A4, WAYBEL_1:def 2; :: thesis: ( (corestr d) . x <= (corestr d) . y implies x <= y )

thus ( (corestr d) . x <= (corestr d) . y implies x <= y ) :: thesis: verum

proof

for t being Element of T holds d . t is_minimum_of g " {t}
by A1, A2, WAYBEL_1:22;

then A6: g * d = id T by WAYBEL_1:23;

assume A7: (corestr d) . x <= (corestr d) . y ; :: thesis: x <= y

y in the carrier of T ;

then A8: y in dom d by FUNCT_2:def 1;

A9: g is monotone by A2, WAYBEL_1:8;

( d . x = (corestr d) . x & d . y = (corestr d) . y ) by WAYBEL_1:30;

then d . x <= d . y by A7, YELLOW_0:59;

then A10: g . (d . x) <= g . (d . y) by A9;

x in the carrier of T ;

then x in dom d by FUNCT_2:def 1;

then (g * d) . x <= g . (d . y) by A10, FUNCT_1:13;

then (g * d) . x <= (g * d) . y by A8, FUNCT_1:13;

then (id T) . x <= y by A6;

hence x <= y ; :: thesis: verum

end;then A6: g * d = id T by WAYBEL_1:23;

assume A7: (corestr d) . x <= (corestr d) . y ; :: thesis: x <= y

y in the carrier of T ;

then A8: y in dom d by FUNCT_2:def 1;

A9: g is monotone by A2, WAYBEL_1:8;

( d . x = (corestr d) . x & d . y = (corestr d) . y ) by WAYBEL_1:30;

then d . x <= d . y by A7, YELLOW_0:59;

then A10: g . (d . x) <= g . (d . y) by A9;

x in the carrier of T ;

then x in dom d by FUNCT_2:def 1;

then (g * d) . x <= g . (d . y) by A10, FUNCT_1:13;

then (g * d) . x <= (g * d) . y by A8, FUNCT_1:13;

then (id T) . x <= y by A6;

hence x <= y ; :: thesis: verum

then corestr d is isomorphic by A3, A5, WAYBEL_0:66;

hence T, Image d are_isomorphic ; :: thesis: verum