| Step | Hyp | Ref
| Expression |
| 1 | | qqhval2.0 |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
| 2 | | qqhval2.1 |
. . 3
⊢ / =
(/r‘𝑅) |
| 3 | | qqhval2.2 |
. . 3
⊢ 𝐿 = (ℤRHom‘𝑅) |
| 4 | 1, 2, 3 | qqhval2 33983 |
. 2
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) =
(𝑞 ∈ ℚ ↦
((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))))) |
| 5 | | drngring 20736 |
. . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
| 6 | 5 | adantr 480 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
𝑅 ∈
Ring) |
| 7 | 6 | adantr 480 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
𝑅 ∈
Ring) |
| 8 | 3 | zrhrhm 21522 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
| 9 | | zringbas 21464 |
. . . . . 6
⊢ ℤ =
(Base‘ℤring) |
| 10 | 9, 1 | rhmf 20485 |
. . . . 5
⊢ (𝐿 ∈ (ℤring
RingHom 𝑅) → 𝐿:ℤ⟶𝐵) |
| 11 | 7, 8, 10 | 3syl 18 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
𝐿:ℤ⟶𝐵) |
| 12 | | qnumcl 16777 |
. . . . 5
⊢ (𝑞 ∈ ℚ →
(numer‘𝑞) ∈
ℤ) |
| 13 | 12 | adantl 481 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
(numer‘𝑞) ∈
ℤ) |
| 14 | 11, 13 | ffvelcdmd 7105 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
(𝐿‘(numer‘𝑞)) ∈ 𝐵) |
| 15 | | simpll 767 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
𝑅 ∈
DivRing) |
| 16 | | qdencl 16778 |
. . . . . . 7
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
ℕ) |
| 17 | 16 | adantl 481 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
(denom‘𝑞) ∈
ℕ) |
| 18 | 17 | nnzd 12640 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
(denom‘𝑞) ∈
ℤ) |
| 19 | 11, 18 | ffvelcdmd 7105 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
(𝐿‘(denom‘𝑞)) ∈ 𝐵) |
| 20 | 17 | nnne0d 12316 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
(denom‘𝑞) ≠
0) |
| 21 | 20 | neneqd 2945 |
. . . . . . . . 9
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
¬ (denom‘𝑞) =
0) |
| 22 | | fvex 6919 |
. . . . . . . . . 10
⊢
(denom‘𝑞)
∈ V |
| 23 | 22 | elsn 4641 |
. . . . . . . . 9
⊢
((denom‘𝑞)
∈ {0} ↔ (denom‘𝑞) = 0) |
| 24 | 21, 23 | sylnibr 329 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
¬ (denom‘𝑞)
∈ {0}) |
| 25 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 26 | 1, 3, 25 | zrhker 33976 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
((chr‘𝑅) = 0 ↔
(◡𝐿 “ {(0g‘𝑅)}) = {0})) |
| 27 | 26 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧
(chr‘𝑅) = 0) →
(◡𝐿 “ {(0g‘𝑅)}) = {0}) |
| 28 | 5, 27 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(◡𝐿 “ {(0g‘𝑅)}) = {0}) |
| 29 | 28 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
(◡𝐿 “ {(0g‘𝑅)}) = {0}) |
| 30 | 24, 29 | neleqtrrd 2864 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
¬ (denom‘𝑞)
∈ (◡𝐿 “ {(0g‘𝑅)})) |
| 31 | | ffn 6736 |
. . . . . . . . . . . 12
⊢ (𝐿:ℤ⟶𝐵 → 𝐿 Fn ℤ) |
| 32 | 8, 10, 31 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝐿 Fn ℤ) |
| 33 | | elpreima 7078 |
. . . . . . . . . . 11
⊢ (𝐿 Fn ℤ →
((denom‘𝑞) ∈
(◡𝐿 “ {(0g‘𝑅)}) ↔ ((denom‘𝑞) ∈ ℤ ∧ (𝐿‘(denom‘𝑞)) ∈
{(0g‘𝑅)}))) |
| 34 | 5, 32, 33 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑅 ∈ DivRing →
((denom‘𝑞) ∈
(◡𝐿 “ {(0g‘𝑅)}) ↔ ((denom‘𝑞) ∈ ℤ ∧ (𝐿‘(denom‘𝑞)) ∈
{(0g‘𝑅)}))) |
| 35 | 34 | biimpar 477 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DivRing ∧
((denom‘𝑞) ∈
ℤ ∧ (𝐿‘(denom‘𝑞)) ∈ {(0g‘𝑅)})) → (denom‘𝑞) ∈ (◡𝐿 “ {(0g‘𝑅)})) |
| 36 | 35 | expr 456 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧
(denom‘𝑞) ∈
ℤ) → ((𝐿‘(denom‘𝑞)) ∈ {(0g‘𝑅)} → (denom‘𝑞) ∈ (◡𝐿 “ {(0g‘𝑅)}))) |
| 37 | 36 | con3dimp 408 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(denom‘𝑞) ∈
ℤ) ∧ ¬ (denom‘𝑞) ∈ (◡𝐿 “ {(0g‘𝑅)})) → ¬ (𝐿‘(denom‘𝑞)) ∈
{(0g‘𝑅)}) |
| 38 | 15, 18, 30, 37 | syl21anc 838 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
¬ (𝐿‘(denom‘𝑞)) ∈ {(0g‘𝑅)}) |
| 39 | | fvex 6919 |
. . . . . . 7
⊢ (𝐿‘(denom‘𝑞)) ∈ V |
| 40 | 39 | elsn 4641 |
. . . . . 6
⊢ ((𝐿‘(denom‘𝑞)) ∈
{(0g‘𝑅)}
↔ (𝐿‘(denom‘𝑞)) = (0g‘𝑅)) |
| 41 | 38, 40 | sylnib 328 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
¬ (𝐿‘(denom‘𝑞)) = (0g‘𝑅)) |
| 42 | 41 | neqned 2947 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
(𝐿‘(denom‘𝑞)) ≠
(0g‘𝑅)) |
| 43 | | eqid 2737 |
. . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 44 | 1, 43, 25 | drngunit 20734 |
. . . . 5
⊢ (𝑅 ∈ DivRing → ((𝐿‘(denom‘𝑞)) ∈ (Unit‘𝑅) ↔ ((𝐿‘(denom‘𝑞)) ∈ 𝐵 ∧ (𝐿‘(denom‘𝑞)) ≠ (0g‘𝑅)))) |
| 45 | 44 | biimpar 477 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ ((𝐿‘(denom‘𝑞)) ∈ 𝐵 ∧ (𝐿‘(denom‘𝑞)) ≠ (0g‘𝑅))) → (𝐿‘(denom‘𝑞)) ∈ (Unit‘𝑅)) |
| 46 | 15, 19, 42, 45 | syl12anc 837 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
(𝐿‘(denom‘𝑞)) ∈ (Unit‘𝑅)) |
| 47 | 1, 43, 2 | dvrcl 20404 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝐿‘(numer‘𝑞)) ∈ 𝐵 ∧ (𝐿‘(denom‘𝑞)) ∈ (Unit‘𝑅)) → ((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))) ∈ 𝐵) |
| 48 | 7, 14, 46, 47 | syl3anc 1373 |
. 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
((𝐿‘(numer‘𝑞)) / (𝐿‘(denom‘𝑞))) ∈ 𝐵) |
| 49 | 4, 48 | fmpt3d 7136 |
1
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅):ℚ⟶𝐵) |