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 eqtrdi
 |-  ( 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 )