| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. . . 4
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ V) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
𝑅 ∈
V) |
| 3 | | qqhval2.1 |
. . . 4
⊢ / =
(/r‘𝑅) |
| 4 | | eqid 2737 |
. . . 4
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 5 | | qqhval2.2 |
. . . 4
⊢ 𝐿 = (ℤRHom‘𝑅) |
| 6 | 3, 4, 5 | qqhval 33973 |
. . 3
⊢ (𝑅 ∈ V →
(ℚHom‘𝑅) = ran
(𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
| 7 | 2, 6 | syl 17 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) = ran
(𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
| 8 | | eqid 2737 |
. . . 4
⊢ ℤ =
ℤ |
| 9 | | qqhval2.0 |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
| 10 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 11 | 9, 5, 10 | zrhunitpreima 33977 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(◡𝐿 “ (Unit‘𝑅)) = (ℤ ∖ {0})) |
| 12 | | mpoeq12 7506 |
. . . 4
⊢ ((ℤ
= ℤ ∧ (◡𝐿 “ (Unit‘𝑅)) = (ℤ ∖ {0})) → (𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0}) ↦
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
| 13 | 8, 11, 12 | sylancr 587 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(𝑥 ∈ ℤ, 𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0}) ↦
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
| 14 | 13 | rneqd 5949 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
ran (𝑥 ∈ ℤ,
𝑦 ∈ (◡𝐿 “ (Unit‘𝑅)) ↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = ran (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0}) ↦
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
| 15 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑒(𝑅 ∈ DivRing ∧
(chr‘𝑅) =
0) |
| 16 | | nfab1 2907 |
. . . 4
⊢
Ⅎ𝑒{𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} |
| 17 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑒{〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))} |
| 18 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
| 19 | | zssq 12998 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℚ |
| 20 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑥 ∈ ℤ) |
| 21 | 19, 20 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑥 ∈ ℚ) |
| 22 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑦 ∈ (ℤ ∖
{0})) |
| 23 | 22 | eldifad 3963 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑦 ∈ ℤ) |
| 24 | 19, 23 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑦 ∈ ℚ) |
| 25 | 22 | eldifbd 3964 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → ¬ 𝑦 ∈ {0}) |
| 26 | | velsn 4642 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {0} ↔ 𝑦 = 0) |
| 27 | 26 | necon3bbii 2988 |
. . . . . . . . . . . 12
⊢ (¬
𝑦 ∈ {0} ↔ 𝑦 ≠ 0) |
| 28 | 25, 27 | sylib 218 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑦 ≠ 0) |
| 29 | | qdivcl 13012 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) ∈ ℚ) |
| 30 | 21, 24, 28, 29 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → (𝑥 / 𝑦) ∈ ℚ) |
| 31 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → 𝑅 ∈ DivRing) |
| 32 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → (chr‘𝑅) = 0) |
| 33 | 9, 3, 5 | qqhval2lem 33982 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ ∧
𝑦 ≠ 0)) → ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦)))) = ((𝐿‘𝑥) / (𝐿‘𝑦))) |
| 34 | 33 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ ℤ ∧
𝑦 ≠ 0)) → ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦))))) |
| 35 | 31, 32, 20, 23, 28, 34 | syl23anc 1379 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦))))) |
| 36 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑥 / 𝑦) ∈ V |
| 37 | | ovex 7464 |
. . . . . . . . . . 11
⊢ ((𝐿‘𝑥) / (𝐿‘𝑦)) ∈ V |
| 38 | | opeq12 4875 |
. . . . . . . . . . . . 13
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → 〈𝑞, 𝑠〉 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
| 39 | 38 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝑒 = 〈𝑞, 𝑠〉 ↔ 𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉)) |
| 40 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → 𝑞 = (𝑥 / 𝑦)) |
| 41 | 40 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝑞 ∈ ℚ ↔ (𝑥 / 𝑦) ∈ ℚ)) |
| 42 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) |
| 43 | 40 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (numer‘𝑞) = (numer‘(𝑥 / 𝑦))) |
| 44 | 43 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝐿‘(numer‘𝑞)) = (𝐿‘(numer‘(𝑥 / 𝑦)))) |
| 45 | 40 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (denom‘𝑞) = (denom‘(𝑥 / 𝑦))) |
| 46 | 45 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝐿‘(denom‘𝑞)) = (𝐿‘(denom‘(𝑥 / 𝑦)))) |
| 47 | 44, 46 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦))))) |
| 48 | 42, 47 | eqeq12d 2753 |
. . . . . . . . . . . . 13
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → (𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))) ↔ ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦)))))) |
| 49 | 41, 48 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → ((𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))) ↔ ((𝑥 / 𝑦) ∈ ℚ ∧ ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦))))))) |
| 50 | 39, 49 | anbi12d 632 |
. . . . . . . . . . 11
⊢ ((𝑞 = (𝑥 / 𝑦) ∧ 𝑠 = ((𝐿‘𝑥) / (𝐿‘𝑦))) → ((𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))) ↔ (𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 ∧ ((𝑥 / 𝑦) ∈ ℚ ∧ ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦)))))))) |
| 51 | 36, 37, 50 | spc2ev 3607 |
. . . . . . . . . 10
⊢ ((𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 ∧ ((𝑥 / 𝑦) ∈ ℚ ∧ ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘(𝑥 / 𝑦))) / (𝐿‘(denom‘(𝑥 / 𝑦)))))) → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) |
| 52 | 18, 30, 35, 51 | syl12anc 837 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) ∧ 𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) |
| 53 | 52 | ex 412 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑥 ∈ ℤ ∧
𝑦 ∈ (ℤ ∖
{0}))) → (𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))))) |
| 54 | 53 | rexlimdvva 3213 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(∃𝑥 ∈ ℤ
∃𝑦 ∈ (ℤ
∖ {0})𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))))) |
| 55 | 54 | imp 406 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
∃𝑥 ∈ ℤ
∃𝑦 ∈ (ℤ
∖ {0})𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) → ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) |
| 56 | | 19.42vv 1957 |
. . . . . . 7
⊢
(∃𝑞∃𝑠((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) ↔ ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))))) |
| 57 | | simprrl 781 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑞 ∈ ℚ) |
| 58 | | qnumcl 16777 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℚ →
(numer‘𝑞) ∈
ℤ) |
| 59 | 57, 58 | syl 17 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → (numer‘𝑞) ∈ ℤ) |
| 60 | | qdencl 16778 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
ℕ) |
| 61 | 57, 60 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → (denom‘𝑞) ∈ ℕ) |
| 62 | 61 | nnzd 12640 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → (denom‘𝑞) ∈ ℤ) |
| 63 | | nnne0 12300 |
. . . . . . . . . . 11
⊢
((denom‘𝑞)
∈ ℕ → (denom‘𝑞) ≠ 0) |
| 64 | | nelsn 4666 |
. . . . . . . . . . 11
⊢
((denom‘𝑞)
≠ 0 → ¬ (denom‘𝑞) ∈ {0}) |
| 65 | 61, 63, 64 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → ¬ (denom‘𝑞) ∈ {0}) |
| 66 | 62, 65 | eldifd 3962 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → (denom‘𝑞) ∈ (ℤ ∖
{0})) |
| 67 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑒 = 〈𝑞, 𝑠〉) |
| 68 | | qeqnumdivden 16783 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞))) |
| 69 | 57, 68 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑞 = ((numer‘𝑞) / (denom‘𝑞))) |
| 70 | | simprrr 782 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))) |
| 71 | 69, 70 | opeq12d 4881 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 〈𝑞, 𝑠〉 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉) |
| 72 | 67, 71 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → 𝑒 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉) |
| 73 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = (numer‘𝑞) → (𝑥 / 𝑦) = ((numer‘𝑞) / 𝑦)) |
| 74 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (numer‘𝑞) → (𝐿‘𝑥) = (𝐿‘(numer‘𝑞))) |
| 75 | 74 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑥 = (numer‘𝑞) → ((𝐿‘𝑥) / (𝐿‘𝑦)) = ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))) |
| 76 | 73, 75 | opeq12d 4881 |
. . . . . . . . . . 11
⊢ (𝑥 = (numer‘𝑞) → 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 = 〈((numer‘𝑞) / 𝑦), ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))〉) |
| 77 | 76 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑥 = (numer‘𝑞) → (𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 ↔ 𝑒 = 〈((numer‘𝑞) / 𝑦), ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))〉)) |
| 78 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑦 = (denom‘𝑞) → ((numer‘𝑞) / 𝑦) = ((numer‘𝑞) / (denom‘𝑞))) |
| 79 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (denom‘𝑞) → (𝐿‘𝑦) = (𝐿‘(denom‘𝑞))) |
| 80 | 79 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑦 = (denom‘𝑞) → ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦)) = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))) |
| 81 | 78, 80 | opeq12d 4881 |
. . . . . . . . . . 11
⊢ (𝑦 = (denom‘𝑞) →
〈((numer‘𝑞) /
𝑦), ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))〉 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉) |
| 82 | 81 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑦 = (denom‘𝑞) → (𝑒 = 〈((numer‘𝑞) / 𝑦), ((𝐿‘(numer‘𝑞)) / (𝐿‘𝑦))〉 ↔ 𝑒 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉)) |
| 83 | 77, 82 | rspc2ev 3635 |
. . . . . . . . 9
⊢
(((numer‘𝑞)
∈ ℤ ∧ (denom‘𝑞) ∈ (ℤ ∖ {0}) ∧ 𝑒 = 〈((numer‘𝑞) / (denom‘𝑞)), ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))〉) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
| 84 | 59, 66, 72, 83 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
| 85 | 84 | exlimivv 1932 |
. . . . . . 7
⊢
(∃𝑞∃𝑠((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
| 86 | 56, 85 | sylbir 235 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
| 87 | 55, 86 | impbida 801 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(∃𝑥 ∈ ℤ
∃𝑦 ∈ (ℤ
∖ {0})𝑒 =
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉 ↔ ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))))) |
| 88 | | abid 2718 |
. . . . 5
⊢ (𝑒 ∈ {𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
| 89 | | elopab 5532 |
. . . . 5
⊢ (𝑒 ∈ {〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))} ↔ ∃𝑞∃𝑠(𝑒 = 〈𝑞, 𝑠〉 ∧ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))))) |
| 90 | 87, 88, 89 | 3bitr4g 314 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(𝑒 ∈ {𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖
{0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} ↔ 𝑒 ∈ {〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))})) |
| 91 | 15, 16, 17, 90 | eqrd 4003 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
{𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖
{0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} = {〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))}) |
| 92 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0})
↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = (𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0}) ↦
〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) |
| 93 | 92 | rnmpo 7566 |
. . 3
⊢ ran
(𝑥 ∈ ℤ, 𝑦 ∈ (ℤ ∖ {0})
↦ 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = {𝑒 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ (ℤ ∖ {0})𝑒 = 〈(𝑥 / 𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉} |
| 94 | | df-mpt 5226 |
. . 3
⊢ (𝑞 ∈ ℚ ↦ ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞)))) = {〈𝑞, 𝑠〉 ∣ (𝑞 ∈ ℚ ∧ 𝑠 = ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))} |
| 95 | 91, 93, 94 | 3eqtr4g 2802 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
ran (𝑥 ∈ ℤ,
𝑦 ∈ (ℤ ∖
{0}) ↦ 〈(𝑥 /
𝑦), ((𝐿‘𝑥) / (𝐿‘𝑦))〉) = (𝑞 ∈ ℚ ↦ ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))) |
| 96 | 7, 14, 95 | 3eqtrd 2781 |
1
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) =
(𝑞 ∈ ℚ ↦
((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))) |