Theorem his6

Description: Zero inner product with self means vector is zero. Lemma 3.1(S6) of Beran p. 95. (Contributed by NM, 27-Jul-1999) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-his4	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to 0<A{\cdot }_{\mathrm{ih}}A$$
2	1	gt0ne0d	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to A{\cdot }_{\mathrm{ih}}A\ne 0$$
3	2	ex	$$⊢A\in \mathscr{H}\to \left(A\ne 0_{ℎ}\to A{\cdot }_{\mathrm{ih}}A\ne 0\right)$$
4	3	necon4d	$$⊢A\in \mathscr{H}\to \left(A{\cdot }_{\mathrm{ih}}A=0\to A=0_{ℎ}\right)$$
5		hi01	$$⊢A\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}A=0$$
6		oveq1	$$⊢A=0_{ℎ}\to A{\cdot }_{\mathrm{ih}}A=0_{ℎ}{\cdot }_{\mathrm{ih}}A$$
7	6	eqeq1d	$$⊢A=0_{ℎ}\to \left(A{\cdot }_{\mathrm{ih}}A=0\leftrightarrow 0_{ℎ}{\cdot }_{\mathrm{ih}}A=0\right)$$
8	5 7	syl5ibrcom	$$⊢A\in \mathscr{H}\to \left(A=0_{ℎ}\to A{\cdot }_{\mathrm{ih}}A=0\right)$$
9	4 8	impbid	$$⊢A\in \mathscr{H}\to \left(A{\cdot }_{\mathrm{ih}}A=0\leftrightarrow A=0_{ℎ}\right)$$