This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ) )