Theorem cncms

Description: The field of complex numbers is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Assertion	cncms	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CMetSp}$$

Proof

Step	Hyp	Ref	Expression
1		cnfldms	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}$$
2		eqid	$$⊢\mathrm{abs}\circ -=\mathrm{abs}\circ -$$
3	2	cncmet	$$⊢\mathrm{abs}\circ -\in \mathrm{CMet}\left(ℂ\right)$$
4		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
5		cnmet	$$⊢\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$$
6		metf	$$⊢\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)\to \left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ$$
7	5 6	ax-mp	$$⊢\left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ$$
8		ffn	$$⊢\left(\mathrm{abs}\circ -\right):ℂ\times ℂ⟶ℝ\to \left(\mathrm{abs}\circ -\right)Fn\left(ℂ\times ℂ\right)$$
9		fnresdm	$$⊢\left(\mathrm{abs}\circ -\right)Fn\left(ℂ\times ℂ\right)\to {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}=\mathrm{abs}\circ -$$
10	7 8 9	mp2b	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}=\mathrm{abs}\circ -$$
11		cnfldds	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$$
12	11	reseq1i	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}$$
13	10 12	eqtr3i	$$⊢\mathrm{abs}\circ -={\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)\upharpoonright }_{\left(ℂ\times ℂ\right)}$$
14	4 13	iscms	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CMetSp}\leftrightarrow \left({ℂ}_{\mathrm{fld}}\in \mathrm{MetSp}\wedge \mathrm{abs}\circ -\in \mathrm{CMet}\left(ℂ\right)\right)$$
15	1 3 14	mpbir2an	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CMetSp}$$