Theorem hiidge0

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

	Ref	Expression
Assertion	hiidge0	⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( 𝐴 ·ih 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.1	⊢ ( ¬ 𝐴 = 0ℎ ∨ 𝐴 = 0ℎ )
2		df-ne	⊢ ( 𝐴 ≠ 0ℎ ↔ ¬ 𝐴 = 0ℎ )
3		ax-his4	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ ) → 0 < ( 𝐴 ·ih 𝐴 ) )
4	2 3	sylan2br	⊢ ( ( 𝐴 ∈ ℋ ∧ ¬ 𝐴 = 0ℎ ) → 0 < ( 𝐴 ·ih 𝐴 ) )
5	4	ex	⊢ ( 𝐴 ∈ ℋ → ( ¬ 𝐴 = 0ℎ → 0 < ( 𝐴 ·ih 𝐴 ) ) )
6		oveq1	⊢ ( 𝐴 = 0ℎ → ( 𝐴 ·ih 𝐴 ) = ( 0ℎ ·ih 𝐴 ) )
7		hi01	⊢ ( 𝐴 ∈ ℋ → ( 0ℎ ·ih 𝐴 ) = 0 )
8	6 7	sylan9eqr	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 = 0ℎ ) → ( 𝐴 ·ih 𝐴 ) = 0 )
9	8	eqcomd	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 = 0ℎ ) → 0 = ( 𝐴 ·ih 𝐴 ) )
10	9	ex	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 = 0ℎ → 0 = ( 𝐴 ·ih 𝐴 ) ) )
11	5 10	orim12d	⊢ ( 𝐴 ∈ ℋ → ( ( ¬ 𝐴 = 0ℎ ∨ 𝐴 = 0ℎ ) → ( 0 < ( 𝐴 ·ih 𝐴 ) ∨ 0 = ( 𝐴 ·ih 𝐴 ) ) ) )
12	1 11	mpi	⊢ ( 𝐴 ∈ ℋ → ( 0 < ( 𝐴 ·ih 𝐴 ) ∨ 0 = ( 𝐴 ·ih 𝐴 ) ) )
13		0re	⊢ 0 ∈ ℝ
14		hiidrcl	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ·ih 𝐴 ) ∈ ℝ )
15		leloe	⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 ·ih 𝐴 ) ∈ ℝ ) → ( 0 ≤ ( 𝐴 ·ih 𝐴 ) ↔ ( 0 < ( 𝐴 ·ih 𝐴 ) ∨ 0 = ( 𝐴 ·ih 𝐴 ) ) ) )
16	13 14 15	sylancr	⊢ ( 𝐴 ∈ ℋ → ( 0 ≤ ( 𝐴 ·ih 𝐴 ) ↔ ( 0 < ( 𝐴 ·ih 𝐴 ) ∨ 0 = ( 𝐴 ·ih 𝐴 ) ) ) )
17	12 16	mpbird	⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( 𝐴 ·ih 𝐴 ) )