Theorem norm0

Description: The norm of a zero vector. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	norm0	⊢ ( normℎ ‘ 0ℎ ) = 0

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	⊢ 0ℎ ∈ ℋ
2		normval	⊢ ( 0ℎ ∈ ℋ → ( normℎ ‘ 0ℎ ) = ( √ ‘ ( 0ℎ ·ih 0ℎ ) ) )
3	1 2	ax-mp	⊢ ( normℎ ‘ 0ℎ ) = ( √ ‘ ( 0ℎ ·ih 0ℎ ) )
4		hi01	⊢ ( 0ℎ ∈ ℋ → ( 0ℎ ·ih 0ℎ ) = 0 )
5	4	fveq2d	⊢ ( 0ℎ ∈ ℋ → ( √ ‘ ( 0ℎ ·ih 0ℎ ) ) = ( √ ‘ 0 ) )
6	1 5	ax-mp	⊢ ( √ ‘ ( 0ℎ ·ih 0ℎ ) ) = ( √ ‘ 0 )
7		sqrt0	⊢ ( √ ‘ 0 ) = 0
8	3 6 7	3eqtri	⊢ ( normℎ ‘ 0ℎ ) = 0