hi02

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

		Ref	Expression
	Assertion	hi02	$⊢ A \in ℋ \to A \cdot_{ih} 0_{ℎ} = 0$

Step	Hyp	Ref	Expression
1		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
2		ax-his1	$⊢ (A \in ℋ \land 0_{ℎ} \in ℋ) \to A \cdot_{ih} 0_{ℎ} = \overline{0_{ℎ} \cdot_{ih} A}$
3	1 2	mpan2	$⊢ A \in ℋ \to A \cdot_{ih} 0_{ℎ} = \overline{0_{ℎ} \cdot_{ih} A}$
4		hi01	$⊢ A \in ℋ \to 0_{ℎ} \cdot_{ih} A = 0$
5	4	fveq2d	$⊢ A \in ℋ \to \overline{0_{ℎ} \cdot_{ih} A} = \overline{0}$
6		cj0	$⊢ \overline{0} = 0$
7	5 6	syl6eq	$⊢ A \in ℋ \to \overline{0_{ℎ} \cdot_{ih} A} = 0$
8	3 7	eqtrd	$⊢ A \in ℋ \to A \cdot_{ih} 0_{ℎ} = 0$

Metamath Proof Explorer