Theorem cnnm

Description: The norm of the normed subcomplex vector space of complex numbers is the absolute value. (Contributed by NM, 12-Jan-2008) (Revised by AV, 9-Oct-2021)

	Ref	Expression
Hypothesis	cnrnvc.c	$$⊢C=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cnnm	$$⊢\mathrm{norm}\left(C\right)=\mathrm{abs}$$

Proof

Step	Hyp	Ref	Expression
1		cnrnvc.c	$$⊢C=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
2		rlmnm	$$⊢\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{norm}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
3		cnfldnm	$$⊢\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$
4	1	fveq2i	$$⊢\mathrm{norm}\left(C\right)=\mathrm{norm}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
5	2 3 4	3eqtr4ri	$$⊢\mathrm{norm}\left(C\right)=\mathrm{abs}$$