Theorem cnfldnm

Description: The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	cnfldnm	$$⊢\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		eqid	$$⊢\mathrm{abs}\circ -=\mathrm{abs}\circ -$$
3	2	cnmetdval	$$⊢\left(x\in ℂ\wedge 0\in ℂ\right)\to x\left(\mathrm{abs}\circ -\right)0=\left|x-0\right|$$
4	1 3	mpan2	$$⊢x\in ℂ\to x\left(\mathrm{abs}\circ -\right)0=\left|x-0\right|$$
5		subid1	$$⊢x\in ℂ\to x-0=x$$
6	5	fveq2d	$$⊢x\in ℂ\to \left|x-0\right|=\left|x\right|$$
7	4 6	eqtrd	$$⊢x\in ℂ\to x\left(\mathrm{abs}\circ -\right)0=\left|x\right|$$
8	7	mpteq2ia	$$⊢\left(x\in ℂ⟼x\left(\mathrm{abs}\circ -\right)0\right)=\left(x\in ℂ⟼\left|x\right|\right)$$
9		eqid	$$⊢\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$
10		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
11		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
12		cnfldds	$$⊢\mathrm{abs}\circ -=\mathrm{dist}\left({ℂ}_{\mathrm{fld}}\right)$$
13	9 10 11 12	nmfval	$$⊢\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)=\left(x\in ℂ⟼x\left(\mathrm{abs}\circ -\right)0\right)$$
14		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
15	14	a1i	$$⊢\top \to \mathrm{abs}:ℂ⟶ℝ$$
16	15	feqmptd	$$⊢\top \to \mathrm{abs}=\left(x\in ℂ⟼\left|x\right|\right)$$
17	16	mptru	$$⊢\mathrm{abs}=\left(x\in ℂ⟼\left|x\right|\right)$$
18	8 13 17	3eqtr4ri	$$⊢\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$