Step | Hyp | Ref
| Expression |
1 | | catcocl.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
2 | | catcocl.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
3 | | catcocl.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
4 | | catcocl.o |
. . . . 5
⊢ · =
(comp‘𝐶) |
5 | 2, 3, 4 | iscat 17175 |
. . . 4
⊢ (𝐶 ∈ Cat → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))))) |
6 | 5 | ibi 270 |
. . 3
⊢ (𝐶 ∈ Cat → ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
7 | 1, 6 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))))) |
8 | | catcocl.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
9 | | catcocl.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
10 | 9 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑌 ∈ 𝐵) |
11 | | catcocl.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
12 | 11 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝑍 ∈ 𝐵) |
13 | | catcocl.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑋𝐻𝑌)) |
14 | 13 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑋𝐻𝑌)) |
15 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑥 = 𝑋) |
16 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌) |
17 | 15, 16 | oveq12d 7231 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌)) |
18 | 14, 17 | eleqtrrd 2841 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝐹 ∈ (𝑥𝐻𝑦)) |
19 | | catcocl.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (𝑌𝐻𝑍)) |
20 | 19 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝐺 ∈ (𝑌𝐻𝑍)) |
21 | | simpllr 776 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝑦 = 𝑌) |
22 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝑧 = 𝑍) |
23 | 21, 22 | oveq12d 7231 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → (𝑦𝐻𝑧) = (𝑌𝐻𝑍)) |
24 | 20, 23 | eleqtrrd 2841 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → 𝐺 ∈ (𝑦𝐻𝑧)) |
25 | | catass.w |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ 𝐵) |
26 | 25 | ad5antr 734 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑊 ∈ 𝐵) |
27 | | catass.g |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ (𝑍𝐻𝑊)) |
28 | 27 | ad6antr 736 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → 𝐾 ∈ (𝑍𝐻𝑊)) |
29 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → 𝑧 = 𝑍) |
30 | | simpr 488 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → 𝑤 = 𝑊) |
31 | 29, 30 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → (𝑧𝐻𝑤) = (𝑍𝐻𝑊)) |
32 | 28, 31 | eleqtrrd 2841 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → 𝐾 ∈ (𝑧𝐻𝑤)) |
33 | | simp-7r 790 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑥 = 𝑋) |
34 | | simp-6r 788 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑦 = 𝑌) |
35 | 33, 34 | opeq12d 4792 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 〈𝑥, 𝑦〉 = 〈𝑋, 𝑌〉) |
36 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑤 = 𝑊) |
37 | 35, 36 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (〈𝑥, 𝑦〉 · 𝑤) = (〈𝑋, 𝑌〉 · 𝑊)) |
38 | | simp-5r 786 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑧 = 𝑍) |
39 | 34, 38 | opeq12d 4792 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 〈𝑦, 𝑧〉 = 〈𝑌, 𝑍〉) |
40 | 39, 36 | oveq12d 7231 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (〈𝑦, 𝑧〉 · 𝑤) = (〈𝑌, 𝑍〉 · 𝑊)) |
41 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾) |
42 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑔 = 𝐺) |
43 | 40, 41, 42 | oveq123d 7234 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔) = (𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)) |
44 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 𝑓 = 𝐹) |
45 | 37, 43, 44 | oveq123d 7234 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹)) |
46 | 33, 38 | opeq12d 4792 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → 〈𝑥, 𝑧〉 = 〈𝑋, 𝑍〉) |
47 | 46, 36 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (〈𝑥, 𝑧〉 · 𝑤) = (〈𝑋, 𝑍〉 · 𝑊)) |
48 | 35, 38 | oveq12d 7231 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑋, 𝑌〉 · 𝑍)) |
49 | 48, 42, 44 | oveq123d 7234 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)) |
50 | 47, 41, 49 | oveq123d 7234 |
. . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹))) |
51 | 45, 50 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) ∧ 𝑘 = 𝐾) → (((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
52 | 32, 51 | rspcdv 3529 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) ∧ 𝑤 = 𝑊) → (∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
53 | 26, 52 | rspcimdv 3527 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
54 | 53 | adantld 494 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
55 | 24, 54 | rspcimdv 3527 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
56 | 18, 55 | rspcimdv 3527 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
57 | 12, 56 | rspcimdv 3527 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → (∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
58 | 10, 57 | rspcimdv 3527 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
59 | 58 | adantld 494 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
60 | 8, 59 | rspcimdv 3527 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦 ∈ 𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(〈𝑦, 𝑥〉 · 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(〈𝑥, 𝑥〉 · 𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤 ∈ 𝐵 ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)))) → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹)))) |
61 | 7, 60 | mpd 15 |
1
⊢ (𝜑 → ((𝐾(〈𝑌, 𝑍〉 · 𝑊)𝐺)(〈𝑋, 𝑌〉 · 𝑊)𝐹) = (𝐾(〈𝑋, 𝑍〉 · 𝑊)(𝐺(〈𝑋, 𝑌〉 · 𝑍)𝐹))) |