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
|- U = <. <. +h , .h >. , normh >.
Assertion hh0v
|- 0h = ( 0vec ` U )

Proof

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 )