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 | |- U = <. <. +h , .h >. , normh >. |
|
Assertion | hh0v | |- 0h = ( 0vec ` U ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hhnv.1 | |- U = <. <. +h , .h >. , normh >. |
|
2 | 1 | hhnv | |- U e. NrmCVec |
3 | eqid | |- ( +v ` U ) = ( +v ` U ) |
|
4 | eqid | |- ( 0vec ` U ) = ( 0vec ` U ) |
|
5 | 3 4 | 0vfval | |- ( U e. NrmCVec -> ( 0vec ` U ) = ( GId ` ( +v ` U ) ) ) |
6 | 2 5 | ax-mp | |- ( 0vec ` U ) = ( GId ` ( +v ` U ) ) |
7 | 1 | hhva | |- +h = ( +v ` U ) |
8 | 7 | fveq2i | |- ( GId ` +h ) = ( GId ` ( +v ` U ) ) |
9 | hilid | |- ( GId ` +h ) = 0h |
|
10 | 6 8 9 | 3eqtr2ri | |- 0h = ( 0vec ` U ) |