Metamath Proof Explorer


Theorem hhnm

Description: The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypothesis hhnv.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
Assertion hhnm normโ„Ž = ( normCV โ€˜ ๐‘ˆ )

Proof

Step Hyp Ref Expression
1 hhnv.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 1 hhnv โŠข ๐‘ˆ โˆˆ NrmCVec
3 1 2 h2hnm โŠข normโ„Ž = ( normCV โ€˜ ๐‘ˆ )