 Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  hofval Structured version   Visualization version   GIF version

Theorem hofval 17372
 Description: Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat‘𝐶) × 𝐶 to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017.)
Hypotheses
Ref Expression
hofval.m 𝑀 = (HomF𝐶)
hofval.c (𝜑𝐶 ∈ Cat)
hofval.b 𝐵 = (Base‘𝐶)
hofval.h 𝐻 = (Hom ‘𝐶)
hofval.o · = (comp‘𝐶)
Assertion
Ref Expression
hofval (𝜑𝑀 = ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩)
Distinct variable groups:   𝑓,𝑔,,𝑥,𝑦,𝐵   𝜑,𝑓,𝑔,,𝑥,𝑦   𝐶,𝑓,𝑔,,𝑥,𝑦   𝑓,𝐻,𝑔,,𝑥,𝑦   · ,𝑓,𝑔,,𝑥,𝑦
Allowed substitution hints:   𝑀(𝑥,𝑦,𝑓,𝑔,)

Proof of Theorem hofval
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hofval.m . 2 𝑀 = (HomF𝐶)
2 df-hof 17370 . . 3 HomF = (𝑐 ∈ Cat ↦ ⟨(Homf𝑐), (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))⟩)
3 simpr 477 . . . . 5 ((𝜑𝑐 = 𝐶) → 𝑐 = 𝐶)
43fveq2d 6500 . . . 4 ((𝜑𝑐 = 𝐶) → (Homf𝑐) = (Homf𝐶))
5 fvexd 6511 . . . . 5 ((𝜑𝑐 = 𝐶) → (Base‘𝑐) ∈ V)
63fveq2d 6500 . . . . . 6 ((𝜑𝑐 = 𝐶) → (Base‘𝑐) = (Base‘𝐶))
7 hofval.b . . . . . 6 𝐵 = (Base‘𝐶)
86, 7syl6eqr 2825 . . . . 5 ((𝜑𝑐 = 𝐶) → (Base‘𝑐) = 𝐵)
9 simpr 477 . . . . . . 7 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
109sqxpeqd 5435 . . . . . 6 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
11 simplr 757 . . . . . . . . . 10 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶)
1211fveq2d 6500 . . . . . . . . 9 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶))
13 hofval.h . . . . . . . . 9 𝐻 = (Hom ‘𝐶)
1412, 13syl6eqr 2825 . . . . . . . 8 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻)
1514oveqd 6991 . . . . . . 7 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((1st𝑦)(Hom ‘𝑐)(1st𝑥)) = ((1st𝑦)𝐻(1st𝑥)))
1614oveqd 6991 . . . . . . 7 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) = ((2nd𝑥)𝐻(2nd𝑦)))
1714fveq1d 6498 . . . . . . . 8 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑐)‘𝑥) = (𝐻𝑥))
1811fveq2d 6500 . . . . . . . . . . 11 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = (comp‘𝐶))
19 hofval.o . . . . . . . . . . 11 · = (comp‘𝐶)
2018, 19syl6eqr 2825 . . . . . . . . . 10 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = · )
2120oveqd 6991 . . . . . . . . 9 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦)) = (⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦)))
2220oveqd 6991 . . . . . . . . . 10 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥(comp‘𝑐)(2nd𝑦)) = (𝑥 · (2nd𝑦)))
2322oveqd 6991 . . . . . . . . 9 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑔(𝑥(comp‘𝑐)(2nd𝑦))) = (𝑔(𝑥 · (2nd𝑦))))
24 eqidd 2772 . . . . . . . . 9 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓)
2521, 23, 24oveq123d 6995 . . . . . . . 8 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓) = ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))
2617, 25mpteq12dv 5008 . . . . . . 7 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓)) = ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓)))
2715, 16, 26mpoeq123dv 7045 . . . . . 6 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))) = (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))
2810, 10, 27mpoeq123dv 7045 . . . . 5 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓)))))
295, 8, 28csbied2 3809 . . . 4 ((𝜑𝑐 = 𝐶) → (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓)))))
304, 29opeq12d 4681 . . 3 ((𝜑𝑐 = 𝐶) → ⟨(Homf𝑐), (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))⟩ = ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩)
31 hofval.c . . 3 (𝜑𝐶 ∈ Cat)
32 opex 5209 . . . 4 ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩ ∈ V
3332a1i 11 . . 3 (𝜑 → ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩ ∈ V)
342, 30, 31, 33fvmptd2 6600 . 2 (𝜑 → (HomF𝐶) = ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩)
351, 34syl5eq 2819 1 (𝜑𝑀 = ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 387   = wceq 1508   ∈ wcel 2051  Vcvv 3408  ⦋csb 3779  ⟨cop 4441   ↦ cmpt 5004   × cxp 5401  ‘cfv 6185  (class class class)co 6974   ∈ cmpo 6976  1st c1st 7497  2nd c2nd 7498  Basecbs 16337  Hom chom 16430  compcco 16431  Catccat 16805  Homf chomf 16807  HomFchof 17368 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-sep 5056  ax-nul 5063  ax-pr 5182 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ral 3086  df-rex 3087  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-opab 4988  df-mpt 5005  df-id 5308  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-iota 6149  df-fun 6187  df-fv 6193  df-ov 6977  df-oprab 6978  df-mpo 6979  df-hof 17370 This theorem is referenced by:  hof1fval  17373  hof2fval  17375  hofcl  17379  hofpropd  17387
 Copyright terms: Public domain W3C validator