# Metamath Proof Explorer

## Theorem homfeqval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses homfeqval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
homfeqval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
homfeqval.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
homfeqval.1 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
homfeqval.x ${⊢}{\phi }\to {X}\in {B}$
homfeqval.y ${⊢}{\phi }\to {Y}\in {B}$
Assertion homfeqval ${⊢}{\phi }\to {X}{H}{Y}={X}{J}{Y}$

### Proof

Step Hyp Ref Expression
1 homfeqval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 homfeqval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 homfeqval.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
4 homfeqval.1 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
5 homfeqval.x ${⊢}{\phi }\to {X}\in {B}$
6 homfeqval.y ${⊢}{\phi }\to {Y}\in {B}$
7 4 oveqd ${⊢}{\phi }\to {X}{\mathrm{Hom}}_{𝑓}\left({C}\right){Y}={X}{\mathrm{Hom}}_{𝑓}\left({D}\right){Y}$
8 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({C}\right)$
9 8 1 2 5 6 homfval ${⊢}{\phi }\to {X}{\mathrm{Hom}}_{𝑓}\left({C}\right){Y}={X}{H}{Y}$
10 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left({D}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
11 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
12 4 homfeqbas ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{D}}$
13 1 12 syl5eq ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{D}}$
14 5 13 eleqtrd ${⊢}{\phi }\to {X}\in {\mathrm{Base}}_{{D}}$
15 6 13 eleqtrd ${⊢}{\phi }\to {Y}\in {\mathrm{Base}}_{{D}}$
16 10 11 3 14 15 homfval ${⊢}{\phi }\to {X}{\mathrm{Hom}}_{𝑓}\left({D}\right){Y}={X}{J}{Y}$
17 7 9 16 3eqtr3d ${⊢}{\phi }\to {X}{H}{Y}={X}{J}{Y}$