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 )