Step | Hyp | Ref
| Expression |
1 | | rngidpropd.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) |
2 | 1 | anassrs 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) |
3 | 2 | eqeq1d 2741 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((𝑥(.r‘𝐾)𝑦) = 𝑧 ↔ (𝑥(.r‘𝐿)𝑦) = 𝑧)) |
4 | 3 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) → ((𝑥(.r‘𝐾)𝑦) = 𝑧 ↔ (𝑥(.r‘𝐿)𝑦) = 𝑧)) |
5 | 4 | rexbidva 3207 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐾)𝑦) = 𝑧 ↔ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐿)𝑦) = 𝑧)) |
6 | 5 | pm5.32da 582 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐾)𝑦) = 𝑧) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐿)𝑦) = 𝑧))) |
7 | | rngidpropd.1 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
8 | 7 | eleq2d 2819 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐾))) |
9 | 7 | rexeqdv 3318 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐾)𝑦) = 𝑧 ↔ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧)) |
10 | 8, 9 | anbi12d 634 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐾)𝑦) = 𝑧) ↔ (𝑦 ∈ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧))) |
11 | | rngidpropd.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
12 | 11 | eleq2d 2819 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐿))) |
13 | 11 | rexeqdv 3318 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐿)𝑦) = 𝑧 ↔ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧)) |
14 | 12, 13 | anbi12d 634 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐵 (𝑥(.r‘𝐿)𝑦) = 𝑧) ↔ (𝑦 ∈ (Base‘𝐿) ∧ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧))) |
15 | 6, 10, 14 | 3bitr3d 312 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧) ↔ (𝑦 ∈ (Base‘𝐿) ∧ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧))) |
16 | 15 | opabbidv 5106 |
. 2
⊢ (𝜑 → {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ (Base‘𝐿) ∧ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧)}) |
17 | | eqid 2739 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
18 | | eqid 2739 |
. . 3
⊢
(∥r‘𝐾) = (∥r‘𝐾) |
19 | | eqid 2739 |
. . 3
⊢
(.r‘𝐾) = (.r‘𝐾) |
20 | 17, 18, 19 | dvdsrval 19530 |
. 2
⊢
(∥r‘𝐾) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(𝑥(.r‘𝐾)𝑦) = 𝑧)} |
21 | | eqid 2739 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
22 | | eqid 2739 |
. . 3
⊢
(∥r‘𝐿) = (∥r‘𝐿) |
23 | | eqid 2739 |
. . 3
⊢
(.r‘𝐿) = (.r‘𝐿) |
24 | 21, 22, 23 | dvdsrval 19530 |
. 2
⊢
(∥r‘𝐿) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ (Base‘𝐿) ∧ ∃𝑥 ∈ (Base‘𝐿)(𝑥(.r‘𝐿)𝑦) = 𝑧)} |
25 | 16, 20, 24 | 3eqtr4g 2799 |
1
⊢ (𝜑 →
(∥r‘𝐾) = (∥r‘𝐿)) |