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

Theorem hofval 18101
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 18099 . . 3 HomF = (𝑐 ∈ Cat ↦ ⟨(Homf β€˜π‘), ⦋(Baseβ€˜π‘) / π‘β¦Œ(π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ (𝑏 Γ— 𝑏) ↦ (𝑓 ∈ ((1st β€˜π‘¦)(Hom β€˜π‘)(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)(Hom β€˜π‘)(2nd β€˜π‘¦)) ↦ (β„Ž ∈ ((Hom β€˜π‘)β€˜π‘₯) ↦ ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓))))⟩)
3 simpr 485 . . . . 5 ((πœ‘ ∧ 𝑐 = 𝐢) β†’ 𝑐 = 𝐢)
43fveq2d 6843 . . . 4 ((πœ‘ ∧ 𝑐 = 𝐢) β†’ (Homf β€˜π‘) = (Homf β€˜πΆ))
5 fvexd 6854 . . . . 5 ((πœ‘ ∧ 𝑐 = 𝐢) β†’ (Baseβ€˜π‘) ∈ V)
63fveq2d 6843 . . . . . 6 ((πœ‘ ∧ 𝑐 = 𝐢) β†’ (Baseβ€˜π‘) = (Baseβ€˜πΆ))
7 hofval.b . . . . . 6 𝐡 = (Baseβ€˜πΆ)
86, 7eqtr4di 2795 . . . . 5 ((πœ‘ ∧ 𝑐 = 𝐢) β†’ (Baseβ€˜π‘) = 𝐡)
9 simpr 485 . . . . . . 7 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ 𝑏 = 𝐡)
109sqxpeqd 5663 . . . . . 6 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ (𝑏 Γ— 𝑏) = (𝐡 Γ— 𝐡))
11 simplr 767 . . . . . . . . . 10 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ 𝑐 = 𝐢)
1211fveq2d 6843 . . . . . . . . 9 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ (Hom β€˜π‘) = (Hom β€˜πΆ))
13 hofval.h . . . . . . . . 9 𝐻 = (Hom β€˜πΆ)
1412, 13eqtr4di 2795 . . . . . . . 8 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ (Hom β€˜π‘) = 𝐻)
1514oveqd 7368 . . . . . . 7 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ ((1st β€˜π‘¦)(Hom β€˜π‘)(1st β€˜π‘₯)) = ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)))
1614oveqd 7368 . . . . . . 7 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ ((2nd β€˜π‘₯)(Hom β€˜π‘)(2nd β€˜π‘¦)) = ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)))
1714fveq1d 6841 . . . . . . . 8 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ ((Hom β€˜π‘)β€˜π‘₯) = (π»β€˜π‘₯))
1811fveq2d 6843 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ (compβ€˜π‘) = (compβ€˜πΆ))
19 hofval.o . . . . . . . . . . 11 Β· = (compβ€˜πΆ)
2018, 19eqtr4di 2795 . . . . . . . . . 10 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ (compβ€˜π‘) = Β· )
2120oveqd 7368 . . . . . . . . 9 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ (⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦)) = (⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦)))
2220oveqd 7368 . . . . . . . . . 10 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ (π‘₯(compβ€˜π‘)(2nd β€˜π‘¦)) = (π‘₯ Β· (2nd β€˜π‘¦)))
2322oveqd 7368 . . . . . . . . 9 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ (𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž) = (𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž))
24 eqidd 2738 . . . . . . . . 9 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ 𝑓 = 𝑓)
2521, 23, 24oveq123d 7372 . . . . . . . 8 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓) = ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓))
2617, 25mpteq12dv 5194 . . . . . . 7 (((πœ‘ ∧ 𝑐 = 𝐢) ∧ 𝑏 = 𝐡) β†’ (β„Ž ∈ ((Hom β€˜π‘)β€˜π‘₯) ↦ ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓)) = (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓)))
2715, 16, 26mpoeq123dv 7426 . . . . . 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 7426 . . . . 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 3893 . . . 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 4836 . . 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 5419 . . . 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 6953 . 2 (πœ‘ β†’ (HomFβ€˜πΆ) = ⟨(Homf β€˜πΆ), (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ (𝐡 Γ— 𝐡) ↦ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓))))⟩)
351, 34eqtrid 2789 1 (πœ‘ β†’ 𝑀 = ⟨(Homf β€˜πΆ), (π‘₯ ∈ (𝐡 Γ— 𝐡), 𝑦 ∈ (𝐡 Γ— 𝐡) ↦ (𝑓 ∈ ((1st β€˜π‘¦)𝐻(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)𝐻(2nd β€˜π‘¦)) ↦ (β„Ž ∈ (π»β€˜π‘₯) ↦ ((𝑔(π‘₯ Β· (2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩ Β· (2nd β€˜π‘¦))𝑓))))⟩)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3443  β¦‹csb 3853  βŸ¨cop 4590   ↦ cmpt 5186   Γ— cxp 5629  β€˜cfv 6493  (class class class)co 7351   ∈ cmpo 7353  1st c1st 7911  2nd c2nd 7912  Basecbs 17043  Hom chom 17104  compcco 17105  Catccat 17504  Homf chomf 17506  HomFchof 18097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6445  df-fun 6495  df-fv 6501  df-ov 7354  df-oprab 7355  df-mpo 7356  df-hof 18099
This theorem is referenced by:  hof1fval  18102  hof2fval  18104  hofcl  18108  hofpropd  18116
  Copyright terms: Public domain W3C validator