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 31216

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 31209	. . 3 ⊢ norm_CV = 2^nd
3	2	fveq1i 6889	. 2 ⊢ (norm_CV‘𝑈) = (2^nd ‘𝑈)
4	1, 3	eqtri 2783	1 ⊢ 𝑁 = (2^nd ‘𝑈)

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1569 ‘cfv 6541 2^nd c2nd 8002 norm_CVcnmcv 31199

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732

This proof depends on definitions: df-bi 210 df-an 402 df-tru 1572 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-v 3452 df-ss 3897 df-uni 4867 df-br 5103 df-iota 6496 df-fv 6549 df-nmcv 31209

This theorem is used by: nvop2 31217 nvop 31285 cnnvnm 31290 phop 31427 h2hnm 31585 hhssnm 31868