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 31030

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1570 ‘cfv 6540 2^nd c2nd 7991 norm_CVcnmcv 31013

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 2148 ax-9 2156 ax-ext 2737

This proof depends on definitions: df-bi 210 df-an 402 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2744 df-cleq 2757 df-clel 2840 df-v 3459 df-ss 3923 df-uni 4875 df-br 5112 df-iota 6496 df-fv 6548 df-nmcv 31023

This theorem is used by: nvop2 31031 nvop 31099 cnnvnm 31104 phop 31241 h2hnm 31399 hhssnm 31682