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 XHY=XJY$$

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=XHY$$
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=XJY$$
17	7 9 16	3eqtr3d	$$⊢\phi \to XHY=XJY$$