Theorem cnrrext

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

	Ref	Expression
Assertion	cnrrext	⊢ ℂfld ∈ ℝExt

Proof

Step	Hyp	Ref	Expression
1		cnnrg	⊢ ℂfld ∈ NrmRing
2		cndrng	⊢ ℂfld ∈ DivRing
3	1 2	pm3.2i	⊢ ( ℂfld ∈ NrmRing ∧ ℂfld ∈ DivRing )
4		cnzh	⊢ ( ℤMod ‘ ℂfld ) ∈ NrmMod
5		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
6	5	fveq2i	⊢ ( chr ‘ ℝfld ) = ( chr ‘ ( ℂfld ↾s ℝ ) )
7		reofld	⊢ ℝfld ∈ oField
8		ofldchr	⊢ ( ℝfld ∈ oField → ( chr ‘ ℝfld ) = 0 )
9	7 8	ax-mp	⊢ ( chr ‘ ℝfld ) = 0
10		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
11	10	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
12		subrgchr	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ( chr ‘ ( ℂfld ↾s ℝ ) ) = ( chr ‘ ℂfld ) )
13	11 12	ax-mp	⊢ ( chr ‘ ( ℂfld ↾s ℝ ) ) = ( chr ‘ ℂfld )
14	6 9 13	3eqtr3ri	⊢ ( chr ‘ ℂfld ) = 0
15	4 14	pm3.2i	⊢ ( ( ℤMod ‘ ℂfld ) ∈ NrmMod ∧ ( chr ‘ ℂfld ) = 0 )
16		cnfldcusp	⊢ ℂfld ∈ CUnifSp
17		eqid	⊢ ( UnifSt ‘ ℂfld ) = ( UnifSt ‘ ℂfld )
18	17	cnflduss	⊢ ( UnifSt ‘ ℂfld ) = ( metUnif ‘ ( abs ∘ − ) )
19	16 18	pm3.2i	⊢ ( ℂfld ∈ CUnifSp ∧ ( UnifSt ‘ ℂfld ) = ( metUnif ‘ ( abs ∘ − ) ) )
20		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
21		cnmet	⊢ ( abs ∘ − ) ∈ ( Met ‘ ℂ )
22		metf	⊢ ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
23		ffn	⊢ ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ → ( abs ∘ − ) Fn ( ℂ × ℂ ) )
24	21 22 23	mp2b	⊢ ( abs ∘ − ) Fn ( ℂ × ℂ )
25		fnresdm	⊢ ( ( abs ∘ − ) Fn ( ℂ × ℂ ) → ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − ) )
26	24 25	ax-mp	⊢ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − )
27		cnfldds	⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
28	27	reseq1i	⊢ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
29	26 28	eqtr3i	⊢ ( abs ∘ − ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
30		eqid	⊢ ( ℤMod ‘ ℂfld ) = ( ℤMod ‘ ℂfld )
31	20 29 30	isrrext	⊢ ( ℂfld ∈ ℝExt ↔ ( ( ℂfld ∈ NrmRing ∧ ℂfld ∈ DivRing ) ∧ ( ( ℤMod ‘ ℂfld ) ∈ NrmMod ∧ ( chr ‘ ℂfld ) = 0 ) ∧ ( ℂfld ∈ CUnifSp ∧ ( UnifSt ‘ ℂfld ) = ( metUnif ‘ ( abs ∘ − ) ) ) ) )
32	3 15 19 31	mpbir3an	⊢ ℂfld ∈ ℝExt