Theorem cnfldms

Description: The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Assertion	cnfldms	⊢ ℂfld ∈ MetSp

Proof

Step	Hyp	Ref	Expression
1		cnmet	⊢ ( abs ∘ − ) ∈ ( Met ‘ ℂ )
2		eqid	⊢ ( MetOpen ‘ ( abs ∘ − ) ) = ( MetOpen ‘ ( abs ∘ − ) )
3		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
4	2	mopntopon	⊢ ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → ( MetOpen ‘ ( abs ∘ − ) ) ∈ ( TopOn ‘ ℂ ) )
5		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
6		cnfldtset	⊢ ( MetOpen ‘ ( abs ∘ − ) ) = ( TopSet ‘ ℂfld )
7	5 6	topontopn	⊢ ( ( MetOpen ‘ ( abs ∘ − ) ) ∈ ( TopOn ‘ ℂ ) → ( MetOpen ‘ ( abs ∘ − ) ) = ( TopOpen ‘ ℂfld ) )
8	3 4 7	mp2b	⊢ ( MetOpen ‘ ( abs ∘ − ) ) = ( TopOpen ‘ ℂfld )
9		absf	⊢ abs : ℂ ⟶ ℝ
10		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
11		fco	⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
12	9 10 11	mp2an	⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
13		ffn	⊢ ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ → ( abs ∘ − ) Fn ( ℂ × ℂ ) )
14		fnresdm	⊢ ( ( abs ∘ − ) Fn ( ℂ × ℂ ) → ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − ) )
15	12 13 14	mp2b	⊢ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − )
16		cnfldds	⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
17	16	reseq1i	⊢ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
18	15 17	eqtr3i	⊢ ( abs ∘ − ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
19	8 5 18	isms2	⊢ ( ℂfld ∈ MetSp ↔ ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) ∧ ( MetOpen ‘ ( abs ∘ − ) ) = ( MetOpen ‘ ( abs ∘ − ) ) ) )
20	1 2 19	mpbir2an	⊢ ℂfld ∈ MetSp