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

Metamath Proof Explorer

Theorem comfeqd

Description: Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfeqd.1 ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐷 ) )
comfeqd.2 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
Assertion comfeqd ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 comfeqd.1 ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐷 ) )
2 comfeqd.2 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
3 1 oveqd ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) )
4 3 oveqd ⊢ ( 𝜑 → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) )
5 4 ralrimivw ⊢ ( 𝜑 → ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) )
6 5 ralrimivw ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) )
7 6 ralrimivw ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) )
8 7 ralrimivw ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) )
9 8 ralrimivw ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) )
10 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
12 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
13 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) )
14 2 homfeqbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
15 10 11 12 13 14 2 comfeq ⊢ ( 𝜑 → ( ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) ) )
16 9 15 mpbird ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )