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

Theorem catass 17454
Description: Associativity of composition in a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
catcocl.b 𝐵 = (Base‘𝐶)
catcocl.h 𝐻 = (Hom ‘𝐶)
catcocl.o · = (comp‘𝐶)
catcocl.c (𝜑𝐶 ∈ Cat)
catcocl.x (𝜑𝑋𝐵)
catcocl.y (𝜑𝑌𝐵)
catcocl.z (𝜑𝑍𝐵)
catcocl.f (𝜑𝐹 ∈ (𝑋𝐻𝑌))
catcocl.g (𝜑𝐺 ∈ (𝑌𝐻𝑍))
catass.w (𝜑𝑊𝐵)
catass.g (𝜑𝐾 ∈ (𝑍𝐻𝑊))
Assertion
Ref Expression
catass (𝜑 → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹)))

Proof of Theorem catass
Dummy variables 𝑓 𝑔 𝑘 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcocl.c . . 3 (𝜑𝐶 ∈ Cat)
2 catcocl.b . . . . 5 𝐵 = (Base‘𝐶)
3 catcocl.h . . . . 5 𝐻 = (Hom ‘𝐶)
4 catcocl.o . . . . 5 · = (comp‘𝐶)
52, 3, 4iscat 17440 . . . 4 (𝐶 ∈ Cat → (𝐶 ∈ Cat ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
65ibi 266 . . 3 (𝐶 ∈ Cat → ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
71, 6syl 17 . 2 (𝜑 → ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
8 catcocl.x . . 3 (𝜑𝑋𝐵)
9 catcocl.y . . . . . 6 (𝜑𝑌𝐵)
109adantr 481 . . . . 5 ((𝜑𝑥 = 𝑋) → 𝑌𝐵)
11 catcocl.z . . . . . . 7 (𝜑𝑍𝐵)
1211ad2antrr 723 . . . . . 6 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑍𝐵)
13 catcocl.f . . . . . . . . 9 (𝜑𝐹 ∈ (𝑋𝐻𝑌))
1413ad3antrrr 727 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑋𝐻𝑌))
15 simpllr 773 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑥 = 𝑋)
16 simplr 766 . . . . . . . . 9 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
1715, 16oveq12d 7326 . . . . . . . 8 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌))
1814, 17eleqtrrd 2839 . . . . . . 7 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑥𝐻𝑦))
19 catcocl.g . . . . . . . . . 10 (𝜑𝐺 ∈ (𝑌𝐻𝑍))
2019ad4antr 729 . . . . . . . . 9 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝐺 ∈ (𝑌𝐻𝑍))
21 simpllr 773 . . . . . . . . . 10 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝑦 = 𝑌)
22 simplr 766 . . . . . . . . . 10 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝑧 = 𝑍)
2321, 22oveq12d 7326 . . . . . . . . 9 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → (𝑦𝐻𝑧) = (𝑌𝐻𝑍))
2420, 23eleqtrrd 2839 . . . . . . . 8 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝐺 ∈ (𝑦𝐻𝑧))
25 catass.w . . . . . . . . . . 11 (𝜑𝑊𝐵)
2625ad5antr 731 . . . . . . . . . 10 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑊𝐵)
27 catass.g . . . . . . . . . . . . 13 (𝜑𝐾 ∈ (𝑍𝐻𝑊))
2827ad6antr 733 . . . . . . . . . . . 12 (((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → 𝐾 ∈ (𝑍𝐻𝑊))
29 simp-4r 781 . . . . . . . . . . . . 13 (((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → 𝑧 = 𝑍)
30 simpr 485 . . . . . . . . . . . . 13 (((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → 𝑤 = 𝑊)
3129, 30oveq12d 7326 . . . . . . . . . . . 12 (((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → (𝑧𝐻𝑤) = (𝑍𝐻𝑊))
3228, 31eleqtrrd 2839 . . . . . . . . . . 11 (((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → 𝐾 ∈ (𝑧𝐻𝑤))
33 simp-7r 787 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑥 = 𝑋)
34 simp-6r 785 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑦 = 𝑌)
3533, 34opeq12d 4816 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩)
36 simplr 766 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑤 = 𝑊)
3735, 36oveq12d 7326 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (⟨𝑥, 𝑦· 𝑤) = (⟨𝑋, 𝑌· 𝑊))
38 simp-5r 783 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑧 = 𝑍)
3934, 38opeq12d 4816 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ⟨𝑦, 𝑧⟩ = ⟨𝑌, 𝑍⟩)
4039, 36oveq12d 7326 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (⟨𝑦, 𝑧· 𝑤) = (⟨𝑌, 𝑍· 𝑊))
41 simpr 485 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾)
42 simpllr 773 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑔 = 𝐺)
4340, 41, 42oveq123d 7329 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔) = (𝐾(⟨𝑌, 𝑍· 𝑊)𝐺))
44 simp-4r 781 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑓 = 𝐹)
4537, 43, 44oveq123d 7329 . . . . . . . . . . . 12 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹))
4633, 38opeq12d 4816 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ⟨𝑥, 𝑧⟩ = ⟨𝑋, 𝑍⟩)
4746, 36oveq12d 7326 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (⟨𝑥, 𝑧· 𝑤) = (⟨𝑋, 𝑍· 𝑊))
4835, 38oveq12d 7326 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (⟨𝑥, 𝑦· 𝑧) = (⟨𝑋, 𝑌· 𝑍))
4948, 42, 44oveq123d 7329 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) = (𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))
5047, 41, 49oveq123d 7329 . . . . . . . . . . . 12 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹)))
5145, 50eqeq12d 2751 . . . . . . . . . . 11 ((((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) ↔ ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
5232, 51rspcdv 3557 . . . . . . . . . 10 (((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → (∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
5326, 52rspcimdv 3555 . . . . . . . . 9 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)) → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
5453adantld 491 . . . . . . . 8 ((((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
5524, 54rspcimdv 3555 . . . . . . 7 (((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
5618, 55rspcimdv 3555 . . . . . 6 ((((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
5712, 56rspcimdv 3555 . . . . 5 (((𝜑𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
5810, 57rspcimdv 3555 . . . 4 ((𝜑𝑥 = 𝑋) → (∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))) → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
5958adantld 491 . . 3 ((𝜑𝑥 = 𝑋) → ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
608, 59rspcimdv 3555 . 2 (𝜑 → (∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))) → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹))))
617, 60mpd 15 1 (𝜑 → ((𝐾(⟨𝑌, 𝑍· 𝑊)𝐺)(⟨𝑋, 𝑌· 𝑊)𝐹) = (𝐾(⟨𝑋, 𝑍· 𝑊)(𝐺(⟨𝑋, 𝑌· 𝑍)𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1538  wcel 2103  wral 3060  wrex 3069  cop 4570  cfv 6458  (class class class)co 7308  Basecbs 16971  Hom chom 17032  compcco 17033  Catccat 17432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-ext 2706  ax-nul 5238
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-sb 2065  df-clab 2713  df-cleq 2727  df-clel 2813  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3357  df-v 3438  df-sbc 3721  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4844  df-br 5081  df-iota 6410  df-fv 6466  df-ov 7311  df-cat 17436
This theorem is referenced by:  oppccatid  17489  sectcan  17526  sectco  17527  sectmon  17553  monsect  17554  rcaninv  17565  subccatid  17620  fuccocl  17741  fucass  17745  invfuc  17751  arwass  17848  xpccatid  17964  evlfcllem  17998  hofcllem  18035  bj-endmnd  35547  endmndlem  46553
  Copyright terms: Public domain W3C validator