| Step | Hyp | Ref
| Expression |
| 1 | | rngidpropd.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) |
| 2 | 1 | anassrs 467 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) |
| 3 | 2 | eqeq1d 2739 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((𝑥(.r‘𝐾)𝑦) = 𝑧 ↔ (𝑥(.r‘𝐿)𝑦) = 𝑧)) |
| 4 | 3 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) → ((𝑥(.r‘𝐾)𝑦) = 𝑧 ↔ (𝑥(.r‘𝐿)𝑦) = 𝑧)) |
| 5 | 4 | rexbidva 3177 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐾)𝑦) = 𝑧 ↔ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐿)𝑦) = 𝑧)) |
| 6 | 5 | pm5.32da 579 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐾)𝑦) = 𝑧) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐿)𝑦) = 𝑧))) |
| 7 | | rngidpropd.1 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
| 8 | 7 | eleq2d 2827 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐾))) |
| 9 | 7 | rexeqdv 3327 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐾)𝑦) = 𝑧 ↔ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧)) |
| 10 | 8, 9 | anbi12d 632 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐾)𝑦) = 𝑧) ↔ (𝑦 ∈ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧))) |
| 11 | | rngidpropd.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
| 12 | 11 | eleq2d 2827 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐿))) |
| 13 | 11 | rexeqdv 3327 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐿)𝑦) = 𝑧 ↔ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧)) |
| 14 | 12, 13 | anbi12d 632 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐿)𝑦) = 𝑧) ↔ (𝑦 ∈ (Base‘𝐿) ∧ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧))) |
| 15 | 6, 10, 14 | 3bitr3d 309 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧) ↔ (𝑦 ∈ (Base‘𝐿) ∧ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧))) |
| 16 | 15 | opabbidv 5209 |
. 2
⊢ (𝜑 → {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ (Base‘𝐿) ∧ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧)}) |
| 17 | | eqid 2737 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 18 | | eqid 2737 |
. . 3
⊢
(∥r‘𝐾) = (∥r‘𝐾) |
| 19 | | eqid 2737 |
. . 3
⊢
(.r‘𝐾) = (.r‘𝐾) |
| 20 | 17, 18, 19 | dvdsrval 20361 |
. 2
⊢
(∥r‘𝐾) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧)} |
| 21 | | eqid 2737 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
| 22 | | eqid 2737 |
. . 3
⊢
(∥r‘𝐿) = (∥r‘𝐿) |
| 23 | | eqid 2737 |
. . 3
⊢
(.r‘𝐿) = (.r‘𝐿) |
| 24 | 21, 22, 23 | dvdsrval 20361 |
. 2
⊢
(∥r‘𝐿) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ (Base‘𝐿) ∧ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧)} |
| 25 | 16, 20, 24 | 3eqtr4g 2802 |
1
⊢ (𝜑 →
(∥r‘𝐾) = (∥r‘𝐿)) |