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