# Metamath Proof Explorer

## Theorem comfeqval

Description: Equality of two compositions. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfeqval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
comfeqval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
comfeqval.1
comfeqval.2
comfeqval.3 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
comfeqval.4 ${⊢}{\phi }\to {\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$
comfeqval.x ${⊢}{\phi }\to {X}\in {B}$
comfeqval.y ${⊢}{\phi }\to {Y}\in {B}$
comfeqval.z ${⊢}{\phi }\to {Z}\in {B}$
comfeqval.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
comfeqval.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{Z}\right)$
Assertion comfeqval

### Proof

Step Hyp Ref Expression
1 comfeqval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 comfeqval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 comfeqval.1
4 comfeqval.2
5 comfeqval.3 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
6 comfeqval.4 ${⊢}{\phi }\to {\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$
7 comfeqval.x ${⊢}{\phi }\to {X}\in {B}$
8 comfeqval.y ${⊢}{\phi }\to {Y}\in {B}$
9 comfeqval.z ${⊢}{\phi }\to {Z}\in {B}$
10 comfeqval.f ${⊢}{\phi }\to {F}\in \left({X}{H}{Y}\right)$
11 comfeqval.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{Z}\right)$
12 6 oveqd ${⊢}{\phi }\to ⟨{X},{Y}⟩{\mathrm{comp}}_{𝑓}\left({C}\right){Z}=⟨{X},{Y}⟩{\mathrm{comp}}_{𝑓}\left({D}\right){Z}$
13 12 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}$
14 eqid ${⊢}{\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({C}\right)$
15 14 1 2 3 7 8 9 10 11 comfval
16 eqid ${⊢}{\mathrm{comp}}_{𝑓}\left({D}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$
17 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
18 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
19 5 homfeqbas ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{D}}$
20 1 19 syl5eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{D}}$
21 7 20 eleqtrd ${⊢}{\phi }\to {X}\in {\mathrm{Base}}_{{D}}$
22 8 20 eleqtrd ${⊢}{\phi }\to {Y}\in {\mathrm{Base}}_{{D}}$
23 9 20 eleqtrd ${⊢}{\phi }\to {Z}\in {\mathrm{Base}}_{{D}}$
24 1 2 18 5 7 8 homfeqval ${⊢}{\phi }\to {X}{H}{Y}={X}\mathrm{Hom}\left({D}\right){Y}$
25 10 24 eleqtrd ${⊢}{\phi }\to {F}\in \left({X}\mathrm{Hom}\left({D}\right){Y}\right)$
26 1 2 18 5 8 9 homfeqval ${⊢}{\phi }\to {Y}{H}{Z}={Y}\mathrm{Hom}\left({D}\right){Z}$
27 11 26 eleqtrd ${⊢}{\phi }\to {G}\in \left({Y}\mathrm{Hom}\left({D}\right){Z}\right)$
28 16 17 18 4 21 22 23 25 27 comfval
29 13 15 28 3eqtr3d