Metamath Proof Explorer

Theorem invco

Description: The composition of two isomorphisms is an isomorphism, and the inverse is the composition of the individual inverses. Proposition 3.14(2) of Adamek p. 29. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses invfval.b 
|- B = ( Base ` C )
invfval.n 
|- N = ( Inv ` C )
invfval.c 
|- ( ph -> C e. Cat )
invfval.x 
|- ( ph -> X e. B )
invfval.y 
|- ( ph -> Y e. B )
isoval.n 
|- I = ( Iso ` C )
invinv.f 
|- ( ph -> F e. ( X I Y ) )
invco.o 
|- .x. = ( comp ` C )
invco.z 
|- ( ph -> Z e. B )
invco.f 
|- ( ph -> G e. ( Y I Z ) )
Assertion invco 
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) ( X N Z ) ( ( ( X N Y ) ` F ) ( <. Z , Y >. .x. X ) ( ( Y N Z ) ` G ) ) )

Proof

Step Hyp Ref Expression
1 invfval.b 
 |-  B = ( Base ` C )
2 invfval.n 
 |-  N = ( Inv ` C )
3 invfval.c 
 |-  ( ph -> C e. Cat )
4 invfval.x 
 |-  ( ph -> X e. B )
5 invfval.y 
 |-  ( ph -> Y e. B )
6 isoval.n 
 |-  I = ( Iso ` C )
7 invinv.f 
 |-  ( ph -> F e. ( X I Y ) )
8 invco.o 
 |-  .x. = ( comp ` C )
9 invco.z 
 |-  ( ph -> Z e. B )
10 invco.f 
 |-  ( ph -> G e. ( Y I Z ) )
11 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
12 1 2 3 4 5 6 isoval 
 |-  ( ph -> ( X I Y ) = dom ( X N Y ) )
13 7 12 eleqtrd 
 |-  ( ph -> F e. dom ( X N Y ) )
14 1 2 3 4 5 invfun 
 |-  ( ph -> Fun ( X N Y ) )
15 funfvbrb 
 |-  ( Fun ( X N Y ) -> ( F e. dom ( X N Y ) <-> F ( X N Y ) ( ( X N Y ) ` F ) ) )
16 14 15 syl 
 |-  ( ph -> ( F e. dom ( X N Y ) <-> F ( X N Y ) ( ( X N Y ) ` F ) ) )
17 13 16 mpbid 
 |-  ( ph -> F ( X N Y ) ( ( X N Y ) ` F ) )
18 1 2 3 4 5 11 isinv 
 |-  ( ph -> ( F ( X N Y ) ( ( X N Y ) ` F ) <-> ( F ( X ( Sect ` C ) Y ) ( ( X N Y ) ` F ) /\ ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F ) ) )
19 17 18 mpbid 
 |-  ( ph -> ( F ( X ( Sect ` C ) Y ) ( ( X N Y ) ` F ) /\ ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F ) )
20 19 simpld 
 |-  ( ph -> F ( X ( Sect ` C ) Y ) ( ( X N Y ) ` F ) )
21 1 2 3 5 9 6 isoval 
 |-  ( ph -> ( Y I Z ) = dom ( Y N Z ) )
22 10 21 eleqtrd 
 |-  ( ph -> G e. dom ( Y N Z ) )
23 1 2 3 5 9 invfun 
 |-  ( ph -> Fun ( Y N Z ) )
24 funfvbrb 
 |-  ( Fun ( Y N Z ) -> ( G e. dom ( Y N Z ) <-> G ( Y N Z ) ( ( Y N Z ) ` G ) ) )
25 23 24 syl 
 |-  ( ph -> ( G e. dom ( Y N Z ) <-> G ( Y N Z ) ( ( Y N Z ) ` G ) ) )
26 22 25 mpbid 
 |-  ( ph -> G ( Y N Z ) ( ( Y N Z ) ` G ) )
27 1 2 3 5 9 11 isinv 
 |-  ( ph -> ( G ( Y N Z ) ( ( Y N Z ) ` G ) <-> ( G ( Y ( Sect ` C ) Z ) ( ( Y N Z ) ` G ) /\ ( ( Y N Z ) ` G ) ( Z ( Sect ` C ) Y ) G ) ) )
28 26 27 mpbid 
 |-  ( ph -> ( G ( Y ( Sect ` C ) Z ) ( ( Y N Z ) ` G ) /\ ( ( Y N Z ) ` G ) ( Z ( Sect ` C ) Y ) G ) )
29 28 simpld 
 |-  ( ph -> G ( Y ( Sect ` C ) Z ) ( ( Y N Z ) ` G ) )
30 1 8 11 3 4 5 9 20 29 sectco 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) ( X ( Sect ` C ) Z ) ( ( ( X N Y ) ` F ) ( <. Z , Y >. .x. X ) ( ( Y N Z ) ` G ) ) )
31 28 simprd 
 |-  ( ph -> ( ( Y N Z ) ` G ) ( Z ( Sect ` C ) Y ) G )
32 19 simprd 
 |-  ( ph -> ( ( X N Y ) ` F ) ( Y ( Sect ` C ) X ) F )
33 1 8 11 3 9 5 4 31 32 sectco 
 |-  ( ph -> ( ( ( X N Y ) ` F ) ( <. Z , Y >. .x. X ) ( ( Y N Z ) ` G ) ) ( Z ( Sect ` C ) X ) ( G ( <. X , Y >. .x. Z ) F ) )
34 1 2 3 4 9 11 isinv 
 |-  ( ph -> ( ( G ( <. X , Y >. .x. Z ) F ) ( X N Z ) ( ( ( X N Y ) ` F ) ( <. Z , Y >. .x. X ) ( ( Y N Z ) ` G ) ) <-> ( ( G ( <. X , Y >. .x. Z ) F ) ( X ( Sect ` C ) Z ) ( ( ( X N Y ) ` F ) ( <. Z , Y >. .x. X ) ( ( Y N Z ) ` G ) ) /\ ( ( ( X N Y ) ` F ) ( <. Z , Y >. .x. X ) ( ( Y N Z ) ` G ) ) ( Z ( Sect ` C ) X ) ( G ( <. X , Y >. .x. Z ) F ) ) ) )
35 30 33 34 mpbir2and 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) ( X N Z ) ( ( ( X N Y ) ` F ) ( <. Z , Y >. .x. X ) ( ( Y N Z ) ` G ) ) )