Metamath Proof Explorer

Theorem zrhre

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

Ref Expression
Assertion zrhre ⊢ ℤRHom ⁡ ℝ fld = I ↾ ℤ

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 remulg ⊢ n ∈ ℤ ∧ 1 ∈ ℝ → n ⋅ ℝ fld 1 = n ⋅ 1
3 1 2 mpan2 ⊢ n ∈ ℤ → n ⋅ ℝ fld 1 = n ⋅ 1
4 zre ⊢ n ∈ ℤ → n ∈ ℝ
5 ax-1rid ⊢ n ∈ ℝ → n ⋅ 1 = n
6 4 5 syl ⊢ n ∈ ℤ → n ⋅ 1 = n
7 3 6 eqtrd ⊢ n ∈ ℤ → n ⋅ ℝ fld 1 = n
8 7 mpteq2ia ⊢ n ∈ ℤ ⟼ n ⋅ ℝ fld 1 = n ∈ ℤ ⟼ n
9 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
10 9 simpri ⊢ ℝ fld ∈ DivRing
11 drngring ⊢ ℝ fld ∈ DivRing → ℝ fld ∈ Ring
12 eqid ⊢ ℤRHom ⁡ ℝ fld = ℤRHom ⁡ ℝ fld
13 eqid ⊢ ⋅ ℝ fld = ⋅ ℝ fld
14 re1r ⊢ 1 = 1 ℝ fld
15 12 13 14 zrhval2 ⊢ ℝ fld ∈ Ring → ℤRHom ⁡ ℝ fld = n ∈ ℤ ⟼ n ⋅ ℝ fld 1
16 10 11 15 mp2b ⊢ ℤRHom ⁡ ℝ fld = n ∈ ℤ ⟼ n ⋅ ℝ fld 1
17 mptresid ⊢ I ↾ ℤ = n ∈ ℤ ⟼ n
18 8 16 17 3eqtr4i ⊢ ℤRHom ⁡ ℝ fld = I ↾ ℤ