Theorem re1r

Description: The multiplicative neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017)

	Ref	Expression
Assertion	re1r	⊢ 1 = ( 1r ‘ ℝfld )

Proof

Step	Hyp	Ref	Expression
1		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
2	1	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
3		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
4		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
5	3 4	subrg1	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → 1 = ( 1r ‘ ℝfld ) )
6	2 5	ax-mp	⊢ 1 = ( 1r ‘ ℝfld )