nmcvfval - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nmcvfval		Structured version Visualization version GIF version

Theorem nmcvfval 31266

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

**Hypothesis**
Ref	Expression
nmfval.6	⊢ 𝑁 = (norm_CV‘𝑈)

**Assertion**
Ref	Expression
nmcvfval	⊢ 𝑁 = (2^nd ‘𝑈)

**Proof of Theorem nmcvfval**
Step	Hyp	Ref	Expression
1		nmfval.6	. 2 ⊢ 𝑁 = (norm_CV‘𝑈)
2		df-nmcv 31259	. . 3 ⊢ norm_CV = 2^nd
3	2	fveq1i 6917	. 2 ⊢ (norm_CV‘𝑈) = (2^nd ‘𝑈)
4	1, 3	eqtri 2786	1 ⊢ 𝑁 = (2^nd ‘𝑈)

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1570 ‘cfv 6566 2^nd c2nd 8034 norm_CVcnmcv 31249

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-ext 2735

This proof depends on definitions: df-bi 210 df-an 402 df-tru 1573 df-ex 1813 df-sb 2102 df-clab 2742 df-cleq 2755 df-clel 2839 df-v 3456 df-ss 3901 df-uni 4873 df-br 5109 df-iota 6520 df-fv 6574 df-nmcv 31259

This theorem is used by: nvop2 31267 nvop 31335 cnnvnm 31340 phop 31477 h2hnm 31635 hhssnm 31918