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	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
Assertion	hh0v	⊢ 0ℎ = ( 0vec ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2	1	hhnv	⊢ 𝑈 ∈ NrmCVec
3		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
4		eqid	⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
5	3 4	0vfval	⊢ ( 𝑈 ∈ NrmCVec → ( 0vec ‘ 𝑈 ) = ( GId ‘ ( +𝑣 ‘ 𝑈 ) ) )
6	2 5	ax-mp	⊢ ( 0vec ‘ 𝑈 ) = ( GId ‘ ( +𝑣 ‘ 𝑈 ) )
7	1	hhva	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
8	7	fveq2i	⊢ ( GId ‘ +ℎ ) = ( GId ‘ ( +𝑣 ‘ 𝑈 ) )
9		hilid	⊢ ( GId ‘ +ℎ ) = 0ℎ
10	6 8 9	3eqtr2ri	⊢ 0ℎ = ( 0vec ‘ 𝑈 )