Metamath Proof Explorer

Theorem hh0v

Description: The zero vector of Hilbert space. (Contributed by NM, 17-Nov-2007) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hhnv.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 1 hhnv โŠข ๐‘ˆ โˆˆ NrmCVec
3 eqid โŠข ( +๐‘ฃ โ€˜ ๐‘ˆ ) = ( +๐‘ฃ โ€˜ ๐‘ˆ )
4 eqid โŠข ( 0vec โ€˜ ๐‘ˆ ) = ( 0vec โ€˜ ๐‘ˆ )
5 3 4 0vfval โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( 0vec โ€˜ ๐‘ˆ ) = ( GId โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) ) )
6 2 5 ax-mp โŠข ( 0vec โ€˜ ๐‘ˆ ) = ( GId โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) )
7 1 hhva โŠข +โ„Ž = ( +๐‘ฃ โ€˜ ๐‘ˆ )
8 7 fveq2i โŠข ( GId โ€˜ +โ„Ž ) = ( GId โ€˜ ( +๐‘ฃ โ€˜ ๐‘ˆ ) )
9 hilid โŠข ( GId โ€˜ +โ„Ž ) = 0โ„Ž
10 6 8 9 3eqtr2ri โŠข 0โ„Ž = ( 0vec โ€˜ ๐‘ˆ )