Step | Hyp | Ref
| Expression |
1 | | elex 3449 |
. . . 4
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ V) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
𝑅 ∈
V) |
3 | | qqhval2.1 |
. . . 4
⊢ / =
(/r‘𝑅) |
4 | | eqid 2738 |
. . . 4
⊢
(1r‘𝑅) = (1r‘𝑅) |
5 | | qqhval2.2 |
. . . 4
⊢ 𝐿 = (ℤRHom‘𝑅) |
6 | 3, 4, 5 | qqhval 31911 |
. . 3
⊢ (𝑅 ∈ V →
(ℚHom‘𝑅) = ran
(𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
7 | 2, 6 | syl 17 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) = ran
(𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
8 | | eqidd 2739 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
ℤ = ℤ) |
9 | | qqhval2.0 |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
10 | | eqid 2738 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
11 | 9, 5, 10 | zrhunitpreima 31915 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(◡𝐿 “ (Unit‘𝑅)) = (ℤ ∖ {0})) |
12 | | mpoeq12 7340 |
. . . 4
⊢ ((ℤ
= ℤ ∧ (◡𝐿 “ (Unit‘𝑅)) = (ℤ ∖ {0})) → (𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0}) ↦
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
13 | 8, 11, 12 | syl2anc 584 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0}) ↦
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
14 | 13 | rneqd 5842 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
ran (𝑥 ∈ ℤ,
𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = ran (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0}) ↦
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
15 | | nfv 1917 |
. . . 4
⊢
Ⅎ𝑒(𝑅 ∈ DivRing ∧
(chr‘𝑅) =
0) |
16 | | nfab1 2909 |
. . . 4
⊢
Ⅎ𝑒{𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} |
17 | | nfcv 2907 |
. . . 4
⊢
Ⅎ𝑒{〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))} |
18 | | simpr 485 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
19 | | zssq 12685 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℚ |
20 | | simplrl 774 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑥 ∈ ℤ) |
21 | 19, 20 | sselid 3920 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑥 ∈ ℚ) |
22 | | simplrr 775 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑦 ∈ (ℤ ∖
{0})) |
23 | 22 | eldifad 3900 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑦 ∈ ℤ) |
24 | 19, 23 | sselid 3920 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑦 ∈ ℚ) |
25 | 22 | eldifbd 3901 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → ¬ 𝑦 ∈ {0}) |
26 | | velsn 4579 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {0} ↔ 𝑦 = 0) |
27 | 26 | necon3bbii 2991 |
. . . . . . . . . . . 12
⊢ (¬
𝑦 ∈ {0} ↔ 𝑦 ≠ 0) |
28 | 25, 27 | sylib 217 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑦 ≠ 0) |
29 | | qdivcl 12699 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) ∈ ℚ) |
30 | 21, 24, 28, 29 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → (𝑥 / 𝑦) ∈ ℚ) |
31 | | simplll 772 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑅 ∈ DivRing) |
32 | | simpllr 773 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → (chr‘𝑅) = 0) |
33 | 9, 3, 5 | qqhval2lem 31918 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ ∧
𝑦 ≠ 0)) → ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦)))) = ((𝐿‘𝑥) / (𝐿‘𝑦))) |
34 | 33 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ ∧
𝑦 ≠ 0)) → ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦))))) |
35 | 31, 32, 20, 23, 28, 34 | syl23anc 1376 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦))))) |
36 | | ovex 7302 |
. . . . . . . . . . 11
⊢ (𝑥 / 𝑦) ∈ V |
37 | | ovex 7302 |
. . . . . . . . . . 11
⊢ ((𝐿‘𝑥) / (𝐿‘𝑦)) ∈ V |
38 | | opeq12 4808 |
. . . . . . . . . . . . 13
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → 〈𝑞, 𝑠〉 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
39 | 38 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝑒 = 〈𝑞, 𝑠〉 ↔ 𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
40 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → 𝑞 = (𝑥 / 𝑦)) |
41 | 40 | eleq1d 2823 |
. . . . . . . . . . . . 13
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝑞 ∈ ℚ ↔ (𝑥 / 𝑦) ∈ ℚ)) |
42 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) |
43 | 40 | fveq2d 6772 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (numer‘𝑞) = (numer‘(𝑥 / 𝑦))) |
44 | 43 | fveq2d 6772 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝐿‘(numer‘𝑞)) = (𝐿‘(numer‘(𝑥 / 𝑦)))) |
45 | 40 | fveq2d 6772 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (denom‘𝑞) = (denom‘(𝑥 / 𝑦))) |
46 | 45 | fveq2d 6772 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝐿‘(denom‘𝑞)) = (𝐿‘(denom‘(𝑥 / 𝑦)))) |
47 | 44, 46 | oveq12d 7287 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦))))) |
48 | 42, 47 | eqeq12d 2754 |
. . . . . . . . . . . . 13
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))) ↔ ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦)))))) |
49 | 41, 48 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → ((𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))) ↔ ((𝑥 / 𝑦) ∈ ℚ ∧ ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦))))))) |
50 | 39, 49 | anbi12d 631 |
. . . . . . . . . . 11
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → ((𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))) ↔ (𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 ∧ ((𝑥 / 𝑦) ∈ ℚ ∧ ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦)))))))) |
51 | 36, 37, 50 | spc2ev 3545 |
. . . . . . . . . 10
⊢ ((𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 ∧ ((𝑥 / 𝑦) ∈ ℚ ∧ ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦)))))) → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) |
52 | 18, 30, 35, 51 | syl12anc 834 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) |
53 | 52 | ex 413 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) → (𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))))) |
54 | 53 | rexlimdvva 3222 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(∃𝑥 ∈ ℤ
∃𝑦 ∈ (ℤ
∖ {0})𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))))) |
55 | 54 | imp 407 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
∃𝑥 ∈ ℤ
∃𝑦 ∈ (ℤ
∖ {0})𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) |
56 | | 19.42vv 1961 |
. . . . . . 7
⊢
(∃𝑞∃𝑠((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) ↔ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))))) |
57 | | simprrl 778 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑞 ∈ ℚ) |
58 | | qnumcl 16433 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℚ →
(numer‘𝑞) ∈
ℤ) |
59 | 57, 58 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → (numer‘𝑞) ∈ ℤ) |
60 | | qdencl 16434 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
ℕ) |
61 | 57, 60 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → (denom‘𝑞) ∈ ℕ) |
62 | 61 | nnzd 12414 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → (denom‘𝑞) ∈ ℤ) |
63 | | nnne0 11996 |
. . . . . . . . . . 11
⊢
((denom‘𝑞)
∈ ℕ → (denom‘𝑞) ≠ 0) |
64 | | nelsn 4603 |
. . . . . . . . . . 11
⊢
((denom‘𝑞)
≠ 0 → ¬ (denom‘𝑞) ∈ {0}) |
65 | 61, 63, 64 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → ¬ (denom‘𝑞) ∈ {0}) |
66 | 62, 65 | eldifd 3899 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → (denom‘𝑞) ∈ (ℤ ∖
{0})) |
67 | | simprl 768 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑒 = 〈𝑞, 𝑠〉) |
68 | | qeqnumdivden 16439 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞))) |
69 | 57, 68 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑞 = ((numer‘𝑞) / (denom‘𝑞))) |
70 | | simprrr 779 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))) |
71 | 69, 70 | opeq12d 4814 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 〈𝑞, 𝑠〉 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉) |
72 | 67, 71 | eqtrd 2778 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑒 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉) |
73 | | oveq1 7276 |
. . . . . . . . . . . 12
⊢ (𝑥 = (numer‘𝑞) → (𝑥 / 𝑦) = ((numer‘𝑞) / 𝑦)) |
74 | | fveq2 6768 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (numer‘𝑞) → (𝐿‘𝑥) = (𝐿‘(numer‘𝑞))) |
75 | 74 | oveq1d 7284 |
. . . . . . . . . . . 12
⊢ (𝑥 = (numer‘𝑞) → ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))) |
76 | 73, 75 | opeq12d 4814 |
. . . . . . . . . . 11
⊢ (𝑥 = (numer‘𝑞) → 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 = 〈((numer‘𝑞) / 𝑦), ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))〉) |
77 | 76 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑥 = (numer‘𝑞) → (𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 ↔ 𝑒 = 〈((numer‘𝑞) / 𝑦), ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))〉)) |
78 | | oveq2 7277 |
. . . . . . . . . . . 12
⊢ (𝑦 = (denom‘𝑞) → ((numer‘𝑞) / 𝑦) = ((numer‘𝑞) / (denom‘𝑞))) |
79 | | fveq2 6768 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (denom‘𝑞) → (𝐿‘𝑦) = (𝐿‘(denom‘𝑞))) |
80 | 79 | oveq2d 7285 |
. . . . . . . . . . . 12
⊢ (𝑦 = (denom‘𝑞) → ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦)) = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))) |
81 | 78, 80 | opeq12d 4814 |
. . . . . . . . . . 11
⊢ (𝑦 = (denom‘𝑞) →
〈((numer‘𝑞) /
𝑦), ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))〉 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉) |
82 | 81 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑦 = (denom‘𝑞) → (𝑒 = 〈((numer‘𝑞) / 𝑦), ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))〉 ↔ 𝑒 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉)) |
83 | 77, 82 | rspc2ev 3573 |
. . . . . . . . 9
⊢
(((numer‘𝑞)
∈ ℤ ∧ (denom‘𝑞) ∈ (ℤ ∖ {0}) ∧ 𝑒 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
84 | 59, 66, 72, 83 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
85 | 84 | exlimivv 1935 |
. . . . . . 7
⊢
(∃𝑞∃𝑠((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
86 | 56, 85 | sylbir 234 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
87 | 55, 86 | impbida 798 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(∃𝑥 ∈ ℤ
∃𝑦 ∈ (ℤ
∖ {0})𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 ↔ ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))))) |
88 | | abid 2719 |
. . . . 5
⊢ (𝑒 ∈ {𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
89 | | elopab 5439 |
. . . . 5
⊢ (𝑒 ∈ {〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))} ↔ ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) |
90 | 87, 88, 89 | 3bitr4g 314 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(𝑒 ∈ {𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖
{0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} ↔ 𝑒 ∈ {〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))})) |
91 | 15, 16, 17, 90 | eqrd 3941 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
{𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖
{0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} = {〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))}) |
92 | | eqid 2738 |
. . . 4
⊢ (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0})
↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0}) ↦
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
93 | 92 | rnmpo 7399 |
. . 3
⊢ ran
(𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0})
↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = {𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} |
94 | | df-mpt 5159 |
. . 3
⊢ (𝑞 ∈ ℚ ↦ ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))) = {〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))} |
95 | 91, 93, 94 | 3eqtr4g 2803 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
ran (𝑥 ∈ ℤ,
𝑦 ∈ (ℤ ∖
{0}) ↦ 〈(𝑥 /
𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = (𝑞 ∈ ℚ ↦ ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))) |
96 | 7, 14, 95 | 3eqtrd 2782 |
1
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) =
(𝑞 ∈ ℚ ↦
((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))) |