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

Theorem hofval 16813
 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 16811 . . . 4 HomF = (𝑐 ∈ Cat ↦ ⟨(Homf𝑐), (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))⟩)
32a1i 11 . . 3 (𝜑 → HomF = (𝑐 ∈ Cat ↦ ⟨(Homf𝑐), (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))⟩))
4 simpr 477 . . . . 5 ((𝜑𝑐 = 𝐶) → 𝑐 = 𝐶)
54fveq2d 6152 . . . 4 ((𝜑𝑐 = 𝐶) → (Homf𝑐) = (Homf𝐶))
6 fvex 6158 . . . . . 6 (Base‘𝑐) ∈ V
76a1i 11 . . . . 5 ((𝜑𝑐 = 𝐶) → (Base‘𝑐) ∈ V)
84fveq2d 6152 . . . . . 6 ((𝜑𝑐 = 𝐶) → (Base‘𝑐) = (Base‘𝐶))
9 hofval.b . . . . . 6 𝐵 = (Base‘𝐶)
108, 9syl6eqr 2673 . . . . 5 ((𝜑𝑐 = 𝐶) → (Base‘𝑐) = 𝐵)
11 simpr 477 . . . . . . 7 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
1211sqxpeqd 5101 . . . . . 6 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
13 simplr 791 . . . . . . . . . 10 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶)
1413fveq2d 6152 . . . . . . . . 9 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶))
15 hofval.h . . . . . . . . 9 𝐻 = (Hom ‘𝐶)
1614, 15syl6eqr 2673 . . . . . . . 8 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻)
1716oveqd 6621 . . . . . . 7 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((1st𝑦)(Hom ‘𝑐)(1st𝑥)) = ((1st𝑦)𝐻(1st𝑥)))
1816oveqd 6621 . . . . . . 7 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) = ((2nd𝑥)𝐻(2nd𝑦)))
1916fveq1d 6150 . . . . . . . 8 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑐)‘𝑥) = (𝐻𝑥))
2013fveq2d 6152 . . . . . . . . . . 11 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = (comp‘𝐶))
21 hofval.o . . . . . . . . . . 11 · = (comp‘𝐶)
2220, 21syl6eqr 2673 . . . . . . . . . 10 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = · )
2322oveqd 6621 . . . . . . . . 9 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦)) = (⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦)))
2422oveqd 6621 . . . . . . . . . 10 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥(comp‘𝑐)(2nd𝑦)) = (𝑥 · (2nd𝑦)))
2524oveqd 6621 . . . . . . . . 9 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑔(𝑥(comp‘𝑐)(2nd𝑦))) = (𝑔(𝑥 · (2nd𝑦))))
26 eqidd 2622 . . . . . . . . 9 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓)
2723, 25, 26oveq123d 6625 . . . . . . . 8 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓) = ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))
2819, 27mpteq12dv 4693 . . . . . . 7 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓)) = ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓)))
2917, 18, 28mpt2eq123dv 6670 . . . . . 6 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))) = (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))
3012, 12, 29mpt2eq123dv 6670 . . . . 5 (((𝜑𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓)))))
317, 10, 30csbied2 3542 . . . 4 ((𝜑𝑐 = 𝐶) → (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓)))))
325, 31opeq12d 4378 . . 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𝑦))𝑓))))⟩)
33 hofval.c . . 3 (𝜑𝐶 ∈ Cat)
34 opex 4893 . . . 4 ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩ ∈ V
3534a1i 11 . . 3 (𝜑 → ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩ ∈ V)
363, 32, 33, 35fvmptd 6245 . 2 (𝜑 → (HomF𝐶) = ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩)
371, 36syl5eq 2667 1 (𝜑𝑀 = ⟨(Homf𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st𝑦)𝐻(1st𝑥)), 𝑔 ∈ ((2nd𝑥)𝐻(2nd𝑦)) ↦ ( ∈ (𝐻𝑥) ↦ ((𝑔(𝑥 · (2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩ · (2nd𝑦))𝑓))))⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  Vcvv 3186  ⦋csb 3514  ⟨cop 4154   ↦ cmpt 4673   × cxp 5072  ‘cfv 5847  (class class class)co 6604   ↦ cmpt2 6606  1st c1st 7111  2nd c2nd 7112  Basecbs 15781  Hom chom 15873  compcco 15874  Catccat 16246  Homf chomf 16248  HomFchof 16809 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-iota 5810  df-fun 5849  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-hof 16811 This theorem is referenced by:  hof1fval  16814  hof2fval  16816  hofcl  16820  hofpropd  16828
 Copyright terms: Public domain W3C validator