Theorem hi01

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

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

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	⊢ 0ℎ ∈ ℋ
2		ax-hvmul0	⊢ ( 0ℎ ∈ ℋ → ( 0 ·ℎ 0ℎ ) = 0ℎ )
3	1 2	ax-mp	⊢ ( 0 ·ℎ 0ℎ ) = 0ℎ
4	3	oveq1i	⊢ ( ( 0 ·ℎ 0ℎ ) ·ih 𝐴 ) = ( 0ℎ ·ih 𝐴 )
5		0cn	⊢ 0 ∈ ℂ
6		ax-his3	⊢ ( ( 0 ∈ ℂ ∧ 0ℎ ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 0 ·ℎ 0ℎ ) ·ih 𝐴 ) = ( 0 · ( 0ℎ ·ih 𝐴 ) ) )
7	5 1 6	mp3an12	⊢ ( 𝐴 ∈ ℋ → ( ( 0 ·ℎ 0ℎ ) ·ih 𝐴 ) = ( 0 · ( 0ℎ ·ih 𝐴 ) ) )
8	4 7	eqtr3id	⊢ ( 𝐴 ∈ ℋ → ( 0ℎ ·ih 𝐴 ) = ( 0 · ( 0ℎ ·ih 𝐴 ) ) )
9		hicl	⊢ ( ( 0ℎ ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 0ℎ ·ih 𝐴 ) ∈ ℂ )
10	1 9	mpan	⊢ ( 𝐴 ∈ ℋ → ( 0ℎ ·ih 𝐴 ) ∈ ℂ )
11	10	mul02d	⊢ ( 𝐴 ∈ ℋ → ( 0 · ( 0ℎ ·ih 𝐴 ) ) = 0 )
12	8 11	eqtrd	⊢ ( 𝐴 ∈ ℋ → ( 0ℎ ·ih 𝐴 ) = 0 )