Theorem hi02

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

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

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	|- 0h e. ~H
2		ax-his1	|- ( ( A e. ~H /\ 0h e. ~H ) -> ( A .ih 0h ) = ( * ` ( 0h .ih A ) ) )
3	1 2	mpan2	|- ( A e. ~H -> ( A .ih 0h ) = ( * ` ( 0h .ih A ) ) )
4		hi01	|- ( A e. ~H -> ( 0h .ih A ) = 0 )
5	4	fveq2d	|- ( A e. ~H -> ( * ` ( 0h .ih A ) ) = ( * ` 0 ) )
6		cj0	|- ( * ` 0 ) = 0
7	5 6	eqtrdi	|- ( A e. ~H -> ( * ` ( 0h .ih A ) ) = 0 )
8	3 7	eqtrd	|- ( A e. ~H -> ( A .ih 0h ) = 0 )