This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = + ℎ ⋅ ℎ norm ℎ
Assertion hh0v ⊢ 0 ℎ = 0 vec ⁡ U

Proof

Step Hyp Ref Expression
1 hhnv.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 1 hhnv ⊢ U ∈ NrmCVec
3 eqid ⊢ + v ⁡ U = + v ⁡ U
4 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
5 3 4 0vfval ⊢ U ∈ NrmCVec → 0 vec ⁡ U = GId ⁡ + v ⁡ U
6 2 5 ax-mp ⊢ 0 vec ⁡ U = GId ⁡ + v ⁡ U
7 1 hhva ⊢ + ℎ = + v ⁡ U
8 7 fveq2i ⊢ GId ⁡ + ℎ = GId ⁡ + v ⁡ U
9 hilid ⊢ GId ⁡ + ℎ = 0 ℎ
10 6 8 9 3eqtr2ri ⊢ 0 ℎ = 0 vec ⁡ U