# 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}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
Assertion hh0v ${⊢}{0}_{ℎ}={0}_{\mathrm{vec}}\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 hhnv.1 ${⊢}{U}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
2 1 hhnv ${⊢}{U}\in \mathrm{NrmCVec}$
3 eqid ${⊢}{+}_{v}\left({U}\right)={+}_{v}\left({U}\right)$
4 eqid ${⊢}{0}_{\mathrm{vec}}\left({U}\right)={0}_{\mathrm{vec}}\left({U}\right)$
5 3 4 0vfval ${⊢}{U}\in \mathrm{NrmCVec}\to {0}_{\mathrm{vec}}\left({U}\right)=\mathrm{GId}\left({+}_{v}\left({U}\right)\right)$
6 2 5 ax-mp ${⊢}{0}_{\mathrm{vec}}\left({U}\right)=\mathrm{GId}\left({+}_{v}\left({U}\right)\right)$
7 1 hhva ${⊢}{+}_{ℎ}={+}_{v}\left({U}\right)$
8 7 fveq2i ${⊢}\mathrm{GId}\left({+}_{ℎ}\right)=\mathrm{GId}\left({+}_{v}\left({U}\right)\right)$
9 hilid ${⊢}\mathrm{GId}\left({+}_{ℎ}\right)={0}_{ℎ}$
10 6 8 9 3eqtr2ri ${⊢}{0}_{ℎ}={0}_{\mathrm{vec}}\left({U}\right)$