Proof of Theorem qqhnm
| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑄 ∈
ℚ) |
| 2 | | qeqnumdivden 16783 |
. . . 4
⊢ (𝑄 ∈ ℚ → 𝑄 = ((numer‘𝑄) / (denom‘𝑄))) |
| 3 | 2 | fveq2d 6910 |
. . 3
⊢ (𝑄 ∈ ℚ →
(abs‘𝑄) =
(abs‘((numer‘𝑄)
/ (denom‘𝑄)))) |
| 4 | 1, 3 | syl 17 |
. 2
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(abs‘𝑄) =
(abs‘((numer‘𝑄)
/ (denom‘𝑄)))) |
| 5 | | qnumcl 16777 |
. . . . 5
⊢ (𝑄 ∈ ℚ →
(numer‘𝑄) ∈
ℤ) |
| 6 | 1, 5 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(numer‘𝑄) ∈
ℤ) |
| 7 | 6 | zcnd 12723 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(numer‘𝑄) ∈
ℂ) |
| 8 | | qdencl 16778 |
. . . . 5
⊢ (𝑄 ∈ ℚ →
(denom‘𝑄) ∈
ℕ) |
| 9 | 1, 8 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(denom‘𝑄) ∈
ℕ) |
| 10 | 9 | nncnd 12282 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(denom‘𝑄) ∈
ℂ) |
| 11 | | nnne0 12300 |
. . . 4
⊢
((denom‘𝑄)
∈ ℕ → (denom‘𝑄) ≠ 0) |
| 12 | 1, 8, 11 | 3syl 18 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(denom‘𝑄) ≠
0) |
| 13 | 7, 10, 12 | absdivd 15494 |
. 2
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(abs‘((numer‘𝑄)
/ (denom‘𝑄))) =
((abs‘(numer‘𝑄)) / (abs‘(denom‘𝑄)))) |
| 14 | | inss2 4238 |
. . . . 5
⊢ (NrmRing
∩ DivRing) ⊆ DivRing |
| 15 | | simpl1 1192 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑅 ∈ (NrmRing ∩
DivRing)) |
| 16 | 14, 15 | sselid 3981 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑅 ∈
DivRing) |
| 17 | | simpl3 1194 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(chr‘𝑅) =
0) |
| 18 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 19 | | eqid 2737 |
. . . . . 6
⊢
(/r‘𝑅) = (/r‘𝑅) |
| 20 | | eqid 2737 |
. . . . . 6
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
| 21 | 18, 19, 20 | qqhvval 33984 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((ℚHom‘𝑅)‘𝑄) = (((ℤRHom‘𝑅)‘(numer‘𝑄))(/r‘𝑅)((ℤRHom‘𝑅)‘(denom‘𝑄)))) |
| 22 | 21 | fveq2d 6910 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℚHom‘𝑅)‘𝑄)) = (𝑁‘(((ℤRHom‘𝑅)‘(numer‘𝑄))(/r‘𝑅)((ℤRHom‘𝑅)‘(denom‘𝑄))))) |
| 23 | 16, 17, 1, 22 | syl21anc 838 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℚHom‘𝑅)‘𝑄)) = (𝑁‘(((ℤRHom‘𝑅)‘(numer‘𝑄))(/r‘𝑅)((ℤRHom‘𝑅)‘(denom‘𝑄))))) |
| 24 | | inss1 4237 |
. . . . 5
⊢ (NrmRing
∩ DivRing) ⊆ NrmRing |
| 25 | 24, 15 | sselid 3981 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑅 ∈
NrmRing) |
| 26 | | drngnzr 20748 |
. . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) |
| 27 | 16, 26 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑅 ∈
NzRing) |
| 28 | | drngring 20736 |
. . . . . 6
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
| 29 | 20 | zrhrhm 21522 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(ℤRHom‘𝑅)
∈ (ℤring RingHom 𝑅)) |
| 30 | | zringbas 21464 |
. . . . . . 7
⊢ ℤ =
(Base‘ℤring) |
| 31 | 30, 18 | rhmf 20485 |
. . . . . 6
⊢
((ℤRHom‘𝑅) ∈ (ℤring RingHom
𝑅) →
(ℤRHom‘𝑅):ℤ⟶(Base‘𝑅)) |
| 32 | 16, 28, 29, 31 | 4syl 19 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(ℤRHom‘𝑅):ℤ⟶(Base‘𝑅)) |
| 33 | 32, 6 | ffvelcdmd 7105 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((ℤRHom‘𝑅)‘(numer‘𝑄)) ∈ (Base‘𝑅)) |
| 34 | 9 | nnzd 12640 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(denom‘𝑄) ∈
ℤ) |
| 35 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 36 | 18, 20, 35 | elzrhunit 33978 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
((denom‘𝑄) ∈
ℤ ∧ (denom‘𝑄) ≠ 0)) → ((ℤRHom‘𝑅)‘(denom‘𝑄)) ∈ (Unit‘𝑅)) |
| 37 | 16, 17, 34, 12, 36 | syl22anc 839 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((ℤRHom‘𝑅)‘(denom‘𝑄)) ∈ (Unit‘𝑅)) |
| 38 | | qqhnm.n |
. . . . 5
⊢ 𝑁 = (norm‘𝑅) |
| 39 | | eqid 2737 |
. . . . 5
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 40 | 18, 38, 39, 19 | nmdvr 24691 |
. . . 4
⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧
(((ℤRHom‘𝑅)‘(numer‘𝑄)) ∈ (Base‘𝑅) ∧ ((ℤRHom‘𝑅)‘(denom‘𝑄)) ∈ (Unit‘𝑅))) → (𝑁‘(((ℤRHom‘𝑅)‘(numer‘𝑄))(/r‘𝑅)((ℤRHom‘𝑅)‘(denom‘𝑄)))) = ((𝑁‘((ℤRHom‘𝑅)‘(numer‘𝑄))) / (𝑁‘((ℤRHom‘𝑅)‘(denom‘𝑄))))) |
| 41 | 25, 27, 33, 37, 40 | syl22anc 839 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘(((ℤRHom‘𝑅)‘(numer‘𝑄))(/r‘𝑅)((ℤRHom‘𝑅)‘(denom‘𝑄)))) = ((𝑁‘((ℤRHom‘𝑅)‘(numer‘𝑄))) / (𝑁‘((ℤRHom‘𝑅)‘(denom‘𝑄))))) |
| 42 | | simpl2 1193 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑍 ∈
NrmMod) |
| 43 | | qqhnm.z |
. . . . . . 7
⊢ 𝑍 = (ℤMod‘𝑅) |
| 44 | 43 | zhmnrg 33966 |
. . . . . 6
⊢ (𝑅 ∈ NrmRing → 𝑍 ∈
NrmRing) |
| 45 | 25, 44 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑍 ∈
NrmRing) |
| 46 | 18, 38, 43, 20 | zrhnm 33968 |
. . . . 5
⊢ (((𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧
(numer‘𝑄) ∈
ℤ) → (𝑁‘((ℤRHom‘𝑅)‘(numer‘𝑄))) = (abs‘(numer‘𝑄))) |
| 47 | 42, 45, 27, 6, 46 | syl31anc 1375 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℤRHom‘𝑅)‘(numer‘𝑄))) = (abs‘(numer‘𝑄))) |
| 48 | 18, 38, 43, 20 | zrhnm 33968 |
. . . . 5
⊢ (((𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧
(denom‘𝑄) ∈
ℤ) → (𝑁‘((ℤRHom‘𝑅)‘(denom‘𝑄))) = (abs‘(denom‘𝑄))) |
| 49 | 42, 45, 27, 34, 48 | syl31anc 1375 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℤRHom‘𝑅)‘(denom‘𝑄))) = (abs‘(denom‘𝑄))) |
| 50 | 47, 49 | oveq12d 7449 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((𝑁‘((ℤRHom‘𝑅)‘(numer‘𝑄))) / (𝑁‘((ℤRHom‘𝑅)‘(denom‘𝑄)))) = ((abs‘(numer‘𝑄)) /
(abs‘(denom‘𝑄)))) |
| 51 | 23, 41, 50 | 3eqtrrd 2782 |
. 2
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((abs‘(numer‘𝑄)) / (abs‘(denom‘𝑄))) = (𝑁‘((ℚHom‘𝑅)‘𝑄))) |
| 52 | 4, 13, 51 | 3eqtrrd 2782 |
1
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℚHom‘𝑅)‘𝑄)) = (abs‘𝑄)) |