Theorem cnims

Description: The metric induced on the complex numbers. cnmet proves that it is a metric. (Contributed by Steve Rodriguez, 5-Dec-2006) (Revised by NM, 15-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cnims.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
	cnims.7	$$⊢D=\mathrm{abs}\circ -$$
Assertion	cnims	$$⊢D=\mathrm{IndMet}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnims.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
2		cnims.7	$$⊢D=\mathrm{abs}\circ -$$
3	1	cnnv	$$⊢U\in \mathrm{NrmCVec}$$
4	1	cnnvm	$$⊢-={-}_v\left(U\right)$$
5	1	cnnvnm	$$⊢\mathrm{abs}={norm}_{CV}\left(U\right)$$
6		eqid	$$⊢\mathrm{IndMet}\left(U\right)=\mathrm{IndMet}\left(U\right)$$
7	4 5 6	imsval	$$⊢U\in \mathrm{NrmCVec}\to \mathrm{IndMet}\left(U\right)=\mathrm{abs}\circ -$$
8	3 7	ax-mp	$$⊢\mathrm{IndMet}\left(U\right)=\mathrm{abs}\circ -$$
9	2 8	eqtr4i	$$⊢D=\mathrm{IndMet}\left(U\right)$$