Proof of Theorem qqhre
Step | Hyp | Ref
| Expression |
1 | | resubdrg 20598 |
. . . . . 6
⊢ (ℝ
∈ (SubRing‘ℂfld) ∧ ℝfld ∈
DivRing) |
2 | 1 | simpri 489 |
. . . . 5
⊢
ℝfld ∈ DivRing |
3 | | drngring 19802 |
. . . . . 6
⊢
(ℝfld ∈ DivRing → ℝfld
∈ Ring) |
4 | | f1oi 6717 |
. . . . . . . . . 10
⊢ ( I
↾ ℤ):ℤ–1-1-onto→ℤ |
5 | | f1of1 6679 |
. . . . . . . . . 10
⊢ (( I
↾ ℤ):ℤ–1-1-onto→ℤ → ( I ↾
ℤ):ℤ–1-1→ℤ) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . 9
⊢ ( I
↾ ℤ):ℤ–1-1→ℤ |
7 | | zssre 12208 |
. . . . . . . . 9
⊢ ℤ
⊆ ℝ |
8 | | f1ss 6640 |
. . . . . . . . 9
⊢ ((( I
↾ ℤ):ℤ–1-1→ℤ ∧ ℤ ⊆ ℝ) → (
I ↾ ℤ):ℤ–1-1→ℝ) |
9 | 6, 7, 8 | mp2an 692 |
. . . . . . . 8
⊢ ( I
↾ ℤ):ℤ–1-1→ℝ |
10 | | zrhre 31708 |
. . . . . . . . 9
⊢
(ℤRHom‘ℝfld) = ( I ↾
ℤ) |
11 | | f1eq1 6629 |
. . . . . . . . 9
⊢
((ℤRHom‘ℝfld) = ( I ↾ ℤ) →
((ℤRHom‘ℝfld):ℤ–1-1→ℝ ↔ ( I ↾
ℤ):ℤ–1-1→ℝ)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . 8
⊢
((ℤRHom‘ℝfld):ℤ–1-1→ℝ ↔ ( I ↾
ℤ):ℤ–1-1→ℝ) |
13 | 9, 12 | mpbir 234 |
. . . . . . 7
⊢
(ℤRHom‘ℝfld):ℤ–1-1→ℝ |
14 | | rebase 20596 |
. . . . . . . 8
⊢ ℝ =
(Base‘ℝfld) |
15 | | eqid 2738 |
. . . . . . . 8
⊢
(ℤRHom‘ℝfld) =
(ℤRHom‘ℝfld) |
16 | | re0g 20602 |
. . . . . . . 8
⊢ 0 =
(0g‘ℝfld) |
17 | 14, 15, 16 | zrhchr 31665 |
. . . . . . 7
⊢
(ℝfld ∈ Ring →
((chr‘ℝfld) = 0 ↔
(ℤRHom‘ℝfld):ℤ–1-1→ℝ)) |
18 | 13, 17 | mpbiri 261 |
. . . . . 6
⊢
(ℝfld ∈ Ring →
(chr‘ℝfld) = 0) |
19 | 2, 3, 18 | mp2b 10 |
. . . . 5
⊢
(chr‘ℝfld) = 0 |
20 | | eqid 2738 |
. . . . . 6
⊢
(/r‘ℝfld) =
(/r‘ℝfld) |
21 | 14, 20, 15 | qqhvval 31672 |
. . . . 5
⊢
(((ℝfld ∈ DivRing ∧
(chr‘ℝfld) = 0) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘ℝfld)‘𝑞) =
(((ℤRHom‘ℝfld)‘(numer‘𝑞))(/r‘ℝfld)((ℤRHom‘ℝfld)‘(denom‘𝑞)))) |
22 | 2, 19, 21 | mpanl12 702 |
. . . 4
⊢ (𝑞 ∈ ℚ →
((ℚHom‘ℝfld)‘𝑞) =
(((ℤRHom‘ℝfld)‘(numer‘𝑞))(/r‘ℝfld)((ℤRHom‘ℝfld)‘(denom‘𝑞)))) |
23 | | f1f 6634 |
. . . . . . . 8
⊢
((ℤRHom‘ℝfld):ℤ–1-1→ℝ →
(ℤRHom‘ℝfld):ℤ⟶ℝ) |
24 | 13, 23 | ax-mp 5 |
. . . . . . 7
⊢
(ℤRHom‘ℝfld):ℤ⟶ℝ |
25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
(ℤRHom‘ℝfld):ℤ⟶ℝ) |
26 | | qnumcl 16324 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
(numer‘𝑞) ∈
ℤ) |
27 | 25, 26 | ffvelrnd 6924 |
. . . . 5
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(numer‘𝑞)) ∈
ℝ) |
28 | | qdencl 16325 |
. . . . . . 7
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
ℕ) |
29 | 28 | nnzd 12306 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
ℤ) |
30 | 25, 29 | ffvelrnd 6924 |
. . . . 5
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(denom‘𝑞)) ∈
ℝ) |
31 | 29 | anim1i 618 |
. . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) →
((denom‘𝑞) ∈
ℤ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0)) |
32 | 14, 15, 16 | zrhf1ker 31664 |
. . . . . . . . . . . 12
⊢
(ℝfld ∈ Ring →
((ℤRHom‘ℝfld):ℤ–1-1→ℝ ↔ (◡(ℤRHom‘ℝfld)
“ {0}) = {0})) |
33 | 2, 3, 32 | mp2b 10 |
. . . . . . . . . . 11
⊢
((ℤRHom‘ℝfld):ℤ–1-1→ℝ ↔ (◡(ℤRHom‘ℝfld)
“ {0}) = {0}) |
34 | 13, 33 | mpbi 233 |
. . . . . . . . . 10
⊢ (◡(ℤRHom‘ℝfld)
“ {0}) = {0} |
35 | 34 | eleq2i 2830 |
. . . . . . . . 9
⊢
((denom‘𝑞)
∈ (◡(ℤRHom‘ℝfld)
“ {0}) ↔ (denom‘𝑞) ∈ {0}) |
36 | | ffn 6564 |
. . . . . . . . . 10
⊢
((ℤRHom‘ℝfld):ℤ⟶ℝ →
(ℤRHom‘ℝfld) Fn ℤ) |
37 | | fniniseg 6899 |
. . . . . . . . . 10
⊢
((ℤRHom‘ℝfld) Fn ℤ →
((denom‘𝑞) ∈
(◡(ℤRHom‘ℝfld)
“ {0}) ↔ ((denom‘𝑞) ∈ ℤ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0))) |
38 | 24, 36, 37 | mp2b 10 |
. . . . . . . . 9
⊢
((denom‘𝑞)
∈ (◡(ℤRHom‘ℝfld)
“ {0}) ↔ ((denom‘𝑞) ∈ ℤ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0)) |
39 | | fvex 6749 |
. . . . . . . . . 10
⊢
(denom‘𝑞)
∈ V |
40 | 39 | elsn 4571 |
. . . . . . . . 9
⊢
((denom‘𝑞)
∈ {0} ↔ (denom‘𝑞) = 0) |
41 | 35, 38, 40 | 3bitr3ri 305 |
. . . . . . . 8
⊢
((denom‘𝑞) = 0
↔ ((denom‘𝑞)
∈ ℤ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0)) |
42 | 31, 41 | sylibr 237 |
. . . . . . 7
⊢ ((𝑞 ∈ ℚ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) →
(denom‘𝑞) =
0) |
43 | 28 | nnne0d 11905 |
. . . . . . . . 9
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ≠
0) |
44 | 43 | adantr 484 |
. . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) →
(denom‘𝑞) ≠
0) |
45 | 44 | neneqd 2946 |
. . . . . . 7
⊢ ((𝑞 ∈ ℚ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) → ¬
(denom‘𝑞) =
0) |
46 | 42, 45 | pm2.65da 817 |
. . . . . 6
⊢ (𝑞 ∈ ℚ → ¬
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) |
47 | 46 | neqned 2948 |
. . . . 5
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(denom‘𝑞)) ≠ 0) |
48 | | redvr 20607 |
. . . . 5
⊢
((((ℤRHom‘ℝfld)‘(numer‘𝑞)) ∈ ℝ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) ∈ ℝ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) ≠ 0) →
(((ℤRHom‘ℝfld)‘(numer‘𝑞))(/r‘ℝfld)((ℤRHom‘ℝfld)‘(denom‘𝑞))) = (((ℤRHom‘ℝfld)‘(numer‘𝑞)) / ((ℤRHom‘ℝfld)‘(denom‘𝑞)))) |
49 | 27, 30, 47, 48 | syl3anc 1373 |
. . . 4
⊢ (𝑞 ∈ ℚ →
(((ℤRHom‘ℝfld)‘(numer‘𝑞))(/r‘ℝfld)((ℤRHom‘ℝfld)‘(denom‘𝑞))) = (((ℤRHom‘ℝfld)‘(numer‘𝑞)) / ((ℤRHom‘ℝfld)‘(denom‘𝑞)))) |
50 | 10 | fveq1i 6737 |
. . . . . . . 8
⊢
((ℤRHom‘ℝfld)‘(numer‘𝑞)) = (( I ↾
ℤ)‘(numer‘𝑞)) |
51 | | fvresi 7007 |
. . . . . . . 8
⊢
((numer‘𝑞)
∈ ℤ → (( I ↾ ℤ)‘(numer‘𝑞)) = (numer‘𝑞)) |
52 | 50, 51 | syl5eq 2791 |
. . . . . . 7
⊢
((numer‘𝑞)
∈ ℤ →
((ℤRHom‘ℝfld)‘(numer‘𝑞)) = (numer‘𝑞)) |
53 | 26, 52 | syl 17 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(numer‘𝑞)) = (numer‘𝑞)) |
54 | 10 | fveq1i 6737 |
. . . . . . . 8
⊢
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = (( I ↾
ℤ)‘(denom‘𝑞)) |
55 | | fvresi 7007 |
. . . . . . . 8
⊢
((denom‘𝑞)
∈ ℤ → (( I ↾ ℤ)‘(denom‘𝑞)) = (denom‘𝑞)) |
56 | 54, 55 | syl5eq 2791 |
. . . . . . 7
⊢
((denom‘𝑞)
∈ ℤ →
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = (denom‘𝑞)) |
57 | 29, 56 | syl 17 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = (denom‘𝑞)) |
58 | 53, 57 | oveq12d 7250 |
. . . . 5
⊢ (𝑞 ∈ ℚ →
(((ℤRHom‘ℝfld)‘(numer‘𝑞)) /
((ℤRHom‘ℝfld)‘(denom‘𝑞))) = ((numer‘𝑞) / (denom‘𝑞))) |
59 | | qeqnumdivden 16330 |
. . . . 5
⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞))) |
60 | 58, 59 | eqtr4d 2781 |
. . . 4
⊢ (𝑞 ∈ ℚ →
(((ℤRHom‘ℝfld)‘(numer‘𝑞)) /
((ℤRHom‘ℝfld)‘(denom‘𝑞))) = 𝑞) |
61 | 22, 49, 60 | 3eqtrd 2782 |
. . 3
⊢ (𝑞 ∈ ℚ →
((ℚHom‘ℝfld)‘𝑞) = 𝑞) |
62 | 61 | mpteq2ia 5161 |
. 2
⊢ (𝑞 ∈ ℚ ↦
((ℚHom‘ℝfld)‘𝑞)) = (𝑞 ∈ ℚ ↦ 𝑞) |
63 | 14, 20, 15 | qqhf 31675 |
. . . . . 6
⊢
((ℝfld ∈ DivRing ∧
(chr‘ℝfld) = 0) →
(ℚHom‘ℝfld):ℚ⟶ℝ) |
64 | 2, 19, 63 | mp2an 692 |
. . . . 5
⊢
(ℚHom‘ℝfld):ℚ⟶ℝ |
65 | 64 | a1i 11 |
. . . 4
⊢ (⊤
→
(ℚHom‘ℝfld):ℚ⟶ℝ) |
66 | 65 | feqmptd 6799 |
. . 3
⊢ (⊤
→ (ℚHom‘ℝfld) = (𝑞 ∈ ℚ ↦
((ℚHom‘ℝfld)‘𝑞))) |
67 | 66 | mptru 1550 |
. 2
⊢
(ℚHom‘ℝfld) = (𝑞 ∈ ℚ ↦
((ℚHom‘ℝfld)‘𝑞)) |
68 | | mptresid 5933 |
. 2
⊢ ( I
↾ ℚ) = (𝑞
∈ ℚ ↦ 𝑞) |
69 | 62, 67, 68 | 3eqtr4i 2776 |
1
⊢
(ℚHom‘ℝfld) = ( I ↾
ℚ) |