This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isoco

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

Ref Expression
Hypotheses isoco.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isoco.o ⊢ · = ( comp ‘ 𝐶 )
isoco.n ⊢ 𝐼 = ( Iso ‘ 𝐶 )
isoco.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
isoco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
isoco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
isoco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
isoco.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
isoco.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐼 𝑍 ) )
Assertion isoco ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐼 𝑍 ) )

Proof

Step Hyp Ref Expression
1 isoco.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isoco.o ⊢ · = ( comp ‘ 𝐶 )
3 isoco.n ⊢ 𝐼 = ( Iso ‘ 𝐶 )
4 isoco.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 isoco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 isoco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 isoco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8 isoco.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
9 isoco.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐼 𝑍 ) )
10 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
11 1 10 4 5 6 3 8 2 7 9 invco ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 ( Inv ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 ( Inv ‘ 𝐶 ) 𝑍 ) ‘ 𝐺 ) ) )
12 1 10 4 5 7 3 11 inviso1 ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ ( 𝑋 𝐼 𝑍 ) )