This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmcvfval

Description: Value of the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	nmfval.6	$⊢ N = {norm}_{CV} (U)$
	Assertion	nmcvfval	$⊢ N = 2^{nd} (U)$

Step	Hyp	Ref	Expression
1		nmfval.6	$⊢ N = {norm}_{CV} (U)$
2		df-nmcv	$⊢ {norm}_{CV} = 2^{nd}$
3	2	fveq1i	$⊢ {norm}_{CV} (U) = 2^{nd} (U)$
4	1 3	eqtri	$⊢ N = 2^{nd} (U)$