This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( 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 eqtrid ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐷 ) )
14 5 13 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
15 6 13 eleqtrd ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
16 10 11 3 14 15 homfval ⊢ ( 𝜑 → ( 𝑋 ( Homf ‘ 𝐷 ) 𝑌 ) = ( 𝑋 𝐽 𝑌 ) )
17 7 9 16 3eqtr3d ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 𝐽 𝑌 ) )