Theorem cnindmet

Description: The metric induced on the complex numbers. cnmet proves that it is a metric. The induced metric is identical with the original metric on the complex numbers, see cnfldds and also cnmet . (Contributed by Steve Rodriguez, 5-Dec-2006) (Revised by AV, 17-Oct-2021)

	Ref	Expression
Hypothesis	cnindmet.t	$$⊢T={ℂ}_{\mathrm{fld}}\mathrm{toNrmGrp}\mathrm{abs}$$
Assertion	cnindmet	$$⊢\mathrm{dist}\left(T\right)=\mathrm{abs}\circ -$$

Proof

Step	Hyp	Ref	Expression
1		cnindmet.t	$$⊢T={ℂ}_{\mathrm{fld}}\mathrm{toNrmGrp}\mathrm{abs}$$
2		absabv	$$⊢\mathrm{abs}\in \mathrm{AbsVal}\left({ℂ}_{\mathrm{fld}}\right)$$
3		cnfldsub	$$⊢-={-}_{{ℂ}_{\mathrm{fld}}}$$
4	1 3	tngds	$$⊢\mathrm{abs}\in \mathrm{AbsVal}\left({ℂ}_{\mathrm{fld}}\right)\to \mathrm{abs}\circ -=\mathrm{dist}\left(T\right)$$
5	2 4	ax-mp	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left(T\right)$$
6	5	eqcomi	$$⊢\mathrm{dist}\left(T\right)=\mathrm{abs}\circ -$$