Theorem 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_{ℎ}$$

Proof

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 \mathscr{H}$$
4		ax-hvmul0	$$⊢0_{ℎ}\in \mathscr{H}\to 0{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
5	3 4	ax-mp	$$⊢0{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
6	2 5	syl6eq	$$⊢A\in ℂ\to A\cdot 0{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
7		0cn	$$⊢0\in ℂ$$
8		ax-hvmulass	$$⊢\left(A\in ℂ\wedge 0\in ℂ\wedge 0_{ℎ}\in \mathscr{H}\right)\to A\cdot 0{\cdot }_{ℎ}{0}_{ℎ}=A{\cdot }_{ℎ}\left(0{\cdot }_{ℎ}{0}_{ℎ}\right)$$
9	7 3 8	mp3an23	$$⊢A\in ℂ\to A\cdot 0{\cdot }_{ℎ}{0}_{ℎ}=A{\cdot }_{ℎ}\left(0{\cdot }_{ℎ}{0}_{ℎ}\right)$$
10	6 9	eqtr3d	$$⊢A\in ℂ\to 0_{ℎ}=A{\cdot }_{ℎ}\left(0{\cdot }_{ℎ}{0}_{ℎ}\right)$$
11	5	oveq2i	$$⊢A{\cdot }_{ℎ}\left(0{\cdot }_{ℎ}{0}_{ℎ}\right)=A{\cdot }_{ℎ}{0}_{ℎ}$$
12	10 11	syl6req	$$⊢A\in ℂ\to A{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$