Proof of Theorem qqhnm
Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑄 ∈
ℚ) |
2 | | qeqnumdivden 16450 |
. . . 4
⊢ (𝑄 ∈ ℚ → 𝑄 = ((numer‘𝑄) / (denom‘𝑄))) |
3 | 2 | fveq2d 6778 |
. . 3
⊢ (𝑄 ∈ ℚ →
(abs‘𝑄) =
(abs‘((numer‘𝑄)
/ (denom‘𝑄)))) |
4 | 1, 3 | syl 17 |
. 2
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(abs‘𝑄) =
(abs‘((numer‘𝑄)
/ (denom‘𝑄)))) |
5 | | qnumcl 16444 |
. . . . 5
⊢ (𝑄 ∈ ℚ →
(numer‘𝑄) ∈
ℤ) |
6 | 1, 5 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(numer‘𝑄) ∈
ℤ) |
7 | 6 | zcnd 12427 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(numer‘𝑄) ∈
ℂ) |
8 | | qdencl 16445 |
. . . . 5
⊢ (𝑄 ∈ ℚ →
(denom‘𝑄) ∈
ℕ) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(denom‘𝑄) ∈
ℕ) |
10 | 9 | nncnd 11989 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(denom‘𝑄) ∈
ℂ) |
11 | | nnne0 12007 |
. . . 4
⊢
((denom‘𝑄)
∈ ℕ → (denom‘𝑄) ≠ 0) |
12 | 1, 8, 11 | 3syl 18 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(denom‘𝑄) ≠
0) |
13 | 7, 10, 12 | absdivd 15167 |
. 2
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(abs‘((numer‘𝑄)
/ (denom‘𝑄))) =
((abs‘(numer‘𝑄)) / (abs‘(denom‘𝑄)))) |
14 | | inss2 4163 |
. . . . 5
⊢ (NrmRing
∩ DivRing) ⊆ DivRing |
15 | | simpl1 1190 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑅 ∈ (NrmRing ∩
DivRing)) |
16 | 14, 15 | sselid 3919 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑅 ∈
DivRing) |
17 | | simpl3 1192 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(chr‘𝑅) =
0) |
18 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
19 | | eqid 2738 |
. . . . . 6
⊢
(/r‘𝑅) = (/r‘𝑅) |
20 | | eqid 2738 |
. . . . . 6
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
21 | 18, 19, 20 | qqhvval 31933 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((ℚHom‘𝑅)‘𝑄) = (((ℤRHom‘𝑅)‘(numer‘𝑄))(/r‘𝑅)((ℤRHom‘𝑅)‘(denom‘𝑄)))) |
22 | 21 | fveq2d 6778 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℚHom‘𝑅)‘𝑄)) = (𝑁‘(((ℤRHom‘𝑅)‘(numer‘𝑄))(/r‘𝑅)((ℤRHom‘𝑅)‘(denom‘𝑄))))) |
23 | 16, 17, 1, 22 | syl21anc 835 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℚHom‘𝑅)‘𝑄)) = (𝑁‘(((ℤRHom‘𝑅)‘(numer‘𝑄))(/r‘𝑅)((ℤRHom‘𝑅)‘(denom‘𝑄))))) |
24 | | inss1 4162 |
. . . . 5
⊢ (NrmRing
∩ DivRing) ⊆ NrmRing |
25 | 24, 15 | sselid 3919 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑅 ∈
NrmRing) |
26 | | drngnzr 20533 |
. . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) |
27 | 16, 26 | syl 17 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑅 ∈
NzRing) |
28 | | drngring 19998 |
. . . . . 6
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
29 | 20 | zrhrhm 20713 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(ℤRHom‘𝑅)
∈ (ℤring RingHom 𝑅)) |
30 | | zringbas 20676 |
. . . . . . 7
⊢ ℤ =
(Base‘ℤring) |
31 | 30, 18 | rhmf 19970 |
. . . . . 6
⊢
((ℤRHom‘𝑅) ∈ (ℤring RingHom
𝑅) →
(ℤRHom‘𝑅):ℤ⟶(Base‘𝑅)) |
32 | 16, 28, 29, 31 | 4syl 19 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(ℤRHom‘𝑅):ℤ⟶(Base‘𝑅)) |
33 | 32, 6 | ffvelrnd 6962 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((ℤRHom‘𝑅)‘(numer‘𝑄)) ∈ (Base‘𝑅)) |
34 | 9 | nnzd 12425 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(denom‘𝑄) ∈
ℤ) |
35 | | eqid 2738 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
36 | 18, 20, 35 | elzrhunit 31929 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
((denom‘𝑄) ∈
ℤ ∧ (denom‘𝑄) ≠ 0)) → ((ℤRHom‘𝑅)‘(denom‘𝑄)) ∈ (Unit‘𝑅)) |
37 | 16, 17, 34, 12, 36 | syl22anc 836 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((ℤRHom‘𝑅)‘(denom‘𝑄)) ∈ (Unit‘𝑅)) |
38 | | qqhnm.n |
. . . . 5
⊢ 𝑁 = (norm‘𝑅) |
39 | | eqid 2738 |
. . . . 5
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
40 | 18, 38, 39, 19 | nmdvr 23834 |
. . . 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 836 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘(((ℤRHom‘𝑅)‘(numer‘𝑄))(/r‘𝑅)((ℤRHom‘𝑅)‘(denom‘𝑄)))) = ((𝑁‘((ℤRHom‘𝑅)‘(numer‘𝑄))) / (𝑁‘((ℤRHom‘𝑅)‘(denom‘𝑄))))) |
42 | | simpl2 1191 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑍 ∈
NrmMod) |
43 | | qqhnm.z |
. . . . . . 7
⊢ 𝑍 = (ℤMod‘𝑅) |
44 | 43 | zhmnrg 31917 |
. . . . . 6
⊢ (𝑅 ∈ NrmRing → 𝑍 ∈
NrmRing) |
45 | 25, 44 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
𝑍 ∈
NrmRing) |
46 | 18, 38, 43, 20 | zrhnm 31919 |
. . . . 5
⊢ (((𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧
(numer‘𝑄) ∈
ℤ) → (𝑁‘((ℤRHom‘𝑅)‘(numer‘𝑄))) = (abs‘(numer‘𝑄))) |
47 | 42, 45, 27, 6, 46 | syl31anc 1372 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℤRHom‘𝑅)‘(numer‘𝑄))) = (abs‘(numer‘𝑄))) |
48 | 18, 38, 43, 20 | zrhnm 31919 |
. . . . 5
⊢ (((𝑍 ∈ NrmMod ∧ 𝑍 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧
(denom‘𝑄) ∈
ℤ) → (𝑁‘((ℤRHom‘𝑅)‘(denom‘𝑄))) = (abs‘(denom‘𝑄))) |
49 | 42, 45, 27, 34, 48 | syl31anc 1372 |
. . . 4
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℤRHom‘𝑅)‘(denom‘𝑄))) = (abs‘(denom‘𝑄))) |
50 | 47, 49 | oveq12d 7293 |
. . 3
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((𝑁‘((ℤRHom‘𝑅)‘(numer‘𝑄))) / (𝑁‘((ℤRHom‘𝑅)‘(denom‘𝑄)))) = ((abs‘(numer‘𝑄)) /
(abs‘(denom‘𝑄)))) |
51 | 23, 41, 50 | 3eqtrrd 2783 |
. 2
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
((abs‘(numer‘𝑄)) / (abs‘(denom‘𝑄))) = (𝑁‘((ℚHom‘𝑅)‘𝑄))) |
52 | 4, 13, 51 | 3eqtrrd 2783 |
1
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑄 ∈ ℚ) →
(𝑁‘((ℚHom‘𝑅)‘𝑄)) = (abs‘𝑄)) |