Step | Hyp | Ref
| Expression |
1 | | dvdsrvald.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ SRing) |
2 | | reldvdsrsrg 13214 |
. . . . . 6
⊢ (𝑅 ∈ SRing → Rel
(∥r‘𝑅)) |
3 | 1, 2 | syl 14 |
. . . . 5
⊢ (𝜑 → Rel
(∥r‘𝑅)) |
4 | | dvdsrvald.2 |
. . . . . 6
⊢ (𝜑 → ∥ =
(∥r‘𝑅)) |
5 | 4 | releqd 4710 |
. . . . 5
⊢ (𝜑 → (Rel ∥ ↔ Rel
(∥r‘𝑅))) |
6 | 3, 5 | mpbird 167 |
. . . 4
⊢ (𝜑 → Rel ∥ ) |
7 | | brrelex12 4664 |
. . . 4
⊢ ((Rel
∥
∧ 𝑋 ∥ 𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
8 | 6, 7 | sylan 283 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∥ 𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
9 | 8 | ex 115 |
. 2
⊢ (𝜑 → (𝑋 ∥ 𝑌 → (𝑋 ∈ V ∧ 𝑌 ∈ V))) |
10 | | simplr 528 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → 𝑋 ∈ 𝐵) |
11 | 10 | elexd 2750 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → 𝑋 ∈ V) |
12 | | simprr 531 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → (𝑧 · 𝑋) = 𝑌) |
13 | 1 | ad2antrr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → 𝑅 ∈ SRing) |
14 | | simprl 529 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → 𝑧 ∈ 𝐵) |
15 | | dvdsrvald.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
16 | 15 | ad2antrr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → 𝐵 = (Base‘𝑅)) |
17 | 14, 16 | eleqtrd 2256 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → 𝑧 ∈ (Base‘𝑅)) |
18 | 10, 16 | eleqtrd 2256 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → 𝑋 ∈ (Base‘𝑅)) |
19 | | eqid 2177 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
20 | | eqid 2177 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
21 | 19, 20 | srgcl 13106 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ 𝑧 ∈ (Base‘𝑅) ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑧(.r‘𝑅)𝑋) ∈ (Base‘𝑅)) |
22 | 13, 17, 18, 21 | syl3anc 1238 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → (𝑧(.r‘𝑅)𝑋) ∈ (Base‘𝑅)) |
23 | | dvdsrvald.3 |
. . . . . . . . . 10
⊢ (𝜑 → · =
(.r‘𝑅)) |
24 | 23 | ad2antrr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → · =
(.r‘𝑅)) |
25 | 24 | oveqd 5891 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → (𝑧 · 𝑋) = (𝑧(.r‘𝑅)𝑋)) |
26 | 22, 25, 16 | 3eltr4d 2261 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → (𝑧 · 𝑋) ∈ 𝐵) |
27 | 12, 26 | eqeltrrd 2255 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → 𝑌 ∈ 𝐵) |
28 | 27 | elexd 2750 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → 𝑌 ∈ V) |
29 | 11, 28 | jca 306 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐵) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 · 𝑋) = 𝑌)) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
30 | 29 | rexlimdvaa 2595 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌 → (𝑋 ∈ V ∧ 𝑌 ∈ V))) |
31 | 30 | expimpd 363 |
. 2
⊢ (𝜑 → ((𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V))) |
32 | 15, 4, 1, 23 | dvdsrvald 13215 |
. . . . . 6
⊢ (𝜑 → ∥ = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
33 | 32 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ V ∧ 𝑌 ∈ V)) → ∥ = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}) |
34 | 33 | breqd 4014 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ V ∧ 𝑌 ∈ V)) → (𝑋 ∥ 𝑌 ↔ 𝑋{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}𝑌)) |
35 | | simpl 109 |
. . . . . . . 8
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑥 = 𝑋) |
36 | 35 | eleq1d 2246 |
. . . . . . 7
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝑥 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵)) |
37 | 35 | oveq2d 5890 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝑧 · 𝑥) = (𝑧 · 𝑋)) |
38 | | simpr 110 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌) |
39 | 37, 38 | eqeq12d 2192 |
. . . . . . . 8
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → ((𝑧 · 𝑥) = 𝑦 ↔ (𝑧 · 𝑋) = 𝑌)) |
40 | 39 | rexbidv 2478 |
. . . . . . 7
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦 ↔ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)) |
41 | 36, 40 | anbi12d 473 |
. . . . . 6
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → ((𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦) ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌))) |
42 | | eqid 2177 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)} |
43 | 41, 42 | brabga 4264 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌))) |
44 | 43 | adantl 277 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ V ∧ 𝑌 ∈ V)) → (𝑋{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑥) = 𝑦)}𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌))) |
45 | 34, 44 | bitrd 188 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ V ∧ 𝑌 ∈ V)) → (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌))) |
46 | 45 | ex 115 |
. 2
⊢ (𝜑 → ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌)))) |
47 | 9, 31, 46 | pm5.21ndd 705 |
1
⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 (𝑧 · 𝑋) = 𝑌))) |