hvmul0

Description: Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

		Ref	Expression
	Assertion	hvmul0	$⊢ A \in ℂ \to A \cdot_{ℎ} 0_{ℎ} = 0_{ℎ}$

Step	Hyp	Ref	Expression
1		mul01	$⊢ A \in ℂ \to A \cdot 0 = 0$
2	1	oveq1d	$⊢ A \in ℂ \to A \cdot 0 \cdot_{ℎ} 0_{ℎ} = 0 \cdot_{ℎ} 0_{ℎ}$
3		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
4		ax-hvmul0	$⊢ 0_{ℎ} \in ℋ \to 0 \cdot_{ℎ} 0_{ℎ} = 0_{ℎ}$
5	3 4	ax-mp	$⊢ 0 \cdot_{ℎ} 0_{ℎ} = 0_{ℎ}$
6	2 5	eqtrdi	$⊢ A \in ℂ \to A \cdot 0 \cdot_{ℎ} 0_{ℎ} = 0_{ℎ}$
7		0cn	$⊢ 0 \in ℂ$
8		ax-hvmulass	$⊢ (A \in ℂ \land 0 \in ℂ \land 0_{ℎ} \in ℋ) \to A \cdot 0 \cdot_{ℎ} 0_{ℎ} = A \cdot_{ℎ} (0 \cdot_{ℎ} 0_{ℎ})$
9	7 3 8	mp3an23	$⊢ A \in ℂ \to A \cdot 0 \cdot_{ℎ} 0_{ℎ} = A \cdot_{ℎ} (0 \cdot_{ℎ} 0_{ℎ})$
10	6 9	eqtr3d	$⊢ A \in ℂ \to 0_{ℎ} = A \cdot_{ℎ} (0 \cdot_{ℎ} 0_{ℎ})$
11	5	oveq2i	$⊢ A \cdot_{ℎ} (0 \cdot_{ℎ} 0_{ℎ}) = A \cdot_{ℎ} 0_{ℎ}$
12	10 11	eqtr2di	$⊢ A \in ℂ \to A \cdot_{ℎ} 0_{ℎ} = 0_{ℎ}$

Metamath Proof Explorer