Step | Hyp | Ref
| Expression |
1 | | df-dvdsr 13189 |
. . 3
⊢
∥r = (𝑟 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦)}) |
2 | | fveq2 5514 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
3 | 2 | eleq2d 2247 |
. . . . 5
⊢ (𝑟 = 𝑅 → (𝑥 ∈ (Base‘𝑟) ↔ 𝑥 ∈ (Base‘𝑅))) |
4 | | fveq2 5514 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
5 | 4 | oveqd 5889 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (𝑧(.r‘𝑟)𝑥) = (𝑧(.r‘𝑅)𝑥)) |
6 | 5 | eqeq1d 2186 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((𝑧(.r‘𝑟)𝑥) = 𝑦 ↔ (𝑧(.r‘𝑅)𝑥) = 𝑦)) |
7 | 2, 6 | rexeqbidv 2685 |
. . . . 5
⊢ (𝑟 = 𝑅 → (∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦 ↔ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)) |
8 | 3, 7 | anbi12d 473 |
. . . 4
⊢ (𝑟 = 𝑅 → ((𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦) ↔ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦))) |
9 | 8 | opabbidv 4068 |
. . 3
⊢ (𝑟 = 𝑅 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑟) ∧ ∃𝑧 ∈ (Base‘𝑟)(𝑧(.r‘𝑟)𝑥) = 𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)}) |
10 | | dvdsrvald.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ SRing) |
11 | 10 | elexd 2750 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
12 | | basfn 12512 |
. . . . . 6
⊢ Base Fn
V |
13 | | funfvex 5531 |
. . . . . . 7
⊢ ((Fun
Base ∧ 𝑅 ∈ dom
Base) → (Base‘𝑅)
∈ V) |
14 | 13 | funfni 5315 |
. . . . . 6
⊢ ((Base Fn
V ∧ 𝑅 ∈ V) →
(Base‘𝑅) ∈
V) |
15 | 12, 11, 14 | sylancr 414 |
. . . . 5
⊢ (𝜑 → (Base‘𝑅) ∈ V) |
16 | | xpexg 4739 |
. . . . 5
⊢
(((Base‘𝑅)
∈ V ∧ (Base‘𝑅) ∈ V) → ((Base‘𝑅) × (Base‘𝑅)) ∈ V) |
17 | 15, 15, 16 | syl2anc 411 |
. . . 4
⊢ (𝜑 → ((Base‘𝑅) × (Base‘𝑅)) ∈ V) |
18 | | simprr 531 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → (𝑧(.r‘𝑅)𝑥) = 𝑦) |
19 | 10 | ad2antrr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → 𝑅 ∈ SRing) |
20 | | simprl 529 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → 𝑧 ∈ (Base‘𝑅)) |
21 | | simplr 528 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → 𝑥 ∈ (Base‘𝑅)) |
22 | | eqid 2177 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
23 | | eqid 2177 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
24 | 22, 23 | srgcl 13084 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ SRing ∧ 𝑧 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑧(.r‘𝑅)𝑥) ∈ (Base‘𝑅)) |
25 | 19, 20, 21, 24 | syl3anc 1238 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → (𝑧(.r‘𝑅)𝑥) ∈ (Base‘𝑅)) |
26 | 18, 25 | eqeltrrd 2255 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → 𝑦 ∈ (Base‘𝑅)) |
27 | 26 | rexlimdvaa 2595 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦 → 𝑦 ∈ (Base‘𝑅))) |
28 | 27 | imdistanda 448 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦) → (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)))) |
29 | 28 | ssopab2dv 4277 |
. . . . 5
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))}) |
30 | | df-xp 4631 |
. . . . 5
⊢
((Base‘𝑅)
× (Base‘𝑅)) =
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))} |
31 | 29, 30 | sseqtrrdi 3204 |
. . . 4
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)} ⊆ ((Base‘𝑅) × (Base‘𝑅))) |
32 | 17, 31 | ssexd 4142 |
. . 3
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)} ∈ V) |
33 | 1, 9, 11, 32 | fvmptd3 5608 |
. 2
⊢ (𝜑 →
(∥r‘𝑅) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)}) |
34 | | dvdsrvald.2 |
. 2
⊢ (𝜑 → ∥ =
(∥r‘𝑅)) |
35 | | dvdsrvald.1 |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
36 | 35 | eleq2d 2247 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝑅))) |
37 | | dvdsrvald.3 |
. . . . . . 7
⊢ (𝜑 → · =
(.r‘𝑅)) |
38 | 37 | oveqd 5889 |
. . . . . 6
⊢ (𝜑 → (𝑧 · 𝑥) = (𝑧(.r‘𝑅)𝑥)) |
39 | 38 | eqeq1d 2186 |
. . . . 5
⊢ (𝜑 → ((𝑧 · 𝑥) = 𝑦 ↔ (𝑧(.r‘𝑅)𝑥) = 𝑦)) |
40 | 35, 39 | rexeqbidv 2685 |
. . . 4
⊢ (𝜑 → (∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦 ↔ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)) |
41 | 36, 40 | anbi12d 473 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦) ↔ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦))) |
42 | 41 | opabbidv 4068 |
. 2
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)}) |
43 | 33, 34, 42 | 3eqtr4d 2220 |
1
⊢ (𝜑 → ∥ = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |