Metamath Proof Explorer

Theorem norm0

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

Ref Expression
Assertion norm0 
|- ( normh ` 0h ) = 0

Proof

Step Hyp Ref Expression
1 ax-hv0cl 
 |-  0h e. ~H
2 normval 
 |-  ( 0h e. ~H -> ( normh ` 0h ) = ( sqrt ` ( 0h .ih 0h ) ) )
3 1 2 ax-mp 
 |-  ( normh ` 0h ) = ( sqrt ` ( 0h .ih 0h ) )
4 hi01 
 |-  ( 0h e. ~H -> ( 0h .ih 0h ) = 0 )
5 4 fveq2d 
 |-  ( 0h e. ~H -> ( sqrt ` ( 0h .ih 0h ) ) = ( sqrt ` 0 ) )
6 1 5 ax-mp 
 |-  ( sqrt ` ( 0h .ih 0h ) ) = ( sqrt ` 0 )
7 sqrt0 
 |-  ( sqrt ` 0 ) = 0
8 3 6 7 3eqtri 
 |-  ( normh ` 0h ) = 0