Theorem hiidge0

Description: Inner product with self is not negative. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	hiidge0	$$⊢A\in \mathscr{H}\to 0\le A{\cdot }_{\mathrm{ih}}A$$

Proof

Step	Hyp	Ref	Expression
1		pm2.1	$$⊢\left(\neg A=0_{ℎ}\vee A=0_{ℎ}\right)$$
2		df-ne	$$⊢A\ne 0_{ℎ}\leftrightarrow \neg A=0_{ℎ}$$
3		ax-his4	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to 0<A{\cdot }_{\mathrm{ih}}A$$
4	2 3	sylan2br	$$⊢\left(A\in \mathscr{H}\wedge \neg A=0_{ℎ}\right)\to 0<A{\cdot }_{\mathrm{ih}}A$$
5	4	ex	$$⊢A\in \mathscr{H}\to \left(\neg A=0_{ℎ}\to 0<A{\cdot }_{\mathrm{ih}}A\right)$$
6		oveq1	$$⊢A=0_{ℎ}\to A{\cdot }_{\mathrm{ih}}A=0_{ℎ}{\cdot }_{\mathrm{ih}}A$$
7		hi01	$$⊢A\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}A=0$$
8	6 7	sylan9eqr	$$⊢\left(A\in \mathscr{H}\wedge A=0_{ℎ}\right)\to A{\cdot }_{\mathrm{ih}}A=0$$
9	8	eqcomd	$$⊢\left(A\in \mathscr{H}\wedge A=0_{ℎ}\right)\to 0=A{\cdot }_{\mathrm{ih}}A$$
10	9	ex	$$⊢A\in \mathscr{H}\to \left(A=0_{ℎ}\to 0=A{\cdot }_{\mathrm{ih}}A\right)$$
11	5 10	orim12d	$$⊢A\in \mathscr{H}\to \left(\left(\neg A=0_{ℎ}\vee A=0_{ℎ}\right)\to \left(0<A{\cdot }_{\mathrm{ih}}A\vee 0=A{\cdot }_{\mathrm{ih}}A\right)\right)$$
12	1 11	mpi	$$⊢A\in \mathscr{H}\to \left(0<A{\cdot }_{\mathrm{ih}}A\vee 0=A{\cdot }_{\mathrm{ih}}A\right)$$
13		0re	$$⊢0\in ℝ$$
14		hiidrcl	$$⊢A\in \mathscr{H}\to A{\cdot }_{\mathrm{ih}}A\in ℝ$$
15		leloe	$$⊢\left(0\in ℝ\wedge A{\cdot }_{\mathrm{ih}}A\in ℝ\right)\to \left(0\le A{\cdot }_{\mathrm{ih}}A\leftrightarrow \left(0<A{\cdot }_{\mathrm{ih}}A\vee 0=A{\cdot }_{\mathrm{ih}}A\right)\right)$$
16	13 14 15	sylancr	$$⊢A\in \mathscr{H}\to \left(0\le A{\cdot }_{\mathrm{ih}}A\leftrightarrow \left(0<A{\cdot }_{\mathrm{ih}}A\vee 0=A{\cdot }_{\mathrm{ih}}A\right)\right)$$
17	12 16	mpbird	$$⊢A\in \mathscr{H}\to 0\le A{\cdot }_{\mathrm{ih}}A$$