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	$⊢ φ \to C \in Cat$
	invfval.x	$⊢ φ \to X \in B$
	invfval.y	$⊢ φ \to Y \in B$
	isoval.n	$⊢ I = Iso (C)$
	invinv.f	$⊢ φ \to F \in (X I Y)$
	invco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	invco.z	$⊢ φ \to Z \in B$
	invco.f	$⊢ φ \to G \in (Y I Z)$
Assertion	invco	$⊢ φ \to (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (X N Z) ((X N Y) (F) (⟨Z, Y⟩ \underset{˙}{\cdot} 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	$⊢ φ \to C \in Cat$
4		invfval.x	$⊢ φ \to X \in B$
5		invfval.y	$⊢ φ \to Y \in B$
6		isoval.n	$⊢ I = Iso (C)$
7		invinv.f	$⊢ φ \to F \in (X I Y)$
8		invco.o	$⊢ \underset{˙}{\cdot} = comp (C)$
9		invco.z	$⊢ φ \to Z \in B$
10		invco.f	$⊢ φ \to G \in (Y I Z)$
11		eqid	$⊢ Sect (C) = Sect (C)$
12	1 2 3 4 5 6	isoval	$⊢ φ \to X I Y = dom (X N Y)$
13	7 12	eleqtrd	$⊢ φ \to F \in dom (X N Y)$
14	1 2 3 4 5	invfun	$⊢ φ \to Fun (X N Y)$
15		funfvbrb	$⊢ Fun (X N Y) \to (F \in dom (X N Y) \leftrightarrow F (X N Y) (X N Y) (F))$
16	14 15	syl	$⊢ φ \to (F \in dom (X N Y) \leftrightarrow F (X N Y) (X N Y) (F))$
17	13 16	mpbid	$⊢ φ \to F (X N Y) (X N Y) (F)$
18	1 2 3 4 5 11	isinv	$⊢ φ \to (F (X N Y) (X N Y) (F) \leftrightarrow (F (X Sect (C) Y) (X N Y) (F) \land (X N Y) (F) (Y Sect (C) X) F))$
19	17 18	mpbid	$⊢ φ \to (F (X Sect (C) Y) (X N Y) (F) \land (X N Y) (F) (Y Sect (C) X) F)$
20	19	simpld	$⊢ φ \to F (X Sect (C) Y) (X N Y) (F)$
21	1 2 3 5 9 6	isoval	$⊢ φ \to Y I Z = dom (Y N Z)$
22	10 21	eleqtrd	$⊢ φ \to G \in dom (Y N Z)$
23	1 2 3 5 9	invfun	$⊢ φ \to Fun (Y N Z)$
24		funfvbrb	$⊢ Fun (Y N Z) \to (G \in dom (Y N Z) \leftrightarrow G (Y N Z) (Y N Z) (G))$
25	23 24	syl	$⊢ φ \to (G \in dom (Y N Z) \leftrightarrow G (Y N Z) (Y N Z) (G))$
26	22 25	mpbid	$⊢ φ \to G (Y N Z) (Y N Z) (G)$
27	1 2 3 5 9 11	isinv	$⊢ φ \to (G (Y N Z) (Y N Z) (G) \leftrightarrow (G (Y Sect (C) Z) (Y N Z) (G) \land (Y N Z) (G) (Z Sect (C) Y) G))$
28	26 27	mpbid	$⊢ φ \to (G (Y Sect (C) Z) (Y N Z) (G) \land (Y N Z) (G) (Z Sect (C) Y) G)$
29	28	simpld	$⊢ φ \to G (Y Sect (C) Z) (Y N Z) (G)$
30	1 8 11 3 4 5 9 20 29	sectco	$⊢ φ \to (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (X Sect (C) Z) ((X N Y) (F) (⟨Z, Y⟩ \underset{˙}{\cdot} X) (Y N Z) (G))$
31	28	simprd	$⊢ φ \to (Y N Z) (G) (Z Sect (C) Y) G$
32	19	simprd	$⊢ φ \to (X N Y) (F) (Y Sect (C) X) F$
33	1 8 11 3 9 5 4 31 32	sectco	$⊢ φ \to ((X N Y) (F) (⟨Z, Y⟩ \underset{˙}{\cdot} X) (Y N Z) (G)) (Z Sect (C) X) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F)$
34	1 2 3 4 9 11	isinv	$⊢ φ \to ((G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (X N Z) ((X N Y) (F) (⟨Z, Y⟩ \underset{˙}{\cdot} X) (Y N Z) (G)) \leftrightarrow ((G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (X Sect (C) Z) ((X N Y) (F) (⟨Z, Y⟩ \underset{˙}{\cdot} X) (Y N Z) (G)) \land ((X N Y) (F) (⟨Z, Y⟩ \underset{˙}{\cdot} X) (Y N Z) (G)) (Z Sect (C) X) (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F)))$
35	30 33 34	mpbir2and	$⊢ φ \to (G (⟨X, Y⟩ \underset{˙}{\cdot} Z) F) (X N Z) ((X N Y) (F) (⟨Z, Y⟩ \underset{˙}{\cdot} X) (Y N Z) (G))$

Metamath Proof Explorer

Theorem invco

Proof