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	⊢ 𝐵 = ( Base ‘ 𝐶 )
	invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	invfval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	invfval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	isoval.n	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	invinv.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
	invco.o	⊢ · = ( comp ‘ 𝐶 )
	invco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	invco.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐼 𝑍 ) )
Assertion	invco	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑁 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
3		invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		invfval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		invfval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		isoval.n	⊢ 𝐼 = ( Iso ‘ 𝐶 )
7		invinv.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
8		invco.o	⊢ · = ( comp ‘ 𝐶 )
9		invco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
10		invco.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐼 𝑍 ) )
11		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
12	1 2 3 4 5 6	isoval	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 ) )
13	7 12	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑋 𝑁 𝑌 ) )
14	1 2 3 4 5	invfun	⊢ ( 𝜑 → Fun ( 𝑋 𝑁 𝑌 ) )
15		funfvbrb	⊢ ( Fun ( 𝑋 𝑁 𝑌 ) → ( 𝐹 ∈ dom ( 𝑋 𝑁 𝑌 ) ↔ 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) )
16	14 15	syl	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 𝑁 𝑌 ) ↔ 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) )
17	13 16	mpbid	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
18	1 2 3 4 5 11	isinv	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∧ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
19	17 18	mpbid	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∧ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) )
20	19	simpld	⊢ ( 𝜑 → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
21	1 2 3 5 9 6	isoval	⊢ ( 𝜑 → ( 𝑌 𝐼 𝑍 ) = dom ( 𝑌 𝑁 𝑍 ) )
22	10 21	eleqtrd	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑌 𝑁 𝑍 ) )
23	1 2 3 5 9	invfun	⊢ ( 𝜑 → Fun ( 𝑌 𝑁 𝑍 ) )
24		funfvbrb	⊢ ( Fun ( 𝑌 𝑁 𝑍 ) → ( 𝐺 ∈ dom ( 𝑌 𝑁 𝑍 ) ↔ 𝐺 ( 𝑌 𝑁 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )
25	23 24	syl	⊢ ( 𝜑 → ( 𝐺 ∈ dom ( 𝑌 𝑁 𝑍 ) ↔ 𝐺 ( 𝑌 𝑁 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )
26	22 25	mpbid	⊢ ( 𝜑 → 𝐺 ( 𝑌 𝑁 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) )
27	1 2 3 5 9 11	isinv	⊢ ( 𝜑 → ( 𝐺 ( 𝑌 𝑁 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ↔ ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ∧ ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ) ) )
28	26 27	mpbid	⊢ ( 𝜑 → ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ∧ ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ) )
29	28	simpld	⊢ ( 𝜑 → 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) )
30	1 8 11 3 4 5 9 20 29	sectco	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )
31	28	simprd	⊢ ( 𝜑 → ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 )
32	19	simprd	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
33	1 8 11 3 9 5 4 31 32	sectco	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑋 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
34	1 2 3 4 9 11	isinv	⊢ ( 𝜑 → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑁 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) ↔ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) ∧ ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑋 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
35	30 33 34	mpbir2and	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑁 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )