Theorem cnnvnm

Description: The norm operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cnnvnm.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
Assertion	cnnvnm	$$⊢\mathrm{abs}={norm}_{CV}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnnvnm.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
2		eqid	$$⊢{norm}_{CV}\left(U\right)={norm}_{CV}\left(U\right)$$
3	2	nmcvfval	$$⊢{norm}_{CV}\left(U\right)=2^{nd}\left(U\right)$$
4	1	fveq2i	$$⊢2^{nd}\left(U\right)=2^{nd}\left(⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)$$
5		opex	$$⊢⟨+,\times ⟩\in \mathrm{V}$$
6		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
7		cnex	$$⊢ℂ\in \mathrm{V}$$
8		fex	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℂ\in \mathrm{V}\right)\to \mathrm{abs}\in \mathrm{V}$$
9	6 7 8	mp2an	$$⊢\mathrm{abs}\in \mathrm{V}$$
10	5 9	op2nd	$$⊢2^{nd}\left(⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)=\mathrm{abs}$$
11	3 4 10	3eqtrri	$$⊢\mathrm{abs}={norm}_{CV}\left(U\right)$$