let C be Category; :: thesis: for a, b being Object of C

for f being Morphism of a,b holds

( f opp is invertible iff f is invertible )

let a, b be Object of C; :: thesis: for f being Morphism of a,b holds

( f opp is invertible iff f is invertible )

let f be Morphism of a,b; :: thesis: ( f opp is invertible iff f is invertible )

thus ( f opp is invertible implies f is invertible ) :: thesis: ( f is invertible implies f opp is invertible )_{1} being Morphism of b,a holds

( not f * b_{1} = id b or not b_{1} * f = id a ) or f opp is invertible )

given g being Morphism of b,a such that A6: ( f * g = id b & g * f = id a ) ; :: thesis: f opp is invertible

thus ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) by A5, Th4; :: according to CAT_1:def 16 :: thesis: ex b_{1} being Morphism of a opp ,b opp st

( (f opp) * b_{1} = id (a opp) & b_{1} * (f opp) = id (b opp) )

take g opp ; :: thesis: ( (f opp) * (g opp) = id (a opp) & (g opp) * (f opp) = id (b opp) )

thus (f opp) * (g opp) = g * f by A5, Lm3

.= id (a opp) by A6, Lm2 ; :: thesis: (g opp) * (f opp) = id (b opp)

thus (g opp) * (f opp) = f * g by A5, Lm3

.= id (b opp) by A6, Lm2 ; :: thesis: verum

for f being Morphism of a,b holds

( f opp is invertible iff f is invertible )

let a, b be Object of C; :: thesis: for f being Morphism of a,b holds

( f opp is invertible iff f is invertible )

let f be Morphism of a,b; :: thesis: ( f opp is invertible iff f is invertible )

thus ( f opp is invertible implies f is invertible ) :: thesis: ( f is invertible implies f opp is invertible )

proof

assume A5:
( Hom (a,b) <> {} & Hom (b,a) <> {} )
; :: according to CAT_1:def 16 :: thesis: ( for b
assume A1:
( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} )
; :: according to CAT_1:def 16 :: thesis: ( for b_{1} being Morphism of a opp ,b opp holds

( not (f opp) * b_{1} = id (a opp) or not b_{1} * (f opp) = id (b opp) ) or f is invertible )

given gg being Morphism of a opp ,b opp such that A2: ( (f opp) * gg = id (a opp) & gg * (f opp) = id (b opp) ) ; :: thesis: f is invertible

thus A3: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, Th4; :: according to CAT_1:def 16 :: thesis: ex b_{1} being Morphism of b,a st

( f * b_{1} = id b & b_{1} * f = id a )

reconsider g = opp gg as Morphism of b,a ;

take g ; :: thesis: ( f * g = id b & g * f = id a )

A4: g opp = g by Def6, A3

.= gg by Def7, A1 ;

thus f * g = (g opp) * (f opp) by A3, Lm3

.= id (b opp) by A2, A4

.= id b by Lm2 ; :: thesis: g * f = id a

thus g * f = (f opp) * (g opp) by A3, Lm3

.= id a by A2, A4, Lm2 ; :: thesis: verum

end;( not (f opp) * b

given gg being Morphism of a opp ,b opp such that A2: ( (f opp) * gg = id (a opp) & gg * (f opp) = id (b opp) ) ; :: thesis: f is invertible

thus A3: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, Th4; :: according to CAT_1:def 16 :: thesis: ex b

( f * b

reconsider g = opp gg as Morphism of b,a ;

take g ; :: thesis: ( f * g = id b & g * f = id a )

A4: g opp = g by Def6, A3

.= gg by Def7, A1 ;

thus f * g = (g opp) * (f opp) by A3, Lm3

.= id (b opp) by A2, A4

.= id b by Lm2 ; :: thesis: g * f = id a

thus g * f = (f opp) * (g opp) by A3, Lm3

.= id a by A2, A4, Lm2 ; :: thesis: verum

( not f * b

given g being Morphism of b,a such that A6: ( f * g = id b & g * f = id a ) ; :: thesis: f opp is invertible

thus ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) by A5, Th4; :: according to CAT_1:def 16 :: thesis: ex b

( (f opp) * b

take g opp ; :: thesis: ( (f opp) * (g opp) = id (a opp) & (g opp) * (f opp) = id (b opp) )

thus (f opp) * (g opp) = g * f by A5, Lm3

.= id (a opp) by A6, Lm2 ; :: thesis: (g opp) * (f opp) = id (b opp)

thus (g opp) * (f opp) = f * g by A5, Lm3

.= id (b opp) by A6, Lm2 ; :: thesis: verum