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 31088

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 31081	. . 3 ⊢ norm_CV = 2^nd
3	2	fveq1i 6879	. 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 1570 ‘cfv 6533 2^nd c2nd 7985 norm_CVcnmcv 31071

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2732

This proof depends on definitions: df-bi 210 df-an 402 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2739 df-cleq 2752 df-clel 2835 df-v 3452 df-ss 3916 df-uni 4868 df-br 5104 df-iota 6489 df-fv 6541 df-nmcv 31081

This theorem is used by: nvop2 31089 nvop 31157 cnnvnm 31162 phop 31299 h2hnm 31457 hhssnm 31740