Theorem hi02

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

	Ref	Expression
Assertion	hi02	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ·ih 0ℎ ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	⊢ 0ℎ ∈ ℋ
2		ax-his1	⊢ ( ( 𝐴 ∈ ℋ ∧ 0ℎ ∈ ℋ ) → ( 𝐴 ·ih 0ℎ ) = ( ∗ ‘ ( 0ℎ ·ih 𝐴 ) ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ·ih 0ℎ ) = ( ∗ ‘ ( 0ℎ ·ih 𝐴 ) ) )
4		hi01	⊢ ( 𝐴 ∈ ℋ → ( 0ℎ ·ih 𝐴 ) = 0 )
5	4	fveq2d	⊢ ( 𝐴 ∈ ℋ → ( ∗ ‘ ( 0ℎ ·ih 𝐴 ) ) = ( ∗ ‘ 0 ) )
6		cj0	⊢ ( ∗ ‘ 0 ) = 0
7	5 6	eqtrdi	⊢ ( 𝐴 ∈ ℋ → ( ∗ ‘ ( 0ℎ ·ih 𝐴 ) ) = 0 )
8	3 7	eqtrd	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ·ih 0ℎ ) = 0 )