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 | | ne0i 3880 |
. . . . . . 7
⊢ ( 1 ∈ (𝑦𝐻𝑦) → (𝑦𝐻𝑦) ≠ ∅) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝐻𝑦) ≠ ∅) |
8 | 7 | 3ad2antr1 1219 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅) |
9 | | n0 3890 |
. . . . 5
⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦)) |
10 | 8, 9 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦)) |
11 | | n0 3890 |
. . . . 5
⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) |
12 | 8, 11 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) |
13 | | eeanv 2170 |
. . . . 5
⊢
(∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))) |
14 | | simpll 786 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑) |
15 | | simplr2 1097 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎 ∈ 𝐵) |
16 | | simplr1 1096 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦 ∈ 𝐵) |
17 | 15, 16 | jca 553 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
18 | | simplr3 1098 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦)) |
19 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦)) |
20 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦)) |
21 | 18, 19, 20 | 3jca 1235 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) |
22 | | iscatd2.ps |
. . . . . . . . . . . . . . 15
⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
23 | | simplll 794 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎) |
24 | 23 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
25 | 24 | anbi1d 737 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
26 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
28 | | simplr 788 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦) |
29 | 28 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
30 | 27, 29 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
31 | | anidm 674 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵) |
32 | 30, 31 | syl6bb 275 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵)) |
33 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟) |
34 | 23 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦)) |
35 | 33, 34 | eleq12d 2682 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦))) |
36 | 26 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦)) |
37 | 36 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦))) |
38 | 26, 28 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦)) |
39 | 38 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦))) |
40 | 35, 37, 39 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) |
41 | 25, 32, 40 | 3anbi123d 1391 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))) |
42 | 22, 41 | syl5bb 271 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))) |
43 | 42 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))) |
44 | 23 | opeq1d 4346 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑦〉) |
45 | 44 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑦) = (〈𝑎, 𝑦〉 · 𝑦)) |
46 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 ) |
47 | 45, 46, 33 | oveq123d 6570 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟)) |
48 | 47, 33 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓 ↔ ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) |
49 | 43, 48 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) |
50 | 49 | sbiedv 2398 |
. . . . . . . . . . 11
⊢ (((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) |
51 | 50 | sbiedv 2398 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) |
52 | 51 | sbiedv 2398 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) |
53 | | iscatd2.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
54 | 53 | sbt 2407 |
. . . . . . . . . . 11
⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
55 | 54 | sbt 2407 |
. . . . . . . . . 10
⊢ [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
56 | 55 | sbt 2407 |
. . . . . . . . 9
⊢ [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) |
57 | 52, 56 | chvarv 2251 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟) |
58 | 14, 17, 16, 21, 57 | syl13anc 1320 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟) |
59 | 58 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) |
60 | 59 | exlimdvv 1849 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) |
61 | 13, 60 | syl5bir 232 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) |
62 | 10, 12, 61 | mp2and 711 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟) |
63 | 7 | 3ad2antr1 1219 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅) |
64 | | n0 3890 |
. . . . 5
⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦)) |
65 | 63, 64 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦)) |
66 | | simpr2 1061 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎 ∈ 𝐵) |
67 | 7 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅) |
68 | 67 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅) |
69 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → 𝑦 = 𝑎) |
70 | 69, 69 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎)) |
71 | 70 | neeq1d 2841 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅)) |
72 | 71 | rspcv 3278 |
. . . . . 6
⊢ (𝑎 ∈ 𝐵 → (∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅ → (𝑎𝐻𝑎) ≠ ∅)) |
73 | 66, 68, 72 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅) |
74 | | n0 3890 |
. . . . 5
⊢ ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) |
75 | 73, 74 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) |
76 | | eeanv 2170 |
. . . . 5
⊢
(∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))) |
77 | | simpll 786 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑) |
78 | | simplr1 1096 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦 ∈ 𝐵) |
79 | | simplr2 1097 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎 ∈ 𝐵) |
80 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦)) |
81 | | simplr3 1098 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎)) |
82 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎)) |
83 | 80, 81, 82 | 3jca 1235 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) |
84 | | simplll 794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦) |
85 | 84 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
86 | 85 | anbi1d 737 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
87 | 86, 31 | syl6bb 275 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵)) |
88 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎) |
89 | 88 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
90 | | simplr 788 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎) |
91 | 90 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
92 | 89, 91 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) |
93 | | anidm 674 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵) |
94 | 92, 93 | syl6bb 275 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵)) |
95 | 84 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦)) |
96 | 95 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦))) |
97 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟) |
98 | 88 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎)) |
99 | 97, 98 | eleq12d 2682 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎))) |
100 | 88, 90 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎)) |
101 | 100 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎))) |
102 | 96, 99, 101 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) |
103 | 87, 94, 102 | 3anbi123d 1391 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))) |
104 | 22, 103 | syl5bb 271 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))) |
105 | 104 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))) |
106 | 88 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (〈𝑦, 𝑦〉 · 𝑧) = (〈𝑦, 𝑦〉 · 𝑎)) |
107 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 ) |
108 | 106, 97, 107 | oveq123d 6570 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 )) |
109 | 108, 97 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔 ↔ (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) |
110 | 105, 109 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) |
111 | 110 | sbiedv 2398 |
. . . . . . . . . . 11
⊢ (((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) |
112 | 111 | sbiedv 2398 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) |
113 | 112 | sbiedv 2398 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) |
114 | | iscatd2.3 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
115 | 114 | sbt 2407 |
. . . . . . . . . . 11
⊢ [𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
116 | 115 | sbt 2407 |
. . . . . . . . . 10
⊢ [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
117 | 116 | sbt 2407 |
. . . . . . . . 9
⊢ [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) |
118 | 113, 117 | chvarv 2251 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟) |
119 | 77, 78, 79, 83, 118 | syl13anc 1320 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟) |
120 | 119 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) |
121 | 120 | exlimdvv 1849 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) |
122 | 76, 121 | syl5bir 232 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) |
123 | 65, 75, 122 | mp2and 711 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟) |
124 | 67 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅) |
125 | | simp23 1089 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧 ∈ 𝐵) |
126 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
127 | 126, 126 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧)) |
128 | 127 | neeq1d 2841 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅)) |
129 | 128 | rspccva 3281 |
. . . . . 6
⊢
((∀𝑦 ∈
𝐵 (𝑦𝐻𝑦) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → (𝑧𝐻𝑧) ≠ ∅) |
130 | 124, 125,
129 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅) |
131 | | n0 3890 |
. . . . 5
⊢ ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧)) |
132 | 130, 131 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧)) |
133 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
134 | 133 | 3anbi1d 1395 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) |
135 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎)) |
136 | 135 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎))) |
137 | 136 | anbi1d 737 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)))) |
138 | 137 | anbi1d 737 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) |
139 | 134, 138 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))) |
140 | 139 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))) |
141 | | opeq1 4340 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑎〉 = 〈𝑦, 𝑎〉) |
142 | 141 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑎〉 · 𝑧) = (〈𝑦, 𝑎〉 · 𝑧)) |
143 | 142 | oveqd 6566 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) = (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟)) |
144 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧)) |
145 | 143, 144 | eleq12d 2682 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))) |
146 | 140, 145 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))) |
147 | | df-3an 1033 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
148 | 22, 147 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
149 | | simpll 786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎) |
150 | 149 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
151 | 150 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) |
152 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧) |
153 | 152 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)) |
154 | 153 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) |
155 | | anidm 674 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵) |
156 | 154, 155 | syl6bb 275 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵)) |
157 | 151, 156 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵))) |
158 | | df-3an 1033 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵)) |
159 | 157, 158 | syl6bbr 277 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) |
160 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟) |
161 | 149 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎)) |
162 | 160, 161 | eleq12d 2682 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎))) |
163 | 149 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧)) |
164 | 163 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧))) |
165 | 152 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧)) |
166 | 165 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧))) |
167 | 162, 164,
166 | 3anbi123d 1391 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) |
168 | | df-3an 1033 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) |
169 | 167, 168 | syl6bb 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) |
170 | 159, 169 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))) |
171 | 148, 170 | syl5bb 271 |
. . . . . . . . . . . . 13
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))) |
172 | 171 | anbi2d 736 |
. . . . . . . . . . . 12
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))) |
173 | 149 | opeq2d 4347 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑎〉) |
174 | 173 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑥, 𝑎〉 · 𝑧)) |
175 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔) |
176 | 174, 175,
160 | oveq123d 6570 |
. . . . . . . . . . . . 13
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) |
177 | 176 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))) |
178 | 172, 177 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))) |
179 | 178 | sbiedv 2398 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))) |
180 | 179 | sbiedv 2398 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))) |
181 | | iscatd2.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
182 | 181 | sbt 2407 |
. . . . . . . . . 10
⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
183 | 182 | sbt 2407 |
. . . . . . . . 9
⊢ [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) |
184 | 180, 183 | chvarv 2251 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) |
185 | 146, 184 | chvarv 2251 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)) |
186 | 185 | exp45 640 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))) |
187 | 186 | 3imp 1249 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))) |
188 | 187 | exlimdv 1848 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))) |
189 | 132, 188 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)) |
190 | 133 | anbi1d 737 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) |
191 | 190 | anbi1d 737 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))) |
192 | 136 | 3anbi1d 1395 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
193 | 191, 192 | 3anbi23d 1394 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
194 | 141 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑎〉 · 𝑤) = (〈𝑦, 𝑎〉 · 𝑤)) |
195 | 194 | oveqd 6566 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟)) |
196 | | opeq1 4340 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑧〉 = 〈𝑦, 𝑧〉) |
197 | 196 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑧〉 · 𝑤) = (〈𝑦, 𝑧〉 · 𝑤)) |
198 | | eqidd 2611 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝑘 = 𝑘) |
199 | 197, 198,
143 | oveq123d 6570 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟))) |
200 | 195, 199 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) ↔ ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟)))) |
201 | 193, 200 | imbi12d 333 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟))))) |
202 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎) |
203 | 202 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) |
204 | 203 | anbi2d 736 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) |
205 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟) |
206 | 202 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎)) |
207 | 205, 206 | eleq12d 2682 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎))) |
208 | 202 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧)) |
209 | 208 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧))) |
210 | 207, 209 | 3anbi12d 1392 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
211 | 204, 210 | 3anbi13d 1393 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
212 | 22, 211 | syl5bb 271 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
213 | | df-3an 1033 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) |
214 | 212, 213 | syl6bb 275 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
215 | 214 | anbi2d 736 |
. . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))) |
216 | | 3anass 1035 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
217 | 215, 216 | syl6bbr 277 |
. . . . . . 7
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) |
218 | 202 | opeq2d 4347 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑎〉) |
219 | 218 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑤) = (〈𝑥, 𝑎〉 · 𝑤)) |
220 | 202 | opeq1d 4346 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 〈𝑦, 𝑧〉 = 〈𝑎, 𝑧〉) |
221 | 220 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (〈𝑦, 𝑧〉 · 𝑤) = (〈𝑎, 𝑧〉 · 𝑤)) |
222 | 221 | oveqd 6566 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔) = (𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)) |
223 | 219, 222,
205 | oveq123d 6570 |
. . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟)) |
224 | 218 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑥, 𝑎〉 · 𝑧)) |
225 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔) |
226 | 224, 225,
205 | oveq123d 6570 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) |
227 | 226 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))) |
228 | 223, 227 | eqeq12d 2625 |
. . . . . . 7
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)))) |
229 | 217, 228 | imbi12d 333 |
. . . . . 6
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))))) |
230 | 229 | sbiedv 2398 |
. . . . 5
⊢ (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))))) |
231 | | iscatd2.5 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
232 | 231 | sbt 2407 |
. . . . 5
⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) |
233 | 230, 232 | chvarv 2251 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))) |
234 | 201, 233 | chvarv 2251 |
. . 3
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟))) |
235 | 1, 2, 3, 4, 5, 62,
123, 189, 234 | iscatd 16157 |
. 2
⊢ (𝜑 → 𝐶 ∈ Cat) |
236 | 1, 2, 3, 235, 5, 62, 123 | catidd 16164 |
. 2
⊢ (𝜑 → (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )) |
237 | 235, 236 | jca 553 |
1
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))) |