Metamath Proof Explorer

Theorem isocoinvid

Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-Apr-2020)

Ref Expression
Hypotheses invisoinv.b 
|- B = ( Base ` C )
invisoinv.i 
|- I = ( Iso ` C )
invisoinv.n 
|- N = ( Inv ` C )
invisoinv.c 
|- ( ph -> C e. Cat )
invisoinv.x 
|- ( ph -> X e. B )
invisoinv.y 
|- ( ph -> Y e. B )
invisoinv.f 
|- ( ph -> F e. ( X I Y ) )
invcoisoid.1 
|- .1. = ( Id ` C )
isocoinvid.o 
|- .o. = ( <. Y , X >. ( comp ` C ) Y )
Assertion isocoinvid 
|- ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) )

Proof

Step Hyp Ref Expression
1 invisoinv.b 
 |-  B = ( Base ` C )
2 invisoinv.i 
 |-  I = ( Iso ` C )
3 invisoinv.n 
 |-  N = ( Inv ` C )
4 invisoinv.c 
 |-  ( ph -> C e. Cat )
5 invisoinv.x 
 |-  ( ph -> X e. B )
6 invisoinv.y 
 |-  ( ph -> Y e. B )
7 invisoinv.f 
 |-  ( ph -> F e. ( X I Y ) )
8 invcoisoid.1 
 |-  .1. = ( Id ` C )
9 isocoinvid.o 
 |-  .o. = ( <. Y , X >. ( comp ` C ) Y )
10 1 2 3 4 5 6 7 invisoinvl 
 |-  ( ph -> ( ( X N Y ) ` F ) ( Y N X ) F )
11 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
12 1 3 4 6 5 11 isinv 
 |-  ( ph -> ( ( ( X N Y ) ` F ) ( Y N X ) F <-> ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) ( ( X N Y ) ` F ) ) ) )
13 simpl 
 |-  ( ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) ( ( X N Y ) ` F ) ) -> ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F )
14 12 13 syl6bi 
 |-  ( ph -> ( ( ( X N Y ) ` F ) ( Y N X ) F -> ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F ) )
15 10 14 mpd 
 |-  ( ph -> ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F )
16 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
17 eqid 
 |-  ( comp ` C ) = ( comp ` C )
18 1 16 2 4 6 5 isohom 
 |-  ( ph -> ( Y I X ) C_ ( Y ( Hom ` C ) X ) )
19 1 3 4 5 6 2 invf 
 |-  ( ph -> ( X N Y ) : ( X I Y ) --> ( Y I X ) )
20 19 7 ffvelrnd 
 |-  ( ph -> ( ( X N Y ) ` F ) e. ( Y I X ) )
21 18 20 sseldd 
 |-  ( ph -> ( ( X N Y ) ` F ) e. ( Y ( Hom ` C ) X ) )
22 1 16 2 4 5 6 isohom 
 |-  ( ph -> ( X I Y ) C_ ( X ( Hom ` C ) Y ) )
23 22 7 sseldd 
 |-  ( ph -> F e. ( X ( Hom ` C ) Y ) )
24 1 16 17 8 11 4 6 5 21 23 issect2 
 |-  ( ph -> ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F <-> ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) )
25 9 a1i 
 |-  ( ph -> .o. = ( <. Y , X >. ( comp ` C ) Y ) )
26 25 eqcomd 
 |-  ( ph -> ( <. Y , X >. ( comp ` C ) Y ) = .o. )
27 26 oveqd 
 |-  ( ph -> ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( F .o. ( ( X N Y ) ` F ) ) )
28 27 eqeq1d 
 |-  ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) ( ( X N Y ) ` F ) ) = ( .1. ` Y ) <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) )
29 24 28 bitrd 
 |-  ( ph -> ( ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F <-> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) ) )
30 15 29 mpbid 
 |-  ( ph -> ( F .o. ( ( X N Y ) ` F ) ) = ( .1. ` Y ) )