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

Theorem nati 17902
Description: Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
natrcl.1 𝑁 = (𝐶 Nat 𝐷)
natixp.2 (𝜑𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩))
natixp.b 𝐵 = (Base‘𝐶)
nati.h 𝐻 = (Hom ‘𝐶)
nati.o · = (comp‘𝐷)
nati.x (𝜑𝑋𝐵)
nati.y (𝜑𝑌𝐵)
nati.r (𝜑𝑅 ∈ (𝑋𝐻𝑌))
Assertion
Ref Expression
nati (𝜑 → ((𝐴𝑌)(⟨(𝐹𝑋), (𝐹𝑌)⟩ · (𝐾𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹𝑋), (𝐾𝑋)⟩ · (𝐾𝑌))(𝐴𝑋)))

Proof of Theorem nati
Dummy variables 𝑥 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 natixp.2 . . . 4 (𝜑𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩))
2 natrcl.1 . . . . 5 𝑁 = (𝐶 Nat 𝐷)
3 natixp.b . . . . 5 𝐵 = (Base‘𝐶)
4 nati.h . . . . 5 𝐻 = (Hom ‘𝐶)
5 eqid 2733 . . . . 5 (Hom ‘𝐷) = (Hom ‘𝐷)
6 nati.o . . . . 5 · = (comp‘𝐷)
72natrcl 17897 . . . . . . . 8 (𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩) → (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) ∧ ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷)))
81, 7syl 17 . . . . . . 7 (𝜑 → (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) ∧ ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷)))
98simpld 496 . . . . . 6 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
10 df-br 5148 . . . . . 6 (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
119, 10sylibr 233 . . . . 5 (𝜑𝐹(𝐶 Func 𝐷)𝐺)
128simprd 497 . . . . . 6 (𝜑 → ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷))
13 df-br 5148 . . . . . 6 (𝐾(𝐶 Func 𝐷)𝐿 ↔ ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷))
1412, 13sylibr 233 . . . . 5 (𝜑𝐾(𝐶 Func 𝐷)𝐿)
152, 3, 4, 5, 6, 11, 14isnat 17894 . . . 4 (𝜑 → (𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩) ↔ (𝐴X𝑥𝐵 ((𝐹𝑥)(Hom ‘𝐷)(𝐾𝑥)) ∧ ∀𝑥𝐵𝑦𝐵𝑓 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)))))
161, 15mpbid 231 . . 3 (𝜑 → (𝐴X𝑥𝐵 ((𝐹𝑥)(Hom ‘𝐷)(𝐾𝑥)) ∧ ∀𝑥𝐵𝑦𝐵𝑓 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥))))
1716simprd 497 . 2 (𝜑 → ∀𝑥𝐵𝑦𝐵𝑓 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)))
18 nati.x . . 3 (𝜑𝑋𝐵)
19 nati.y . . . . 5 (𝜑𝑌𝐵)
2019adantr 482 . . . 4 ((𝜑𝑥 = 𝑋) → 𝑌𝐵)
21 nati.r . . . . . . 7 (𝜑𝑅 ∈ (𝑋𝐻𝑌))
2221ad2antrr 725 . . . . . 6 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑅 ∈ (𝑋𝐻𝑌))
23 simplr 768 . . . . . . 7 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑥 = 𝑋)
24 simpr 486 . . . . . . 7 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌)
2523, 24oveq12d 7422 . . . . . 6 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌))
2622, 25eleqtrrd 2837 . . . . 5 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑅 ∈ (𝑥𝐻𝑦))
27 simpllr 775 . . . . . . . . . 10 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → 𝑥 = 𝑋)
2827fveq2d 6892 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐹𝑥) = (𝐹𝑋))
29 simplr 768 . . . . . . . . . 10 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → 𝑦 = 𝑌)
3029fveq2d 6892 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐹𝑦) = (𝐹𝑌))
3128, 30opeq12d 4880 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨(𝐹𝑋), (𝐹𝑌)⟩)
3229fveq2d 6892 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐾𝑦) = (𝐾𝑌))
3331, 32oveq12d 7422 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦)) = (⟨(𝐹𝑋), (𝐹𝑌)⟩ · (𝐾𝑌)))
3429fveq2d 6892 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐴𝑦) = (𝐴𝑌))
3527, 29oveq12d 7422 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝑥𝐺𝑦) = (𝑋𝐺𝑌))
36 simpr 486 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → 𝑓 = 𝑅)
3735, 36fveq12d 6895 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → ((𝑥𝐺𝑦)‘𝑓) = ((𝑋𝐺𝑌)‘𝑅))
3833, 34, 37oveq123d 7425 . . . . . 6 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → ((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘𝑓)) = ((𝐴𝑌)(⟨(𝐹𝑋), (𝐹𝑌)⟩ · (𝐾𝑌))((𝑋𝐺𝑌)‘𝑅)))
3927fveq2d 6892 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐾𝑥) = (𝐾𝑋))
4028, 39opeq12d 4880 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → ⟨(𝐹𝑥), (𝐾𝑥)⟩ = ⟨(𝐹𝑋), (𝐾𝑋)⟩)
4140, 32oveq12d 7422 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦)) = (⟨(𝐹𝑋), (𝐾𝑋)⟩ · (𝐾𝑌)))
4227, 29oveq12d 7422 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝑥𝐿𝑦) = (𝑋𝐿𝑌))
4342, 36fveq12d 6895 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → ((𝑥𝐿𝑦)‘𝑓) = ((𝑋𝐿𝑌)‘𝑅))
4427fveq2d 6892 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (𝐴𝑥) = (𝐴𝑋))
4541, 43, 44oveq123d 7425 . . . . . 6 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (((𝑥𝐿𝑦)‘𝑓)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹𝑋), (𝐾𝑋)⟩ · (𝐾𝑌))(𝐴𝑋)))
4638, 45eqeq12d 2749 . . . . 5 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑓 = 𝑅) → (((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)) ↔ ((𝐴𝑌)(⟨(𝐹𝑋), (𝐹𝑌)⟩ · (𝐾𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹𝑋), (𝐾𝑋)⟩ · (𝐾𝑌))(𝐴𝑋))))
4726, 46rspcdv 3604 . . . 4 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑓 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)) → ((𝐴𝑌)(⟨(𝐹𝑋), (𝐹𝑌)⟩ · (𝐾𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹𝑋), (𝐾𝑋)⟩ · (𝐾𝑌))(𝐴𝑋))))
4820, 47rspcimdv 3602 . . 3 ((𝜑𝑥 = 𝑋) → (∀𝑦𝐵𝑓 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)) → ((𝐴𝑌)(⟨(𝐹𝑋), (𝐹𝑌)⟩ · (𝐾𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹𝑋), (𝐾𝑋)⟩ · (𝐾𝑌))(𝐴𝑋))))
4918, 48rspcimdv 3602 . 2 (𝜑 → (∀𝑥𝐵𝑦𝐵𝑓 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘𝑓)) = (((𝑥𝐿𝑦)‘𝑓)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)) → ((𝐴𝑌)(⟨(𝐹𝑋), (𝐹𝑌)⟩ · (𝐾𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹𝑋), (𝐾𝑋)⟩ · (𝐾𝑌))(𝐴𝑋))))
5017, 49mpd 15 1 (𝜑 → ((𝐴𝑌)(⟨(𝐹𝑋), (𝐹𝑌)⟩ · (𝐾𝑌))((𝑋𝐺𝑌)‘𝑅)) = (((𝑋𝐿𝑌)‘𝑅)(⟨(𝐹𝑋), (𝐾𝑋)⟩ · (𝐾𝑌))(𝐴𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  wral 3062  cop 4633   class class class wbr 5147  cfv 6540  (class class class)co 7404  Xcixp 8887  Basecbs 17140  Hom chom 17204  compcco 17205   Func cfunc 17800   Nat cnat 17888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7970  df-2nd 7971  df-ixp 8888  df-func 17804  df-nat 17890
This theorem is referenced by:  fuccocl  17913  invfuc  17923  evlfcllem  18170  yonedalem3b  18228  yonedainv  18230
  Copyright terms: Public domain W3C validator