Proof of Theorem qqhre
Step | Hyp | Ref
| Expression |
1 | | resubdrg 19954 |
. . . . . . 7
⊢ (ℝ
∈ (SubRing‘ℂfld) ∧ ℝfld ∈
DivRing) |
2 | 1 | simpri 478 |
. . . . . 6
⊢
ℝfld ∈ DivRing |
3 | | drngring 18754 |
. . . . . . 7
⊢
(ℝfld ∈ DivRing → ℝfld
∈ Ring) |
4 | | f1oi 6174 |
. . . . . . . . . . 11
⊢ ( I
↾ ℤ):ℤ–1-1-onto→ℤ |
5 | | f1of1 6136 |
. . . . . . . . . . 11
⊢ (( I
↾ ℤ):ℤ–1-1-onto→ℤ → ( I ↾
ℤ):ℤ–1-1→ℤ) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . 10
⊢ ( I
↾ ℤ):ℤ–1-1→ℤ |
7 | | zssre 11384 |
. . . . . . . . . 10
⊢ ℤ
⊆ ℝ |
8 | | f1ss 6106 |
. . . . . . . . . 10
⊢ ((( I
↾ ℤ):ℤ–1-1→ℤ ∧ ℤ ⊆ ℝ) → (
I ↾ ℤ):ℤ–1-1→ℝ) |
9 | 6, 7, 8 | mp2an 708 |
. . . . . . . . 9
⊢ ( I
↾ ℤ):ℤ–1-1→ℝ |
10 | | zrhre 30063 |
. . . . . . . . . 10
⊢
(ℤRHom‘ℝfld) = ( I ↾
ℤ) |
11 | | f1eq1 6096 |
. . . . . . . . . 10
⊢
((ℤRHom‘ℝfld) = ( I ↾ ℤ) →
((ℤRHom‘ℝfld):ℤ–1-1→ℝ ↔ ( I ↾
ℤ):ℤ–1-1→ℝ)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢
((ℤRHom‘ℝfld):ℤ–1-1→ℝ ↔ ( I ↾
ℤ):ℤ–1-1→ℝ) |
13 | 9, 12 | mpbir 221 |
. . . . . . . 8
⊢
(ℤRHom‘ℝfld):ℤ–1-1→ℝ |
14 | | rebase 19952 |
. . . . . . . . 9
⊢ ℝ =
(Base‘ℝfld) |
15 | | eqid 2622 |
. . . . . . . . 9
⊢
(ℤRHom‘ℝfld) =
(ℤRHom‘ℝfld) |
16 | | re0g 19958 |
. . . . . . . . 9
⊢ 0 =
(0g‘ℝfld) |
17 | 14, 15, 16 | zrhchr 30020 |
. . . . . . . 8
⊢
(ℝfld ∈ Ring →
((chr‘ℝfld) = 0 ↔
(ℤRHom‘ℝfld):ℤ–1-1→ℝ)) |
18 | 13, 17 | mpbiri 248 |
. . . . . . 7
⊢
(ℝfld ∈ Ring →
(chr‘ℝfld) = 0) |
19 | 2, 3, 18 | mp2b 10 |
. . . . . 6
⊢
(chr‘ℝfld) = 0 |
20 | | eqid 2622 |
. . . . . . 7
⊢
(/r‘ℝfld) =
(/r‘ℝfld) |
21 | 14, 20, 15 | qqhf 30030 |
. . . . . 6
⊢
((ℝfld ∈ DivRing ∧
(chr‘ℝfld) = 0) →
(ℚHom‘ℝfld):ℚ⟶ℝ) |
22 | 2, 19, 21 | mp2an 708 |
. . . . 5
⊢
(ℚHom‘ℝfld):ℚ⟶ℝ |
23 | 22 | a1i 11 |
. . . 4
⊢ (⊤
→
(ℚHom‘ℝfld):ℚ⟶ℝ) |
24 | 23 | feqmptd 6249 |
. . 3
⊢ (⊤
→ (ℚHom‘ℝfld) = (𝑞 ∈ ℚ ↦
((ℚHom‘ℝfld)‘𝑞))) |
25 | 24 | trud 1493 |
. 2
⊢
(ℚHom‘ℝfld) = (𝑞 ∈ ℚ ↦
((ℚHom‘ℝfld)‘𝑞)) |
26 | 14, 20, 15 | qqhvval 30027 |
. . . . 5
⊢
(((ℝfld ∈ DivRing ∧
(chr‘ℝfld) = 0) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘ℝfld)‘𝑞) =
(((ℤRHom‘ℝfld)‘(numer‘𝑞))(/r‘ℝfld)((ℤRHom‘ℝfld)‘(denom‘𝑞)))) |
27 | 2, 19, 26 | mpanl12 718 |
. . . 4
⊢ (𝑞 ∈ ℚ →
((ℚHom‘ℝfld)‘𝑞) =
(((ℤRHom‘ℝfld)‘(numer‘𝑞))(/r‘ℝfld)((ℤRHom‘ℝfld)‘(denom‘𝑞)))) |
28 | | f1f 6101 |
. . . . . . . 8
⊢
((ℤRHom‘ℝfld):ℤ–1-1→ℝ →
(ℤRHom‘ℝfld):ℤ⟶ℝ) |
29 | 13, 28 | ax-mp 5 |
. . . . . . 7
⊢
(ℤRHom‘ℝfld):ℤ⟶ℝ |
30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
(ℤRHom‘ℝfld):ℤ⟶ℝ) |
31 | | qnumcl 15448 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
(numer‘𝑞) ∈
ℤ) |
32 | 30, 31 | ffvelrnd 6360 |
. . . . 5
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(numer‘𝑞)) ∈
ℝ) |
33 | | qdencl 15449 |
. . . . . . 7
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
ℕ) |
34 | 33 | nnzd 11481 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
ℤ) |
35 | 30, 34 | ffvelrnd 6360 |
. . . . 5
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(denom‘𝑞)) ∈
ℝ) |
36 | 34 | anim1i 592 |
. . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) →
((denom‘𝑞) ∈
ℤ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0)) |
37 | 14, 15, 16 | zrhf1ker 30019 |
. . . . . . . . . . . 12
⊢
(ℝfld ∈ Ring →
((ℤRHom‘ℝfld):ℤ–1-1→ℝ ↔ (◡(ℤRHom‘ℝfld)
“ {0}) = {0})) |
38 | 2, 3, 37 | mp2b 10 |
. . . . . . . . . . 11
⊢
((ℤRHom‘ℝfld):ℤ–1-1→ℝ ↔ (◡(ℤRHom‘ℝfld)
“ {0}) = {0}) |
39 | 13, 38 | mpbi 220 |
. . . . . . . . . 10
⊢ (◡(ℤRHom‘ℝfld)
“ {0}) = {0} |
40 | 39 | eleq2i 2693 |
. . . . . . . . 9
⊢
((denom‘𝑞)
∈ (◡(ℤRHom‘ℝfld)
“ {0}) ↔ (denom‘𝑞) ∈ {0}) |
41 | | ffn 6045 |
. . . . . . . . . 10
⊢
((ℤRHom‘ℝfld):ℤ⟶ℝ →
(ℤRHom‘ℝfld) Fn ℤ) |
42 | | fniniseg 6338 |
. . . . . . . . . 10
⊢
((ℤRHom‘ℝfld) Fn ℤ →
((denom‘𝑞) ∈
(◡(ℤRHom‘ℝfld)
“ {0}) ↔ ((denom‘𝑞) ∈ ℤ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0))) |
43 | 29, 41, 42 | mp2b 10 |
. . . . . . . . 9
⊢
((denom‘𝑞)
∈ (◡(ℤRHom‘ℝfld)
“ {0}) ↔ ((denom‘𝑞) ∈ ℤ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0)) |
44 | | fvex 6201 |
. . . . . . . . . 10
⊢
(denom‘𝑞)
∈ V |
45 | 44 | elsn 4192 |
. . . . . . . . 9
⊢
((denom‘𝑞)
∈ {0} ↔ (denom‘𝑞) = 0) |
46 | 40, 43, 45 | 3bitr3ri 291 |
. . . . . . . 8
⊢
((denom‘𝑞) = 0
↔ ((denom‘𝑞)
∈ ℤ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0)) |
47 | 36, 46 | sylibr 224 |
. . . . . . 7
⊢ ((𝑞 ∈ ℚ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) →
(denom‘𝑞) =
0) |
48 | 33 | nnne0d 11065 |
. . . . . . . . 9
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ≠
0) |
49 | 48 | adantr 481 |
. . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) →
(denom‘𝑞) ≠
0) |
50 | 49 | neneqd 2799 |
. . . . . . 7
⊢ ((𝑞 ∈ ℚ ∧
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) → ¬
(denom‘𝑞) =
0) |
51 | 47, 50 | pm2.65da 600 |
. . . . . 6
⊢ (𝑞 ∈ ℚ → ¬
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = 0) |
52 | 51 | neqned 2801 |
. . . . 5
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(denom‘𝑞)) ≠ 0) |
53 | | redvr 19963 |
. . . . 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‘𝑞)))) |
54 | 32, 35, 52, 53 | syl3anc 1326 |
. . . 4
⊢ (𝑞 ∈ ℚ →
(((ℤRHom‘ℝfld)‘(numer‘𝑞))(/r‘ℝfld)((ℤRHom‘ℝfld)‘(denom‘𝑞))) = (((ℤRHom‘ℝfld)‘(numer‘𝑞)) / ((ℤRHom‘ℝfld)‘(denom‘𝑞)))) |
55 | 10 | fveq1i 6192 |
. . . . . . . 8
⊢
((ℤRHom‘ℝfld)‘(numer‘𝑞)) = (( I ↾
ℤ)‘(numer‘𝑞)) |
56 | | fvresi 6439 |
. . . . . . . 8
⊢
((numer‘𝑞)
∈ ℤ → (( I ↾ ℤ)‘(numer‘𝑞)) = (numer‘𝑞)) |
57 | 55, 56 | syl5eq 2668 |
. . . . . . 7
⊢
((numer‘𝑞)
∈ ℤ →
((ℤRHom‘ℝfld)‘(numer‘𝑞)) = (numer‘𝑞)) |
58 | 31, 57 | syl 17 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(numer‘𝑞)) = (numer‘𝑞)) |
59 | 10 | fveq1i 6192 |
. . . . . . . 8
⊢
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = (( I ↾
ℤ)‘(denom‘𝑞)) |
60 | | fvresi 6439 |
. . . . . . . 8
⊢
((denom‘𝑞)
∈ ℤ → (( I ↾ ℤ)‘(denom‘𝑞)) = (denom‘𝑞)) |
61 | 59, 60 | syl5eq 2668 |
. . . . . . 7
⊢
((denom‘𝑞)
∈ ℤ →
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = (denom‘𝑞)) |
62 | 34, 61 | syl 17 |
. . . . . 6
⊢ (𝑞 ∈ ℚ →
((ℤRHom‘ℝfld)‘(denom‘𝑞)) = (denom‘𝑞)) |
63 | 58, 62 | oveq12d 6668 |
. . . . 5
⊢ (𝑞 ∈ ℚ →
(((ℤRHom‘ℝfld)‘(numer‘𝑞)) /
((ℤRHom‘ℝfld)‘(denom‘𝑞))) = ((numer‘𝑞) / (denom‘𝑞))) |
64 | | qeqnumdivden 15454 |
. . . . 5
⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞))) |
65 | 63, 64 | eqtr4d 2659 |
. . . 4
⊢ (𝑞 ∈ ℚ →
(((ℤRHom‘ℝfld)‘(numer‘𝑞)) /
((ℤRHom‘ℝfld)‘(denom‘𝑞))) = 𝑞) |
66 | 27, 54, 65 | 3eqtrd 2660 |
. . 3
⊢ (𝑞 ∈ ℚ →
((ℚHom‘ℝfld)‘𝑞) = 𝑞) |
67 | 66 | mpteq2ia 4740 |
. 2
⊢ (𝑞 ∈ ℚ ↦
((ℚHom‘ℝfld)‘𝑞)) = (𝑞 ∈ ℚ ↦ 𝑞) |
68 | | mptresid 5456 |
. 2
⊢ (𝑞 ∈ ℚ ↦ 𝑞) = ( I ↾
ℚ) |
69 | 25, 67, 68 | 3eqtri 2648 |
1
⊢
(ℚHom‘ℝfld) = ( I ↾
ℚ) |