Theorem hi01

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

	Ref	Expression
Assertion	hi01	$$⊢A\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}A=0$$

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
2		ax-hvmul0	$$⊢0_{ℎ}\in \mathscr{H}\to 0{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
3	1 2	ax-mp	$$⊢0{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
4	3	oveq1i	$$⊢\left(0{\cdot }_{ℎ}{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}A=0_{ℎ}{\cdot }_{\mathrm{ih}}A$$
5		0cn	$$⊢0\in ℂ$$
6		ax-his3	$$⊢\left(0\in ℂ\wedge 0_{ℎ}\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to \left(0{\cdot }_{ℎ}{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}A=0\cdot \left(0_{ℎ}{\cdot }_{\mathrm{ih}}A\right)$$
7	5 1 6	mp3an12	$$⊢A\in \mathscr{H}\to \left(0{\cdot }_{ℎ}{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}A=0\cdot \left(0_{ℎ}{\cdot }_{\mathrm{ih}}A\right)$$
8	4 7	eqtr3id	$$⊢A\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}A=0\cdot \left(0_{ℎ}{\cdot }_{\mathrm{ih}}A\right)$$
9		hicl	$$⊢\left(0_{ℎ}\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to 0_{ℎ}{\cdot }_{\mathrm{ih}}A\in ℂ$$
10	1 9	mpan	$$⊢A\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}A\in ℂ$$
11	10	mul02d	$$⊢A\in \mathscr{H}\to 0\cdot \left(0_{ℎ}{\cdot }_{\mathrm{ih}}A\right)=0$$
12	8 11	eqtrd	$$⊢A\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}A=0$$