| 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 4341 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝐻𝑦) ≠ ∅) | 
| 7 | 6 | 3ad2antr1 1188 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (𝑦𝐻𝑦) ≠ ∅) | 
| 8 |  | n0 4352 | . . . . 5
⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦)) | 
| 9 | 7, 8 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑔 𝑔 ∈ (𝑦𝐻𝑦)) | 
| 10 |  | n0 4352 | . . . . 5
⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) | 
| 11 | 7, 10 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) | 
| 12 |  | exdistrv 1954 | . . . . 5
⊢
(∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) ↔ (∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦))) | 
| 13 |  | simpll 766 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝜑) | 
| 14 |  | simplr2 1216 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑎 ∈ 𝐵) | 
| 15 |  | simplr1 1215 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑦 ∈ 𝐵) | 
| 16 | 14, 15 | jca 511 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) | 
| 17 |  | simplr3 1217 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑟 ∈ (𝑎𝐻𝑦)) | 
| 18 |  | simprl 770 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑔 ∈ (𝑦𝐻𝑦)) | 
| 19 |  | simprr 772 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → 𝑘 ∈ (𝑦𝐻𝑦)) | 
| 20 | 17, 18, 19 | 3jca 1128 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) | 
| 21 |  | iscatd2.ps | . . . . . . . . . . . . . . 15
⊢ (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) | 
| 22 |  | simplll 774 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑥 = 𝑎) | 
| 23 | 22 | eleq1d 2825 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) | 
| 24 | 23 | anbi1d 631 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) | 
| 25 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑧 = 𝑦) | 
| 26 | 25 | eleq1d 2825 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | 
| 27 |  | simplr 768 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑦) | 
| 28 | 27 | eleq1d 2825 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | 
| 29 | 26, 28 | anbi12d 632 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) | 
| 30 |  | anidm 564 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵) | 
| 31 | 29, 30 | bitrdi 287 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵)) | 
| 32 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟) | 
| 33 | 22 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑎𝐻𝑦)) | 
| 34 | 32, 33 | eleq12d 2834 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑎𝐻𝑦))) | 
| 35 | 25 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑦)) | 
| 36 | 35 | eleq2d 2826 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑦𝐻𝑦))) | 
| 37 | 25, 27 | oveq12d 7450 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑦𝐻𝑦)) | 
| 38 | 37 | eleq2d 2826 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑦𝐻𝑦))) | 
| 39 | 34, 36, 38 | 3anbi123d 1437 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) | 
| 40 | 24, 31, 39 | 3anbi123d 1437 | . . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))) | 
| 41 | 21, 40 | bitrid 283 | . . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))))) | 
| 42 | 41 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))))) | 
| 43 | 22 | opeq1d 4878 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑦〉) | 
| 44 | 43 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑦) = (〈𝑎, 𝑦〉 · 𝑦)) | 
| 45 |  | eqidd 2737 | . . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → 1 = 1 ) | 
| 46 | 44, 45, 32 | oveq123d 7453 | . . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟)) | 
| 47 | 46, 32 | eqeq12d 2752 | . . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓 ↔ ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) | 
| 48 | 42, 47 | imbi12d 344 | . . . . . . . . . . . 12
⊢ ((((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) | 
| 49 | 48 | sbiedvw 2094 | . . . . . . . . . . 11
⊢ (((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) ∧ 𝑤 = 𝑦) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) | 
| 50 | 49 | sbiedvw 2094 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑎 ∧ 𝑧 = 𝑦) → ([𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) | 
| 51 | 50 | sbiedvw 2094 | . . . . . . . . 9
⊢ (𝑥 = 𝑎 → ([𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) ↔ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟))) | 
| 52 |  | iscatd2.2 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) | 
| 53 | 52 | sbt 2065 | . . . . . . . . . . 11
⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) | 
| 54 | 53 | sbt 2065 | . . . . . . . . . 10
⊢ [𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) | 
| 55 | 54 | sbt 2065 | . . . . . . . . 9
⊢ [𝑦 / 𝑧][𝑦 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ( 1 (〈𝑥, 𝑦〉 · 𝑦)𝑓) = 𝑓) | 
| 56 | 51, 55 | chvarvv 1997 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵 ∧ (𝑟 ∈ (𝑎𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟) | 
| 57 | 13, 16, 15, 20, 56 | syl13anc 1373 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) ∧ (𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟) | 
| 58 | 57 | ex 412 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) | 
| 59 | 58 | exlimdvv 1933 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → (∃𝑔∃𝑘(𝑔 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) | 
| 60 | 12, 59 | biimtrrid 243 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ((∃𝑔 𝑔 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑦𝐻𝑦)) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟)) | 
| 61 | 9, 11, 60 | mp2and 699 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑎𝐻𝑦))) → ( 1 (〈𝑎, 𝑦〉 · 𝑦)𝑟) = 𝑟) | 
| 62 | 6 | 3ad2antr1 1188 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑦𝐻𝑦) ≠ ∅) | 
| 63 |  | n0 4352 | . . . . 5
⊢ ((𝑦𝐻𝑦) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦)) | 
| 64 | 62, 63 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑓 𝑓 ∈ (𝑦𝐻𝑦)) | 
| 65 |  | id 22 | . . . . . . . 8
⊢ (𝑦 = 𝑎 → 𝑦 = 𝑎) | 
| 66 | 65, 65 | oveq12d 7450 | . . . . . . 7
⊢ (𝑦 = 𝑎 → (𝑦𝐻𝑦) = (𝑎𝐻𝑎)) | 
| 67 | 66 | neeq1d 2999 | . . . . . 6
⊢ (𝑦 = 𝑎 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑎𝐻𝑎) ≠ ∅)) | 
| 68 | 6 | ralrimiva 3145 | . . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅) | 
| 69 | 68 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅) | 
| 70 |  | simpr2 1195 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → 𝑎 ∈ 𝐵) | 
| 71 | 67, 69, 70 | rspcdva 3622 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑎𝐻𝑎) ≠ ∅) | 
| 72 |  | n0 4352 | . . . . 5
⊢ ((𝑎𝐻𝑎) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) | 
| 73 | 71, 72 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) | 
| 74 |  | exdistrv 1954 | . . . . 5
⊢
(∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) ↔ (∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎))) | 
| 75 |  | simpll 766 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝜑) | 
| 76 |  | simplr1 1215 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑦 ∈ 𝐵) | 
| 77 |  | simplr2 1216 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑎 ∈ 𝐵) | 
| 78 |  | simprl 770 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑓 ∈ (𝑦𝐻𝑦)) | 
| 79 |  | simplr3 1217 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑟 ∈ (𝑦𝐻𝑎)) | 
| 80 |  | simprr 772 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → 𝑘 ∈ (𝑎𝐻𝑎)) | 
| 81 | 78, 79, 80 | 3jca 1128 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) | 
| 82 |  | simplll 774 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑥 = 𝑦) | 
| 83 | 82 | eleq1d 2825 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | 
| 84 | 83 | anbi1d 631 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) | 
| 85 | 84, 30 | bitrdi 287 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ 𝑦 ∈ 𝐵)) | 
| 86 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑧 = 𝑎) | 
| 87 | 86 | eleq1d 2825 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) | 
| 88 |  | simplr 768 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑤 = 𝑎) | 
| 89 | 88 | eleq1d 2825 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) | 
| 90 | 87, 89 | anbi12d 632 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) | 
| 91 |  | anidm 564 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵) | 
| 92 | 90, 91 | bitrdi 287 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑎 ∈ 𝐵)) | 
| 93 | 82 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑥𝐻𝑦) = (𝑦𝐻𝑦)) | 
| 94 | 93 | eleq2d 2826 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ (𝑦𝐻𝑦))) | 
| 95 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 𝑔 = 𝑟) | 
| 96 | 86 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑦𝐻𝑧) = (𝑦𝐻𝑎)) | 
| 97 | 95, 96 | eleq12d 2834 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑟 ∈ (𝑦𝐻𝑎))) | 
| 98 | 86, 88 | oveq12d 7450 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑧𝐻𝑤) = (𝑎𝐻𝑎)) | 
| 99 | 98 | eleq2d 2826 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑎𝐻𝑎))) | 
| 100 | 94, 97, 99 | 3anbi123d 1437 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) | 
| 101 | 85, 92, 100 | 3anbi123d 1437 | . . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))) | 
| 102 | 21, 101 | bitrid 283 | . . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝜓 ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎))))) | 
| 103 | 102 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))))) | 
| 104 | 86 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (〈𝑦, 𝑦〉 · 𝑧) = (〈𝑦, 𝑦〉 · 𝑎)) | 
| 105 |  | eqidd 2737 | . . . . . . . . . . . . . . 15
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → 1 = 1 ) | 
| 106 | 104, 95, 105 | oveq123d 7453 | . . . . . . . . . . . . . 14
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 )) | 
| 107 | 106, 95 | eqeq12d 2752 | . . . . . . . . . . . . 13
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → ((𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔 ↔ (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) | 
| 108 | 103, 107 | imbi12d 344 | . . . . . . . . . . . 12
⊢ ((((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) ∧ 𝑔 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) | 
| 109 | 108 | sbiedvw 2094 | . . . . . . . . . . 11
⊢ (((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) ∧ 𝑤 = 𝑎) → ([𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) | 
| 110 | 109 | sbiedvw 2094 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑦 ∧ 𝑧 = 𝑎) → ([𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) | 
| 111 | 110 | sbiedvw 2094 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → ([𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) ↔ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟))) | 
| 112 |  | iscatd2.3 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) | 
| 113 | 112 | sbt 2065 | . . . . . . . . . . 11
⊢ [𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) | 
| 114 | 113 | sbt 2065 | . . . . . . . . . 10
⊢ [𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) | 
| 115 | 114 | sbt 2065 | . . . . . . . . 9
⊢ [𝑎 / 𝑧][𝑎 / 𝑤][𝑟 / 𝑔]((𝜑 ∧ 𝜓) → (𝑔(〈𝑦, 𝑦〉 · 𝑧) 1 ) = 𝑔) | 
| 116 | 111, 115 | chvarvv 1997 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑘 ∈ (𝑎𝐻𝑎)))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟) | 
| 117 | 75, 76, 77, 81, 116 | syl13anc 1373 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) ∧ (𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟) | 
| 118 | 117 | ex 412 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) | 
| 119 | 118 | exlimdvv 1933 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (∃𝑓∃𝑘(𝑓 ∈ (𝑦𝐻𝑦) ∧ 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) | 
| 120 | 74, 119 | biimtrrid 243 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → ((∃𝑓 𝑓 ∈ (𝑦𝐻𝑦) ∧ ∃𝑘 𝑘 ∈ (𝑎𝐻𝑎)) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟)) | 
| 121 | 64, 73, 120 | mp2and 699 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑟 ∈ (𝑦𝐻𝑎))) → (𝑟(〈𝑦, 𝑦〉 · 𝑎) 1 ) = 𝑟) | 
| 122 |  | id 22 | . . . . . . . 8
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) | 
| 123 | 122, 122 | oveq12d 7450 | . . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑦𝐻𝑦) = (𝑧𝐻𝑧)) | 
| 124 | 123 | neeq1d 2999 | . . . . . 6
⊢ (𝑦 = 𝑧 → ((𝑦𝐻𝑦) ≠ ∅ ↔ (𝑧𝐻𝑧) ≠ ∅)) | 
| 125 | 68 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∀𝑦 ∈ 𝐵 (𝑦𝐻𝑦) ≠ ∅) | 
| 126 |  | simp23 1208 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → 𝑧 ∈ 𝐵) | 
| 127 | 124, 125,
126 | rspcdva 3622 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑧𝐻𝑧) ≠ ∅) | 
| 128 |  | n0 4352 | . . . . 5
⊢ ((𝑧𝐻𝑧) ≠ ∅ ↔ ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧)) | 
| 129 | 127, 128 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → ∃𝑘 𝑘 ∈ (𝑧𝐻𝑧)) | 
| 130 |  | eleq1w 2823 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | 
| 131 | 130 | 3anbi1d 1441 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) | 
| 132 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑎) = (𝑦𝐻𝑎)) | 
| 133 | 132 | eleq2d 2826 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑟 ∈ (𝑥𝐻𝑎) ↔ 𝑟 ∈ (𝑦𝐻𝑎))) | 
| 134 | 133 | anbi1d 631 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)))) | 
| 135 | 134 | anbi1d 631 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) | 
| 136 | 131, 135 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))) | 
| 137 | 136 | anbi2d 630 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))) | 
| 138 |  | opeq1 4872 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑎〉 = 〈𝑦, 𝑎〉) | 
| 139 | 138 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑎〉 · 𝑧) = (〈𝑦, 𝑎〉 · 𝑧)) | 
| 140 | 139 | oveqd 7449 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) = (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟)) | 
| 141 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥𝐻𝑧) = (𝑦𝐻𝑧)) | 
| 142 | 140, 141 | eleq12d 2834 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧) ↔ (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))) | 
| 143 | 137, 142 | imbi12d 344 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)))) | 
| 144 |  | df-3an 1088 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) | 
| 145 | 21, 144 | bitri 275 | . . . . . . . . . . . . . 14
⊢ (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) | 
| 146 |  | simpll 766 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎) | 
| 147 | 146 | eleq1d 2825 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) | 
| 148 | 147 | anbi2d 630 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) | 
| 149 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑤 = 𝑧) | 
| 150 | 149 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑤 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)) | 
| 151 | 150 | anbi2d 630 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) | 
| 152 |  | anidm 564 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵) | 
| 153 | 151, 152 | bitrdi 287 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ 𝑧 ∈ 𝐵)) | 
| 154 | 148, 153 | anbi12d 632 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵))) | 
| 155 |  | df-3an 1088 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵)) | 
| 156 | 154, 155 | bitr4di 289 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) | 
| 157 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟) | 
| 158 | 146 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎)) | 
| 159 | 157, 158 | eleq12d 2834 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎))) | 
| 160 | 146 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧)) | 
| 161 | 160 | eleq2d 2826 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧))) | 
| 162 | 149 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑧𝐻𝑤) = (𝑧𝐻𝑧)) | 
| 163 | 162 | eleq2d 2826 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ (𝑧𝐻𝑧))) | 
| 164 | 159, 161,
163 | 3anbi123d 1437 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) | 
| 165 |  | df-3an 1088 | . . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑧)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))) | 
| 166 | 164, 165 | bitrdi 287 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) | 
| 167 | 156, 166 | anbi12d 632 | . . . . . . . . . . . . . 14
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))) | 
| 168 | 145, 167 | bitrid 283 | . . . . . . . . . . . . 13
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧))))) | 
| 169 | 168 | anbi2d 630 | . . . . . . . . . . . 12
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))))) | 
| 170 | 146 | opeq2d 4879 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑎〉) | 
| 171 | 170 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑥, 𝑎〉 · 𝑧)) | 
| 172 |  | eqidd 2737 | . . . . . . . . . . . . . 14
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔) | 
| 173 | 171, 172,
157 | oveq123d 7453 | . . . . . . . . . . . . 13
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) | 
| 174 | 173 | eleq1d 2825 | . . . . . . . . . . . 12
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → ((𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ↔ (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧))) | 
| 175 | 169, 174 | imbi12d 344 | . . . . . . . . . . 11
⊢ (((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))) | 
| 176 | 175 | sbiedvw 2094 | . . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑤 = 𝑧) → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))) | 
| 177 | 176 | sbiedvw 2094 | . . . . . . . . 9
⊢ (𝑦 = 𝑎 → ([𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)))) | 
| 178 |  | iscatd2.4 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | 
| 179 | 178 | sbt 2065 | . . . . . . . . . 10
⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | 
| 180 | 179 | sbt 2065 | . . . . . . . . 9
⊢ [𝑧 / 𝑤][𝑟 / 𝑓]((𝜑 ∧ 𝜓) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) ∈ (𝑥𝐻𝑧)) | 
| 181 | 177, 180 | chvarvv 1997 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟) ∈ (𝑥𝐻𝑧)) | 
| 182 | 143, 181 | chvarvv 1997 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) ∧ 𝑘 ∈ (𝑧𝐻𝑧)))) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)) | 
| 183 | 182 | exp45 438 | . . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧)) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))))) | 
| 184 | 183 | 3imp 1110 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))) | 
| 185 | 184 | exlimdv 1932 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (∃𝑘 𝑘 ∈ (𝑧𝐻𝑧) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧))) | 
| 186 | 129, 185 | mpd 15 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧))) → (𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟) ∈ (𝑦𝐻𝑧)) | 
| 187 | 130 | anbi1d 631 | . . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) | 
| 188 | 187 | anbi1d 631 | . . . . . 6
⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)))) | 
| 189 | 133 | 3anbi1d 1441 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) | 
| 190 | 188, 189 | 3anbi23d 1440 | . . . . 5
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) | 
| 191 | 138 | oveq1d 7447 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑎〉 · 𝑤) = (〈𝑦, 𝑎〉 · 𝑤)) | 
| 192 | 191 | oveqd 7449 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟)) | 
| 193 |  | opeq1 4872 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑧〉 = 〈𝑦, 𝑧〉) | 
| 194 | 193 | oveq1d 7447 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (〈𝑥, 𝑧〉 · 𝑤) = (〈𝑦, 𝑧〉 · 𝑤)) | 
| 195 |  | eqidd 2737 | . . . . . . 7
⊢ (𝑥 = 𝑦 → 𝑘 = 𝑘) | 
| 196 | 194, 195,
140 | oveq123d 7453 | . . . . . 6
⊢ (𝑥 = 𝑦 → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟))) | 
| 197 | 192, 196 | eqeq12d 2752 | . . . . 5
⊢ (𝑥 = 𝑦 → (((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) ↔ ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟)))) | 
| 198 | 190, 197 | imbi12d 344 | . . . 4
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))) ↔ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟))))) | 
| 199 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑦 = 𝑎) | 
| 200 | 199 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦 ∈ 𝐵 ↔ 𝑎 ∈ 𝐵)) | 
| 201 | 200 | anbi2d 630 | . . . . . . . . . . . 12
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵))) | 
| 202 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑓 = 𝑟) | 
| 203 | 199 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑥𝐻𝑦) = (𝑥𝐻𝑎)) | 
| 204 | 202, 203 | eleq12d 2834 | . . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑟 ∈ (𝑥𝐻𝑎))) | 
| 205 | 199 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑦𝐻𝑧) = (𝑎𝐻𝑧)) | 
| 206 | 205 | eleq2d 2826 | . . . . . . . . . . . . 13
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ (𝑎𝐻𝑧))) | 
| 207 | 204, 206 | 3anbi12d 1438 | . . . . . . . . . . . 12
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) | 
| 208 | 201, 207 | 3anbi13d 1439 | . . . . . . . . . . 11
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) | 
| 209 | 21, 208 | bitrid 283 | . . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) | 
| 210 |  | df-3an 1088 | . . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))) | 
| 211 | 209, 210 | bitrdi 287 | . . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝜓 ↔ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) | 
| 212 | 211 | anbi2d 630 | . . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)))))) | 
| 213 |  | 3anass 1094 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (𝜑 ∧ (((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) | 
| 214 | 212, 213 | bitr4di 289 | . . . . . . 7
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))) | 
| 215 | 199 | opeq2d 4879 | . . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 〈𝑥, 𝑦〉 = 〈𝑥, 𝑎〉) | 
| 216 | 215 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑤) = (〈𝑥, 𝑎〉 · 𝑤)) | 
| 217 | 199 | opeq1d 4878 | . . . . . . . . . . 11
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 〈𝑦, 𝑧〉 = 〈𝑎, 𝑧〉) | 
| 218 | 217 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (〈𝑦, 𝑧〉 · 𝑤) = (〈𝑎, 𝑧〉 · 𝑤)) | 
| 219 | 218 | oveqd 7449 | . . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔) = (𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)) | 
| 220 | 216, 219,
202 | oveq123d 7453 | . . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟)) | 
| 221 | 215 | oveq1d 7447 | . . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (〈𝑥, 𝑦〉 · 𝑧) = (〈𝑥, 𝑎〉 · 𝑧)) | 
| 222 |  | eqidd 2737 | . . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → 𝑔 = 𝑔) | 
| 223 | 221, 222,
202 | oveq123d 7453 | . . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓) = (𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)) | 
| 224 | 223 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))) | 
| 225 | 220, 224 | eqeq12d 2752 | . . . . . . 7
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓)) ↔ ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟)))) | 
| 226 | 214, 225 | imbi12d 344 | . . . . . 6
⊢ ((𝑦 = 𝑎 ∧ 𝑓 = 𝑟) → (((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))))) | 
| 227 | 226 | sbiedvw 2094 | . . . . 5
⊢ (𝑦 = 𝑎 → ([𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) ↔ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))))) | 
| 228 |  | iscatd2.5 | . . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) | 
| 229 | 228 | sbt 2065 | . . . . 5
⊢ [𝑟 / 𝑓]((𝜑 ∧ 𝜓) → ((𝑘(〈𝑦, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑦〉 · 𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑦〉 · 𝑧)𝑓))) | 
| 230 | 227, 229 | chvarvv 1997 | . . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑥𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑥, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑥, 𝑧〉 · 𝑤)(𝑔(〈𝑥, 𝑎〉 · 𝑧)𝑟))) | 
| 231 | 198, 230 | chvarvv 1997 | . . 3
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ (𝑟 ∈ (𝑦𝐻𝑎) ∧ 𝑔 ∈ (𝑎𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) → ((𝑘(〈𝑎, 𝑧〉 · 𝑤)𝑔)(〈𝑦, 𝑎〉 · 𝑤)𝑟) = (𝑘(〈𝑦, 𝑧〉 · 𝑤)(𝑔(〈𝑦, 𝑎〉 · 𝑧)𝑟))) | 
| 232 | 1, 2, 3, 4, 5, 61,
121, 186, 231 | iscatd 17717 | . 2
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 233 | 1, 2, 3, 232, 5, 61, 121 | catidd 17724 | . 2
⊢ (𝜑 → (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 )) | 
| 234 | 232, 233 | jca 511 | 1
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (Id‘𝐶) = (𝑦 ∈ 𝐵 ↦ 1 ))) |