Step | Hyp | Ref
| Expression |
1 | | iscatd2.b |
. . 3
⊢ (𝜑 → 𝐵 = (Base‘𝐶)) |
2 | | iscatd2.h |
. . 3
⊢ (𝜑 → 𝐻 = (Hom ‘𝐶)) |
3 | | iscatd2.o |
. . 3
⊢ (𝜑 → · = (comp‘𝐶)) |
4 | | iscatd2.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
5 | | iscatd2.1 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 1 ∈ (𝑦𝐻𝑦)) |
6 | 5 | ne0d 4250 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝐻𝑦) ≠ ∅) |
7 | 6 | 3ad2antr1 1190 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅) |
8 | | n0 4261 |
. . . . 5
⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦)) |
9 | 7, 8 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦)) |
10 | | n0 4261 |
. . . . 5
⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) |
11 | 7, 10 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) |
12 | | exdistrv 1964 |
. . . . 5
⊢
(∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))) |
13 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑) |
14 | | simplr2 1218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎 ∈ 𝐵) |
15 | | simplr1 1217 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦 ∈ 𝐵) |
16 | 14, 15 | jca 515 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
17 | | simplr3 1219 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦)) |
18 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦)) |
19 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦)) |
20 | 17, 18, 19 | 3jca 1130 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) |
21 | | iscatd2.ps |
. . . . . . . . . . . . . . 15
⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
22 | | simplll 775 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎) |
23 | 22 | eleq1d 2822 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
24 | 23 | anbi1d 633 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
25 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦) |
26 | 25 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
27 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦) |
28 | 27 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
29 | 26, 28 | anbi12d 634 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
30 | | anidm 568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵) |
31 | 29, 30 | bitrdi 290 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵)) |
32 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟) |
33 | 22 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦)) |
34 | 32, 33 | eleq12d 2832 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦))) |
35 | 25 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦)) |
36 | 35 | eleq2d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦))) |
37 | 25, 27 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦)) |
38 | 37 | eleq2d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦))) |
39 | 34, 36, 38 | 3anbi123d 1438 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) |
40 | 24, 31, 39 | 3anbi123d 1438 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))) |
41 | 21, 40 | syl5bb 286 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))) |
42 | 41 | anbi2d 632 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))) |
43 | 22 | opeq1d 4790 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑦〉) |
44 | 43 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑦) = (〈𝑎, 𝑦〉 · 𝑦)) |
45 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 ) |
46 | 44, 45, 32 | oveq123d 7234 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟)) |
47 | 46, 32 | eqeq12d 2753 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓 ↔ ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) |
48 | 42, 47 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) |
49 | 48 | sbiedvw 2100 |
. . . . . . . . . . 11
⊢ (((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) |
50 | 49 | sbiedvw 2100 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) |
51 | 50 | sbiedvw 2100 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) |
52 | | iscatd2.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
53 | 52 | sbt 2072 |
. . . . . . . . . . 11
⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
54 | 53 | sbt 2072 |
. . . . . . . . . 10
⊢ [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
55 | 54 | sbt 2072 |
. . . . . . . . 9
⊢ [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
56 | 51, 55 | chvarvv 2007 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟) |
57 | 13, 16, 15, 20, 56 | syl13anc 1374 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟) |
58 | 57 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) |
59 | 58 | exlimdvv 1942 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) |
60 | 12, 59 | syl5bir 246 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) |
61 | 9, 11, 60 | mp2and 699 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟) |
62 | 6 | 3ad2antr1 1190 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅) |
63 | | n0 4261 |
. . . . 5
⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦)) |
64 | 62, 63 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦)) |
65 | | id 22 |
. . . . . . . 8
⊢ (𝑦 = 𝑎 → 𝑦 = 𝑎) |
66 | 65, 65 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎)) |
67 | 66 | neeq1d 3000 |
. . . . . 6
⊢ (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅)) |
68 | 6 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅) |
69 | 68 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅) |
70 | | simpr2 1197 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎 ∈ 𝐵) |
71 | 67, 69, 70 | rspcdva 3539 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅) |
72 | | n0 4261 |
. . . . 5
⊢ ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) |
73 | 71, 72 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) |
74 | | exdistrv 1964 |
. . . . 5
⊢
(∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))) |
75 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑) |
76 | | simplr1 1217 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦 ∈ 𝐵) |
77 | | simplr2 1218 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎 ∈ 𝐵) |
78 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦)) |
79 | | simplr3 1219 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎)) |
80 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎)) |
81 | 78, 79, 80 | 3jca 1130 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) |
82 | | simplll 775 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦) |
83 | 82 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
84 | 83 | anbi1d 633 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
85 | 84, 30 | bitrdi 290 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵)) |
86 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎) |
87 | 86 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
88 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎) |
89 | 88 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
90 | 87, 89 | anbi12d 634 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) |
91 | | anidm 568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵) |
92 | 90, 91 | bitrdi 290 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵)) |
93 | 82 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦)) |
94 | 93 | eleq2d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦))) |
95 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟) |
96 | 86 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎)) |
97 | 95, 96 | eleq12d 2832 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎))) |
98 | 86, 88 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎)) |
99 | 98 | eleq2d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎))) |
100 | 94, 97, 99 | 3anbi123d 1438 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) |
101 | 85, 92, 100 | 3anbi123d 1438 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))) |
102 | 21, 101 | syl5bb 286 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))) |
103 | 102 | anbi2d 632 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))) |
104 | 86 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (〈𝑦, 𝑦〉 · 𝑧) = (〈𝑦, 𝑦〉 · 𝑎)) |
105 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 ) |
106 | 104, 95, 105 | oveq123d 7234 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 )) |
107 | 106, 95 | eqeq12d 2753 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔 ↔ (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) |
108 | 103, 107 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) |
109 | 108 | sbiedvw 2100 |
. . . . . . . . . . 11
⊢ (((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) |
110 | 109 | sbiedvw 2100 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) |
111 | 110 | sbiedvw 2100 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) |
112 | | iscatd2.3 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
113 | 112 | sbt 2072 |
. . . . . . . . . . 11
⊢ [𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
114 | 113 | sbt 2072 |
. . . . . . . . . 10
⊢ [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
115 | 114 | sbt 2072 |
. . . . . . . . 9
⊢ [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
116 | 111, 115 | chvarvv 2007 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟) |
117 | 75, 76, 77, 81, 116 | syl13anc 1374 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟) |
118 | 117 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) |
119 | 118 | exlimdvv 1942 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) |
120 | 74, 119 | syl5bir 246 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) |
121 | 64, 73, 120 | mp2and 699 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟) |
122 | | id 22 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
123 | 122, 122 | oveq12d 7231 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧)) |
124 | 123 | neeq1d 3000 |
. . . . . 6
⊢ (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅)) |
125 | 68 | 3ad2ant1 1135 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅) |
126 | | simp23 1210 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧 ∈ 𝐵) |
127 | 124, 125,
126 | rspcdva 3539 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅) |
128 | | n0 4261 |
. . . . 5
⊢ ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧)) |
129 | 127, 128 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧)) |
130 | | eleq1w 2820 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
131 | 130 | 3anbi1d 1442 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) |
132 | | oveq1 7220 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎)) |
133 | 132 | eleq2d 2823 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎))) |
134 | 133 | anbi1d 633 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)))) |
135 | 134 | anbi1d 633 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) |
136 | 131, 135 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))) |
137 | 136 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))) |
138 | | opeq1 4784 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑎〉 = 〈𝑦, 𝑎〉) |
139 | 138 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑎〉 · 𝑧) = (〈𝑦, 𝑎〉 · 𝑧)) |
140 | 139 | oveqd 7230 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) = (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟)) |
141 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧)) |
142 | 140, 141 | eleq12d 2832 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))) |
143 | 137, 142 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))) |
144 | | df-3an 1091 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
145 | 21, 144 | bitri 278 |
. . . . . . . . . . . . . 14
⊢ (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
146 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎) |
147 | 146 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
148 | 147 | anbi2d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) |
149 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧) |
150 | 149 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)) |
151 | 150 | anbi2d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) |
152 | | anidm 568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵) |
153 | 151, 152 | bitrdi 290 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵)) |
154 | 148, 153 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵))) |
155 | | df-3an 1091 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵)) |
156 | 154, 155 | bitr4di 292 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) |
157 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟) |
158 | 146 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎)) |
159 | 157, 158 | eleq12d 2832 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎))) |
160 | 146 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧)) |
161 | 160 | eleq2d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧))) |
162 | 149 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧)) |
163 | 162 | eleq2d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧))) |
164 | 159, 161,
163 | 3anbi123d 1438 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) |
165 | | df-3an 1091 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) |
166 | 164, 165 | bitrdi 290 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) |
167 | 156, 166 | anbi12d 634 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))) |
168 | 145, 167 | syl5bb 286 |
. . . . . . . . . . . . 13
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))) |
169 | 168 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))) |
170 | 146 | opeq2d 4791 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑎〉) |
171 | 170 | oveq1d 7228 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑥, 𝑎〉 · 𝑧)) |
172 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔) |
173 | 171, 172,
157 | oveq123d 7234 |
. . . . . . . . . . . . 13
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) |
174 | 173 | eleq1d 2822 |
. . . . . . . . . . . 12
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))) |
175 | 169, 174 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))) |
176 | 175 | sbiedvw 2100 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))) |
177 | 176 | sbiedvw 2100 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))) |
178 | | iscatd2.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
179 | 178 | sbt 2072 |
. . . . . . . . . 10
⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
180 | 179 | sbt 2072 |
. . . . . . . . 9
⊢ [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
181 | 177, 180 | chvarvv 2007 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) |
182 | 143, 181 | chvarvv 2007 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)) |
183 | 182 | exp45 442 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))) |
184 | 183 | 3imp 1113 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))) |
185 | 184 | exlimdv 1941 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))) |
186 | 129, 185 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)) |
187 | 130 | anbi1d 633 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) |
188 | 187 | anbi1d 633 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))) |
189 | 133 | 3anbi1d 1442 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
190 | 188, 189 | 3anbi23d 1441 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
191 | 138 | oveq1d 7228 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑎〉 · 𝑤) = (〈𝑦, 𝑎〉 · 𝑤)) |
192 | 191 | oveqd 7230 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟)) |
193 | | opeq1 4784 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑧〉 = 〈𝑦, 𝑧〉) |
194 | 193 | oveq1d 7228 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑧〉 · 𝑤) = (〈𝑦, 𝑧〉 · 𝑤)) |
195 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝑘 = 𝑘) |
196 | 194, 195,
140 | oveq123d 7234 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟))) |
197 | 192, 196 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) ↔ ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟)))) |
198 | 190, 197 | imbi12d 348 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟))))) |
199 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎) |
200 | 199 | eleq1d 2822 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
201 | 200 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) |
202 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟) |
203 | 199 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎)) |
204 | 202, 203 | eleq12d 2832 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎))) |
205 | 199 | oveq1d 7228 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧)) |
206 | 205 | eleq2d 2823 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧))) |
207 | 204, 206 | 3anbi12d 1439 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
208 | 201, 207 | 3anbi13d 1440 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
209 | 21, 208 | syl5bb 286 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
210 | | df-3an 1091 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
211 | 209, 210 | bitrdi 290 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
212 | 211 | anbi2d 632 |
. . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))) |
213 | | 3anass 1097 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
214 | 212, 213 | bitr4di 292 |
. . . . . . 7
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
215 | 199 | opeq2d 4791 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑎〉) |
216 | 215 | oveq1d 7228 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑤) = (〈𝑥, 𝑎〉 · 𝑤)) |
217 | 199 | opeq1d 4790 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 〈𝑦, 𝑧〉 = 〈𝑎, 𝑧〉) |
218 | 217 | oveq1d 7228 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (〈𝑦, 𝑧〉 · 𝑤) = (〈𝑎, 𝑧〉 · 𝑤)) |
219 | 218 | oveqd 7230 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔) = (𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)) |
220 | 216, 219,
202 | oveq123d 7234 |
. . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟)) |
221 | 215 | oveq1d 7228 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑥, 𝑎〉 · 𝑧)) |
222 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔) |
223 | 221, 222,
202 | oveq123d 7234 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) |
224 | 223 | oveq2d 7229 |
. . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))) |
225 | 220, 224 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)))) |
226 | 214, 225 | imbi12d 348 |
. . . . . 6
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))))) |
227 | 226 | sbiedvw 2100 |
. . . . 5
⊢ (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))))) |
228 | | iscatd2.5 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
229 | 228 | sbt 2072 |
. . . . 5
⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
230 | 227, 229 | chvarvv 2007 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))) |
231 | 198, 230 | chvarvv 2007 |
. . 3
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟))) |
232 | 1, 2, 3, 4, 5, 61,
121, 186, 231 | iscatd 17176 |
. 2
⊢ (𝜑 → 𝐶 ∈ Cat) |
233 | 1, 2, 3, 232, 5, 61, 121 | catidd 17183 |
. 2
⊢ (𝜑 → (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )) |
234 | 232, 233 | jca 515 |
1
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))) |