Metamath Proof Explorer

Theorem qqhre

Description: The QQHom homomorphism for the real number structure is the identity. (Contributed by Thierry Arnoux, 31-Oct-2017)

Ref Expression
Assertion qqhre ⊢ℚHom⁡ℝfld=I↾ℚ

Proof

Step Hyp Ref Expression
1 resubdrg ⊢ℝ∈SubRing⁡ℂfld∧ℝfld∈DivRing
2 1 simpri ⊢ℝfld∈DivRing
3 drngring ⊢ℝfld∈DivRing→ℝfld∈Ring
4 f1oi ⊢I↾ℤ:ℤ⟶1-1 ontoℤ
5 f1of1 ⊢I↾ℤ:ℤ⟶1-1 ontoℤ→I↾ℤ:ℤ⟶1-1ℤ
6 4 5 ax-mp ⊢I↾ℤ:ℤ⟶1-1ℤ
7 zssre ⊢ℤ⊆ℝ
8 f1ss ⊢I↾ℤ:ℤ⟶1-1ℤ∧ℤ⊆ℝ→I↾ℤ:ℤ⟶1-1ℝ
9 6 7 8 mp2an ⊢I↾ℤ:ℤ⟶1-1ℝ
10 zrhre ⊢ℤRHom⁡ℝfld=I↾ℤ
11 f1eq1 ⊢ℤRHom⁡ℝfld=I↾ℤ→ℤRHom⁡ℝfld:ℤ⟶1-1ℝ↔I↾ℤ:ℤ⟶1-1ℝ
12 10 11 ax-mp ⊢ℤRHom⁡ℝfld:ℤ⟶1-1ℝ↔I↾ℤ:ℤ⟶1-1ℝ
13 9 12 mpbir ⊢ℤRHom⁡ℝfld:ℤ⟶1-1ℝ
14 rebase ⊢ℝ=Baseℝfld
15 eqid ⊢ℤRHom⁡ℝfld=ℤRHom⁡ℝfld
16 re0g ⊢0=0ℝfld
17 14 15 16 zrhchr ⊢ℝfld∈Ring→chr⁡ℝfld=0↔ℤRHom⁡ℝfld:ℤ⟶1-1ℝ
18 13 17 mpbiri ⊢ℝfld∈Ring→chr⁡ℝfld=0
19 2 3 18 mp2b ⊢chr⁡ℝfld=0
20 eqid ⊢/r⁡ℝfld=/r⁡ℝfld
21 14 20 15 qqhvval ⊢ℝfld∈DivRing∧chr⁡ℝfld=0∧q∈ℚ→ℚHom⁡ℝfld⁡q=ℤRHom⁡ℝfld⁡numer⁡q/r⁡ℝfldℤRHom⁡ℝfld⁡denom⁡q
22 2 19 21 mpanl12 ⊢q∈ℚ→ℚHom⁡ℝfld⁡q=ℤRHom⁡ℝfld⁡numer⁡q/r⁡ℝfldℤRHom⁡ℝfld⁡denom⁡q
23 f1f ⊢ℤRHom⁡ℝfld:ℤ⟶1-1ℝ→ℤRHom⁡ℝfld:ℤ⟶ℝ
24 13 23 ax-mp ⊢ℤRHom⁡ℝfld:ℤ⟶ℝ
25 24 a1i ⊢q∈ℚ→ℤRHom⁡ℝfld:ℤ⟶ℝ
26 qnumcl ⊢q∈ℚ→numer⁡q∈ℤ
27 25 26 ffvelcdmd ⊢q∈ℚ→ℤRHom⁡ℝfld⁡numer⁡q∈ℝ
28 qdencl ⊢q∈ℚ→denom⁡q∈ℕ
29 28 nnzd ⊢q∈ℚ→denom⁡q∈ℤ
30 25 29 ffvelcdmd ⊢q∈ℚ→ℤRHom⁡ℝfld⁡denom⁡q∈ℝ
31 29 anim1i ⊢q∈ℚ∧ℤRHom⁡ℝfld⁡denom⁡q=0→denom⁡q∈ℤ∧ℤRHom⁡ℝfld⁡denom⁡q=0
32 14 15 16 zrhf1ker ⊢ℝfld∈Ring→ℤRHom⁡ℝfld:ℤ⟶1-1ℝ↔ℤRHom⁡ℝfld-10=0
33 2 3 32 mp2b ⊢ℤRHom⁡ℝfld:ℤ⟶1-1ℝ↔ℤRHom⁡ℝfld-10=0
34 13 33 mpbi ⊢ℤRHom⁡ℝfld-10=0
35 34 eleq2i ⊢denom⁡q∈ℤRHom⁡ℝfld-10↔denom⁡q∈0
36 ffn ⊢ℤRHom⁡ℝfld:ℤ⟶ℝ→ℤRHom⁡ℝfldFnℤ
37 fniniseg ⊢ℤRHom⁡ℝfldFnℤ→denom⁡q∈ℤRHom⁡ℝfld-10↔denom⁡q∈ℤ∧ℤRHom⁡ℝfld⁡denom⁡q=0
38 24 36 37 mp2b ⊢denom⁡q∈ℤRHom⁡ℝfld-10↔denom⁡q∈ℤ∧ℤRHom⁡ℝfld⁡denom⁡q=0
39 fvex ⊢denom⁡q∈V
40 39 elsn ⊢denom⁡q∈0↔denom⁡q=0
41 35 38 40 3bitr3ri ⊢denom⁡q=0↔denom⁡q∈ℤ∧ℤRHom⁡ℝfld⁡denom⁡q=0
42 31 41 sylibr ⊢q∈ℚ∧ℤRHom⁡ℝfld⁡denom⁡q=0→denom⁡q=0
43 28 nnne0d ⊢q∈ℚ→denom⁡q≠0
44 43 adantr ⊢q∈ℚ∧ℤRHom⁡ℝfld⁡denom⁡q=0→denom⁡q≠0
45 44 neneqd ⊢q∈ℚ∧ℤRHom⁡ℝfld⁡denom⁡q=0→¬denom⁡q=0
46 42 45 pm2.65da ⊢q∈ℚ→¬ℤRHom⁡ℝfld⁡denom⁡q=0
47 46 neqned ⊢q∈ℚ→ℤRHom⁡ℝfld⁡denom⁡q≠0
48 redvr ⊢ℤRHom⁡ℝfld⁡numer⁡q∈ℝ∧ℤRHom⁡ℝfld⁡denom⁡q∈ℝ∧ℤRHom⁡ℝfld⁡denom⁡q≠0→ℤRHom⁡ℝfld⁡numer⁡q/r⁡ℝfldℤRHom⁡ℝfld⁡denom⁡q=ℤRHom⁡ℝfld⁡numer⁡qℤRHom⁡ℝfld⁡denom⁡q
49 27 30 47 48 syl3anc ⊢q∈ℚ→ℤRHom⁡ℝfld⁡numer⁡q/r⁡ℝfldℤRHom⁡ℝfld⁡denom⁡q=ℤRHom⁡ℝfld⁡numer⁡qℤRHom⁡ℝfld⁡denom⁡q
50 10 fveq1i ⊢ℤRHom⁡ℝfld⁡numer⁡q=I↾ℤ⁡numer⁡q
51 fvresi ⊢numer⁡q∈ℤ→I↾ℤ⁡numer⁡q=numer⁡q
52 50 51 eqtrid ⊢numer⁡q∈ℤ→ℤRHom⁡ℝfld⁡numer⁡q=numer⁡q
53 26 52 syl ⊢q∈ℚ→ℤRHom⁡ℝfld⁡numer⁡q=numer⁡q
54 10 fveq1i ⊢ℤRHom⁡ℝfld⁡denom⁡q=I↾ℤ⁡denom⁡q
55 fvresi ⊢denom⁡q∈ℤ→I↾ℤ⁡denom⁡q=denom⁡q
56 54 55 eqtrid ⊢denom⁡q∈ℤ→ℤRHom⁡ℝfld⁡denom⁡q=denom⁡q
57 29 56 syl ⊢q∈ℚ→ℤRHom⁡ℝfld⁡denom⁡q=denom⁡q
58 53 57 oveq12d ⊢q∈ℚ→ℤRHom⁡ℝfld⁡numer⁡qℤRHom⁡ℝfld⁡denom⁡q=numer⁡qdenom⁡q
59 qeqnumdivden ⊢q∈ℚ→q=numer⁡qdenom⁡q
60 58 59 eqtr4d ⊢q∈ℚ→ℤRHom⁡ℝfld⁡numer⁡qℤRHom⁡ℝfld⁡denom⁡q=q
61 22 49 60 3eqtrd ⊢q∈ℚ→ℚHom⁡ℝfld⁡q=q
62 61 mpteq2ia ⊢q∈ℚ⟼ℚHom⁡ℝfld⁡q=q∈ℚ⟼q
63 14 20 15 qqhf ⊢ℝfld∈DivRing∧chr⁡ℝfld=0→ℚHom⁡ℝfld:ℚ⟶ℝ
64 2 19 63 mp2an ⊢ℚHom⁡ℝfld:ℚ⟶ℝ
65 64 a1i ⊢⊤→ℚHom⁡ℝfld:ℚ⟶ℝ
66 65 feqmptd ⊢⊤→ℚHom⁡ℝfld=q∈ℚ⟼ℚHom⁡ℝfld⁡q
67 66 mptru ⊢ℚHom⁡ℝfld=q∈ℚ⟼ℚHom⁡ℝfld⁡q
68 mptresid ⊢I↾ℚ=q∈ℚ⟼q
69 62 67 68 3eqtr4i ⊢ℚHom⁡ℝfld=I↾ℚ