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

Metamath Proof Explorer

Theorem oppcco

Description: Composition in the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses oppcco.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
oppcco.c ⊢ · = ( comp ‘ 𝐶 )
oppcco.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
oppcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
oppcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
oppcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion oppcco ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑍 ) 𝐹 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 oppcco.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 oppcco.c ⊢ · = ( comp ‘ 𝐶 )
3 oppcco.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
4 oppcco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 oppcco.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 oppcco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7 1 2 3 4 5 6 oppccofval ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑍 ) = tpos ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) )
8 7 oveqd ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑍 ) 𝐹 ) = ( 𝐺 tpos ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) )
9 ovtpos ⊢ ( 𝐺 tpos ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐹 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐺 )
10 8 9 eqtrdi ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑂 ) 𝑍 ) 𝐹 ) = ( 𝐹 ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) 𝐺 ) )