let P, R be non empty Poset; :: thesis: for Con being Connection of P,R st Con is co-Galois holds
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
let Con be Connection of P,R; :: thesis: ( Con is co-Galois implies for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) ) )
assume A1:
Con is co-Galois
; :: thesis: for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
let f be Function of P,R; :: thesis: for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
let g be Function of R,P; :: thesis: ( Con = [f,g] implies ( f = f * (g * f) & g = g * (f * g) ) )
assume A2:
Con = [f,g]
; :: thesis: ( f = f * (g * f) & g = g * (f * g) )
consider f' being Function of P,R, g' being Function of R,P such that
A3:
( Con = [f',g'] & f' is antitone & g' is antitone & ( for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g' . (f' . p1) & r1 <= f' . (g' . r1) ) ) )
by A1, Def10;
A4: f =
Con `1
by A2, MCART_1:def 1
.=
f'
by A3, MCART_1:def 1
;
A5: g =
Con `2
by A2, MCART_1:def 2
.=
g'
by A3, MCART_1:def 2
;
A6:
dom f = the carrier of P
by FUNCT_2:def 1;
A7:
dom g = the carrier of R
by FUNCT_2:def 1;
A8:
dom (f * (g * f)) = the carrier of P
by FUNCT_2:def 1;
A9:
for x being set st x in the carrier of P holds
f . x = (f * (g * f)) . x
proof
let x be
set ;
:: thesis: ( x in the carrier of P implies f . x = (f * (g * f)) . x )
assume
x in the
carrier of
P
;
:: thesis: f . x = (f * (g * f)) . x
then reconsider x =
x as
Element of
P ;
A10:
f . x is
Element of
R
;
A11:
f . x <= f . (g . (f . x))
by A3, A4, A5;
x <= g . (f . x)
by A3, A4, A5;
then
f . x >= f . (g . (f . x))
by A3, A4, WAYBEL_0:def 5;
then
f . x = f . (g . (f . x))
by A11, ORDERS_2:25;
then A12:
f . x = f . ((g * f) . x)
by A6, FUNCT_1:23;
x in dom (g * f)
by A6, A7, A10, FUNCT_1:21;
hence
f . x = (f * (g * f)) . x
by A12, FUNCT_1:23;
:: thesis: verum
end;
A13:
dom (g * (f * g)) = the carrier of R
by FUNCT_2:def 1;
for x being set st x in the carrier of R holds
g . x = (g * (f * g)) . x
proof
let x be
set ;
:: thesis: ( x in the carrier of R implies g . x = (g * (f * g)) . x )
assume
x in the
carrier of
R
;
:: thesis: g . x = (g * (f * g)) . x
then reconsider x =
x as
Element of
R ;
A14:
g . x is
Element of
P
;
A15:
g . x <= g . (f . (g . x))
by A3, A4, A5;
x <= f . (g . x)
by A3, A4, A5;
then
g . x >= g . (f . (g . x))
by A3, A5, WAYBEL_0:def 5;
then
g . x = g . (f . (g . x))
by A15, ORDERS_2:25;
then A16:
g . x = g . ((f * g) . x)
by A7, FUNCT_1:23;
x in dom (f * g)
by A6, A7, A14, FUNCT_1:21;
hence
g . x = (g * (f * g)) . x
by A16, FUNCT_1:23;
:: thesis: verum
end;
hence
( f = f * (g * f) & g = g * (f * g) )
by A6, A7, A8, A9, A13, FUNCT_1:9; :: thesis: verum