Metamath Proof Explorer

Theorem hhnv

Description: Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypothesis hhnv.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
Assertion hhnv ๐‘ˆ โˆˆ NrmCVec

Proof

Step Hyp Ref Expression
1 hhnv.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 hilablo โŠข +โ„Ž โˆˆ AbelOp
3 ablogrpo โŠข ( +โ„Ž โˆˆ AbelOp โ†’ +โ„Ž โˆˆ GrpOp )
4 2 3 ax-mp โŠข +โ„Ž โˆˆ GrpOp
5 ax-hfvadd โŠข +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹
6 5 fdmi โŠข dom +โ„Ž = ( โ„‹ ร— โ„‹ )
7 4 6 grporn โŠข โ„‹ = ran +โ„Ž
8 hilid โŠข ( GId โ€˜ +โ„Ž ) = 0โ„Ž
9 8 eqcomi โŠข 0โ„Ž = ( GId โ€˜ +โ„Ž )
10 hilvc โŠข โŸจ +โ„Ž , ยทโ„Ž โŸฉ โˆˆ CVecOLD
11 normf โŠข normโ„Ž : โ„‹ โŸถ โ„
12 norm-i โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†’ ( ( normโ„Ž โ€˜ ๐‘ฅ ) = 0 โ†” ๐‘ฅ = 0โ„Ž ) )
13 12 biimpa โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ( normโ„Ž โ€˜ ๐‘ฅ ) = 0 ) โ†’ ๐‘ฅ = 0โ„Ž )
14 norm-iii โŠข ( ( ๐‘ฆ โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( normโ„Ž โ€˜ ( ๐‘ฆ ยทโ„Ž ๐‘ฅ ) ) = ( ( abs โ€˜ ๐‘ฆ ) ยท ( normโ„Ž โ€˜ ๐‘ฅ ) ) )
15 norm-ii โŠข ( ( ๐‘ฅ โˆˆ โ„‹ โˆง ๐‘ฆ โˆˆ โ„‹ ) โ†’ ( normโ„Ž โ€˜ ( ๐‘ฅ +โ„Ž ๐‘ฆ ) ) โ‰ค ( ( normโ„Ž โ€˜ ๐‘ฅ ) + ( normโ„Ž โ€˜ ๐‘ฆ ) ) )
16 7 9 10 11 13 14 15 1 isnvi โŠข ๐‘ˆ โˆˆ NrmCVec