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 31202

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1570 ‘cfv 6537 2^nd c2nd 7998 norm_CVcnmcv 31185

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 2733

This proof depends on definitions: df-bi 210 df-an 402 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2740 df-cleq 2753 df-clel 2836 df-v 3453 df-ss 3916 df-uni 4868 df-br 5104 df-iota 6493 df-fv 6545 df-nmcv 31195

This theorem is used by: nvop2 31203 nvop 31271 cnnvnm 31276 phop 31413 h2hnm 31571 hhssnm 31854