Theorem hial02

Description: A vector whose inner product is always zero is zero. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hial02	$$⊢A\in \mathscr{H}\to \left(\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}A=0\leftrightarrow A=0_{ℎ}\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=A\to x{\cdot }_{\mathrm{ih}}A=A{\cdot }_{\mathrm{ih}}A$$
2	1	eqeq1d	$$⊢x=A\to \left(x{\cdot }_{\mathrm{ih}}A=0\leftrightarrow A{\cdot }_{\mathrm{ih}}A=0\right)$$
3	2	rspcv	$$⊢A\in \mathscr{H}\to \left(\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}A=0\to A{\cdot }_{\mathrm{ih}}A=0\right)$$
4		his6	$$⊢A\in \mathscr{H}\to \left(A{\cdot }_{\mathrm{ih}}A=0\leftrightarrow A=0_{ℎ}\right)$$
5	3 4	sylibd	$$⊢A\in \mathscr{H}\to \left(\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}A=0\to A=0_{ℎ}\right)$$
6		oveq2	$$⊢A=0_{ℎ}\to x{\cdot }_{\mathrm{ih}}A=x{\cdot }_{\mathrm{ih}}{0}_{ℎ}$$
7		hi02	$$⊢x\in \mathscr{H}\to x{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0$$
8	6 7	sylan9eq	$$⊢\left(A=0_{ℎ}\wedge x\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}A=0$$
9	8	ex	$$⊢A=0_{ℎ}\to \left(x\in \mathscr{H}\to x{\cdot }_{\mathrm{ih}}A=0\right)$$
10	9	a1i	$$⊢A\in \mathscr{H}\to \left(A=0_{ℎ}\to \left(x\in \mathscr{H}\to x{\cdot }_{\mathrm{ih}}A=0\right)\right)$$
11	10	ralrimdv	$$⊢A\in \mathscr{H}\to \left(A=0_{ℎ}\to \forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}A=0\right)$$
12	5 11	impbid	$$⊢A\in \mathscr{H}\to \left(\forall x\in \mathscr{H}x{\cdot }_{\mathrm{ih}}A=0\leftrightarrow A=0_{ℎ}\right)$$