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 ⊢ B = Base C
homfeqval.h ⊢ H = Hom ⁡ C
homfeqval.j ⊢ J = Hom ⁡ D
homfeqval.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
homfeqval.x ⊢ φ → X ∈ B
homfeqval.y ⊢ φ → Y ∈ B
Assertion homfeqval ⊢ φ → X H Y = X J Y

Proof

Step Hyp Ref Expression
1 homfeqval.b ⊢ B = Base C
2 homfeqval.h ⊢ H = Hom ⁡ C
3 homfeqval.j ⊢ J = Hom ⁡ D
4 homfeqval.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
5 homfeqval.x ⊢ φ → X ∈ B
6 homfeqval.y ⊢ φ → Y ∈ B
7 4 oveqd ⊢ φ → X Hom 𝑓 ⁡ C Y = X Hom 𝑓 ⁡ D Y
8 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
9 8 1 2 5 6 homfval ⊢ φ → X Hom 𝑓 ⁡ C Y = X H Y
10 eqid ⊢ Hom 𝑓 ⁡ D = Hom 𝑓 ⁡ D
11 eqid ⊢ Base D = Base D
12 4 homfeqbas ⊢ φ → Base C = Base D
13 1 12 eqtrid ⊢ φ → B = Base D
14 5 13 eleqtrd ⊢ φ → X ∈ Base D
15 6 13 eleqtrd ⊢ φ → Y ∈ Base D
16 10 11 3 14 15 homfval ⊢ φ → X Hom 𝑓 ⁡ D Y = X J Y
17 7 9 16 3eqtr3d ⊢ φ → X H Y = X J Y