Theorem homfeqval

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

	Ref	Expression
Hypotheses	homfeqval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	homfeqval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	homfeqval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	homfeqval.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
	homfeqval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	homfeqval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	homfeqval	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 𝐽 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		homfeqval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		homfeqval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		homfeqval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
4		homfeqval.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
5		homfeqval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		homfeqval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7	4	oveqd	⊢ ( 𝜑 → ( 𝑋 ( Homf ‘ 𝐶 ) 𝑌 ) = ( 𝑋 ( Homf ‘ 𝐷 ) 𝑌 ) )
8		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
9	8 1 2 5 6	homfval	⊢ ( 𝜑 → ( 𝑋 ( Homf ‘ 𝐶 ) 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )
10		eqid	⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐷 )
11		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
12	4	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
13	1 12	syl5eq	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐷 ) )
14	5 13	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
15	6 13	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
16	10 11 3 14 15	homfval	⊢ ( 𝜑 → ( 𝑋 ( Homf ‘ 𝐷 ) 𝑌 ) = ( 𝑋 𝐽 𝑌 ) )
17	7 9 16	3eqtr3d	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 𝐽 𝑌 ) )