Metamath Proof Explorer
Description: Value of the norm function in a normed complex vector space.
(Contributed by NM, 25-Apr-2007) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypothesis |
nmfval.6 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
|
Assertion |
nmcvfval |
⊢ 𝑁 = ( 2nd ‘ 𝑈 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nmfval.6 |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
2 |
|
df-nmcv |
⊢ normCV = 2nd |
3 |
2
|
fveq1i |
⊢ ( normCV ‘ 𝑈 ) = ( 2nd ‘ 𝑈 ) |
4 |
1 3
|
eqtri |
⊢ 𝑁 = ( 2nd ‘ 𝑈 ) |