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 = ( 0g ‘ ℝ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 ) ∧ 𝑞 ∈ ℚ ) → ( ( ℚHom ‘ ℝfld ) ‘ 𝑞 ) = ( ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) ( /r ‘ ℝfld ) ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) ) )
22 2 19 21 mpanl12 ⊢ ( 𝑞 ∈ ℚ → ( ( ℚHom ‘ ℝfld ) ‘ 𝑞 ) = ( ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) ( /r ‘ ℝfld ) ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) ) )
23 f1f ⊢ ( ( ℤRHom ‘ ℝfld ) : ℤ –1-1→ ℝ → ( ℤRHom ‘ ℝfld ) : ℤ ⟶ ℝ )
24 13 23 ax-mp ⊢ ( ℤRHom ‘ ℝfld ) : ℤ ⟶ ℝ
25 24 a1i ⊢ ( 𝑞 ∈ ℚ → ( ℤRHom ‘ ℝfld ) : ℤ ⟶ ℝ )
26 qnumcl ⊢ ( 𝑞 ∈ ℚ → ( numer ‘ 𝑞 ) ∈ ℤ )
27 25 26 ffvelcdmd ⊢ ( 𝑞 ∈ ℚ → ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) ∈ ℝ )
28 qdencl ⊢ ( 𝑞 ∈ ℚ → ( denom ‘ 𝑞 ) ∈ ℕ )
29 28 nnzd ⊢ ( 𝑞 ∈ ℚ → ( denom ‘ 𝑞 ) ∈ ℤ )
30 25 29 ffvelcdmd ⊢ ( 𝑞 ∈ ℚ → ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) ∈ ℝ )
31 29 anim1i ⊢ ( ( 𝑞 ∈ ℚ ∧ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = 0 ) → ( ( denom ‘ 𝑞 ) ∈ ℤ ∧ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = 0 ) )
32 14 15 16 zrhf1ker ⊢ ( ℝfld ∈ Ring → ( ( ℤRHom ‘ ℝfld ) : ℤ –1-1→ ℝ ↔ ( ◡ ( ℤRHom ‘ ℝfld ) “ { 0 } ) = { 0 } ) )
33 2 3 32 mp2b ⊢ ( ( ℤRHom ‘ ℝfld ) : ℤ –1-1→ ℝ ↔ ( ◡ ( ℤRHom ‘ ℝfld ) “ { 0 } ) = { 0 } )
34 13 33 mpbi ⊢ ( ◡ ( ℤRHom ‘ ℝfld ) “ { 0 } ) = { 0 }
35 34 eleq2i ⊢ ( ( denom ‘ 𝑞 ) ∈ ( ◡ ( ℤRHom ‘ ℝfld ) “ { 0 } ) ↔ ( denom ‘ 𝑞 ) ∈ { 0 } )
36 ffn ⊢ ( ( ℤRHom ‘ ℝfld ) : ℤ ⟶ ℝ → ( ℤRHom ‘ ℝfld ) Fn ℤ )
37 fniniseg ⊢ ( ( ℤRHom ‘ ℝfld ) Fn ℤ → ( ( denom ‘ 𝑞 ) ∈ ( ◡ ( ℤRHom ‘ ℝfld ) “ { 0 } ) ↔ ( ( denom ‘ 𝑞 ) ∈ ℤ ∧ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = 0 ) ) )
38 24 36 37 mp2b ⊢ ( ( denom ‘ 𝑞 ) ∈ ( ◡ ( ℤRHom ‘ ℝfld ) “ { 0 } ) ↔ ( ( denom ‘ 𝑞 ) ∈ ℤ ∧ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = 0 ) )
39 fvex ⊢ ( denom ‘ 𝑞 ) ∈ V
40 39 elsn ⊢ ( ( denom ‘ 𝑞 ) ∈ { 0 } ↔ ( denom ‘ 𝑞 ) = 0 )
41 35 38 40 3bitr3ri ⊢ ( ( denom ‘ 𝑞 ) = 0 ↔ ( ( denom ‘ 𝑞 ) ∈ ℤ ∧ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = 0 ) )
42 31 41 sylibr ⊢ ( ( 𝑞 ∈ ℚ ∧ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = 0 ) → ( denom ‘ 𝑞 ) = 0 )
43 28 nnne0d ⊢ ( 𝑞 ∈ ℚ → ( denom ‘ 𝑞 ) ≠ 0 )
44 43 adantr ⊢ ( ( 𝑞 ∈ ℚ ∧ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = 0 ) → ( denom ‘ 𝑞 ) ≠ 0 )
45 44 neneqd ⊢ ( ( 𝑞 ∈ ℚ ∧ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = 0 ) → ¬ ( denom ‘ 𝑞 ) = 0 )
46 42 45 pm2.65da ⊢ ( 𝑞 ∈ ℚ → ¬ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = 0 )
47 46 neqned ⊢ ( 𝑞 ∈ ℚ → ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) ≠ 0 )
48 redvr ⊢ ( ( ( ( ℤ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 ⊢ ( 𝑞 ∈ ℚ → ( ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) ( /r ‘ ℝfld ) ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) ) = ( ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) / ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) ) )
50 10 fveq1i ⊢ ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) = ( ( I ↾ ℤ ) ‘ ( numer ‘ 𝑞 ) )
51 fvresi ⊢ ( ( numer ‘ 𝑞 ) ∈ ℤ → ( ( I ↾ ℤ ) ‘ ( numer ‘ 𝑞 ) ) = ( numer ‘ 𝑞 ) )
52 50 51 eqtrid ⊢ ( ( numer ‘ 𝑞 ) ∈ ℤ → ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) = ( numer ‘ 𝑞 ) )
53 26 52 syl ⊢ ( 𝑞 ∈ ℚ → ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) = ( numer ‘ 𝑞 ) )
54 10 fveq1i ⊢ ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = ( ( I ↾ ℤ ) ‘ ( denom ‘ 𝑞 ) )
55 fvresi ⊢ ( ( denom ‘ 𝑞 ) ∈ ℤ → ( ( I ↾ ℤ ) ‘ ( denom ‘ 𝑞 ) ) = ( denom ‘ 𝑞 ) )
56 54 55 eqtrid ⊢ ( ( denom ‘ 𝑞 ) ∈ ℤ → ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = ( denom ‘ 𝑞 ) )
57 29 56 syl ⊢ ( 𝑞 ∈ ℚ → ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) = ( denom ‘ 𝑞 ) )
58 53 57 oveq12d ⊢ ( 𝑞 ∈ ℚ → ( ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) / ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) ) = ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) )
59 qeqnumdivden ⊢ ( 𝑞 ∈ ℚ → 𝑞 = ( ( numer ‘ 𝑞 ) / ( denom ‘ 𝑞 ) ) )
60 58 59 eqtr4d ⊢ ( 𝑞 ∈ ℚ → ( ( ( ℤRHom ‘ ℝfld ) ‘ ( numer ‘ 𝑞 ) ) / ( ( ℤRHom ‘ ℝfld ) ‘ ( denom ‘ 𝑞 ) ) ) = 𝑞 )
61 22 49 60 3eqtrd ⊢ ( 𝑞 ∈ ℚ → ( ( ℚHom ‘ ℝfld ) ‘ 𝑞 ) = 𝑞 )
62 61 mpteq2ia ⊢ ( 𝑞 ∈ ℚ ↦ ( ( ℚHom ‘ ℝfld ) ‘ 𝑞 ) ) = ( 𝑞 ∈ ℚ ↦ 𝑞 )
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 ) = ( 𝑞 ∈ ℚ ↦ ( ( ℚHom ‘ ℝfld ) ‘ 𝑞 ) ) )
67 66 mptru ⊢ ( ℚHom ‘ ℝfld ) = ( 𝑞 ∈ ℚ ↦ ( ( ℚHom ‘ ℝfld ) ‘ 𝑞 ) )
68 mptresid ⊢ ( I ↾ ℚ ) = ( 𝑞 ∈ ℚ ↦ 𝑞 )
69 62 67 68 3eqtr4i ⊢ ( ℚHom ‘ ℝfld ) = ( I ↾ ℚ )