Metamath Proof Explorer

Theorem hvmul0

Description: Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

Ref Expression
Assertion hvmul0 
|- ( A e. CC -> ( A .h 0h ) = 0h )

Proof

Step Hyp Ref Expression
1 mul01 
 |-  ( A e. CC -> ( A x. 0 ) = 0 )
2 1 oveq1d 
 |-  ( A e. CC -> ( ( A x. 0 ) .h 0h ) = ( 0 .h 0h ) )
3 ax-hv0cl 
 |-  0h e. ~H
4 ax-hvmul0 
 |-  ( 0h e. ~H -> ( 0 .h 0h ) = 0h )
5 3 4 ax-mp 
 |-  ( 0 .h 0h ) = 0h
6 2 5 syl6eq 
 |-  ( A e. CC -> ( ( A x. 0 ) .h 0h ) = 0h )
7 0cn 
 |-  0 e. CC
8 ax-hvmulass 
 |-  ( ( A e. CC /\ 0 e. CC /\ 0h e. ~H ) -> ( ( A x. 0 ) .h 0h ) = ( A .h ( 0 .h 0h ) ) )
9 7 3 8 mp3an23 
 |-  ( A e. CC -> ( ( A x. 0 ) .h 0h ) = ( A .h ( 0 .h 0h ) ) )
10 6 9 eqtr3d 
 |-  ( A e. CC -> 0h = ( A .h ( 0 .h 0h ) ) )
11 5 oveq2i 
 |-  ( A .h ( 0 .h 0h ) ) = ( A .h 0h )
12 10 11 eqtr2di 
 |-  ( A e. CC -> ( A .h 0h ) = 0h )