# Metamath Proof Explorer

## 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)$