# 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 ${⊢}{\phi }\to \mathrm{comp}\left({C}\right)=\mathrm{comp}\left({D}\right)$
comfeqd.2 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
Assertion comfeqd ${⊢}{\phi }\to {\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$

### Proof

Step Hyp Ref Expression
1 comfeqd.1 ${⊢}{\phi }\to \mathrm{comp}\left({C}\right)=\mathrm{comp}\left({D}\right)$
2 comfeqd.2 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
3 1 oveqd ${⊢}{\phi }\to ⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}=⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}$
4 3 oveqd ${⊢}{\phi }\to {g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}={g}\left(⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}\right){f}$
5 4 ralrimivw ${⊢}{\phi }\to \forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}={g}\left(⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}\right){f}$
6 5 ralrimivw ${⊢}{\phi }\to \forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}={g}\left(⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}\right){f}$
7 6 ralrimivw ${⊢}{\phi }\to \forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}={g}\left(⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}\right){f}$
8 7 ralrimivw ${⊢}{\phi }\to \forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}={g}\left(⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}\right){f}$
9 8 ralrimivw ${⊢}{\phi }\to \forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}={g}\left(⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}\right){f}$
10 eqid ${⊢}\mathrm{comp}\left({C}\right)=\mathrm{comp}\left({C}\right)$
11 eqid ${⊢}\mathrm{comp}\left({D}\right)=\mathrm{comp}\left({D}\right)$
12 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
13 eqidd ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
14 2 homfeqbas ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{D}}$
15 10 11 12 13 14 2 comfeq ${⊢}{\phi }\to \left({\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)↔\forall {x}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{C}}\phantom{\rule{.4em}{0ex}}\forall {f}\in \left({x}\mathrm{Hom}\left({C}\right){y}\right)\phantom{\rule{.4em}{0ex}}\forall {g}\in \left({y}\mathrm{Hom}\left({C}\right){z}\right)\phantom{\rule{.4em}{0ex}}{g}\left(⟨{x},{y}⟩\mathrm{comp}\left({C}\right){z}\right){f}={g}\left(⟨{x},{y}⟩\mathrm{comp}\left({D}\right){z}\right){f}\right)$
16 9 15 mpbird ${⊢}{\phi }\to {\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$