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 ffvelrnd ⊢ q ∈ ℚ → ℤRHom ⁡ ℝ fld ⁡ numer ⁡ q ∈ ℝ
28 qdencl ⊢ q ∈ ℚ → denom ⁡ q ∈ ℕ
29 28 nnzd ⊢ q ∈ ℚ → denom ⁡ q ∈ ℤ
30 25 29 ffvelrnd ⊢ 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 -1 0 = 0
33 2 3 32 mp2b ⊢ ℤRHom ⁡ ℝ fld : ℤ ⟶ 1-1 ℝ ↔ ℤRHom ⁡ ℝ fld -1 0 = 0
34 13 33 mpbi ⊢ ℤRHom ⁡ ℝ fld -1 0 = 0
35 34 eleq2i ⊢ denom ⁡ q ∈ ℤRHom ⁡ ℝ fld -1 0 ↔ denom ⁡ q ∈ 0
36 ffn ⊢ ℤRHom ⁡ ℝ fld : ℤ ⟶ ℝ → ℤRHom ⁡ ℝ fld Fn ℤ
37 fniniseg ⊢ ℤRHom ⁡ ℝ fld Fn ℤ → denom ⁡ q ∈ ℤRHom ⁡ ℝ fld -1 0 ↔ denom ⁡ q ∈ ℤ ∧ ℤRHom ⁡ ℝ fld ⁡ denom ⁡ q = 0
38 24 36 37 mp2b ⊢ denom ⁡ q ∈ ℤRHom ⁡ ℝ fld -1 0 ↔ 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 syl5eq ⊢ 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 syl5eq ⊢ 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 ⁡ q denom ⁡ q
59 qeqnumdivden ⊢ q ∈ ℚ → q = numer ⁡ q denom ⁡ 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 ↾ ℚ