Theorem rerrext

Description: The field of the real numbers is an extension of the real numbers. (Contributed by Thierry Arnoux, 2-May-2018)

	Ref	Expression
Assertion	rerrext	⊢ ℝfld ∈ ℝExt

Proof

Step	Hyp	Ref	Expression
1		cnnrg	⊢ ℂfld ∈ NrmRing
2		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
3	2	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
4		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
5	4	subrgnrg	⊢ ( ( ℂfld ∈ NrmRing ∧ ℝ ∈ ( SubRing ‘ ℂfld ) ) → ℝfld ∈ NrmRing )
6	1 3 5	mp2an	⊢ ℝfld ∈ NrmRing
7	2	simpri	⊢ ℝfld ∈ DivRing
8	6 7	pm3.2i	⊢ ( ℝfld ∈ NrmRing ∧ ℝfld ∈ DivRing )
9		rezh	⊢ ( ℤMod ‘ ℝfld ) ∈ NrmMod
10		reofld	⊢ ℝfld ∈ oField
11		ofldchr	⊢ ( ℝfld ∈ oField → ( chr ‘ ℝfld ) = 0 )
12	10 11	ax-mp	⊢ ( chr ‘ ℝfld ) = 0
13	9 12	pm3.2i	⊢ ( ( ℤMod ‘ ℝfld ) ∈ NrmMod ∧ ( chr ‘ ℝfld ) = 0 )
14		recusp	⊢ ℝfld ∈ CUnifSp
15		reust	⊢ ( UnifSt ‘ ℝfld ) = ( metUnif ‘ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) )
16	14 15	pm3.2i	⊢ ( ℝfld ∈ CUnifSp ∧ ( UnifSt ‘ ℝfld ) = ( metUnif ‘ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) ) )
17		rebase	⊢ ℝ = ( Base ‘ ℝfld )
18		eqid	⊢ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) = ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) )
19		eqid	⊢ ( ℤMod ‘ ℝfld ) = ( ℤMod ‘ ℝfld )
20	17 18 19	isrrext	⊢ ( ℝfld ∈ ℝExt ↔ ( ( ℝfld ∈ NrmRing ∧ ℝfld ∈ DivRing ) ∧ ( ( ℤMod ‘ ℝfld ) ∈ NrmMod ∧ ( chr ‘ ℝfld ) = 0 ) ∧ ( ℝfld ∈ CUnifSp ∧ ( UnifSt ‘ ℝfld ) = ( metUnif ‘ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) ) ) ) )
21	8 13 16 20	mpbir3an	⊢ ℝfld ∈ ℝExt