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	⊢ ( ( 𝑛 ∈ ℤ ∧ 1 ∈ ℝ ) → ( 𝑛 ( .g ‘ ℝfld ) 1 ) = ( 𝑛 · 1 ) )
3	1 2	mpan2	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ( .g ‘ ℝfld ) 1 ) = ( 𝑛 · 1 ) )
4		zre	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℝ )
5		ax-1rid	⊢ ( 𝑛 ∈ ℝ → ( 𝑛 · 1 ) = 𝑛 )
6	4 5	syl	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · 1 ) = 𝑛 )
7	3 6	eqtrd	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ( .g ‘ ℝfld ) 1 ) = 𝑛 )
8	7	mpteq2ia	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ℝfld ) 1 ) ) = ( 𝑛 ∈ ℤ ↦ 𝑛 )
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	⊢ ( .g ‘ ℝfld ) = ( .g ‘ ℝfld )
14		re1r	⊢ 1 = ( 1r ‘ ℝfld )
15	12 13 14	zrhval2	⊢ ( ℝfld ∈ Ring → ( ℤRHom ‘ ℝfld ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ℝfld ) 1 ) ) )
16	10 11 15	mp2b	⊢ ( ℤRHom ‘ ℝfld ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ℝfld ) 1 ) )
17		mptresid	⊢ ( I ↾ ℤ ) = ( 𝑛 ∈ ℤ ↦ 𝑛 )
18	8 16 17	3eqtr4i	⊢ ( ℤRHom ‘ ℝfld ) = ( I ↾ ℤ )