Metamath Proof Explorer

Theorem hi01

Description: Inner product with the 0 vector. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hi01 
|- ( A e. ~H -> ( 0h .ih A ) = 0 )

Proof

Step Hyp Ref Expression
1 ax-hv0cl 
 |-  0h e. ~H
2 ax-hvmul0 
 |-  ( 0h e. ~H -> ( 0 .h 0h ) = 0h )
3 1 2 ax-mp 
 |-  ( 0 .h 0h ) = 0h
4 3 oveq1i 
 |-  ( ( 0 .h 0h ) .ih A ) = ( 0h .ih A )
5 0cn 
 |-  0 e. CC
6 ax-his3 
 |-  ( ( 0 e. CC /\ 0h e. ~H /\ A e. ~H ) -> ( ( 0 .h 0h ) .ih A ) = ( 0 x. ( 0h .ih A ) ) )
7 5 1 6 mp3an12 
 |-  ( A e. ~H -> ( ( 0 .h 0h ) .ih A ) = ( 0 x. ( 0h .ih A ) ) )
8 4 7 eqtr3id 
 |-  ( A e. ~H -> ( 0h .ih A ) = ( 0 x. ( 0h .ih A ) ) )
9 hicl 
 |-  ( ( 0h e. ~H /\ A e. ~H ) -> ( 0h .ih A ) e. CC )
10 1 9 mpan 
 |-  ( A e. ~H -> ( 0h .ih A ) e. CC )
11 10 mul02d 
 |-  ( A e. ~H -> ( 0 x. ( 0h .ih A ) ) = 0 )
12 8 11 eqtrd 
 |-  ( A e. ~H -> ( 0h .ih A ) = 0 )