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 ) |