Metamath Proof Explorer


Theorem pjige0i

Description: The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis pjadjt.1 𝐻C
Assertion pjige0i ( 𝐴 ∈ ℋ → 0 ≤ ( ( ( proj𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pjadjt.1 𝐻C
2 1 pjhcli ( 𝐴 ∈ ℋ → ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ℋ )
3 normcl ( ( ( proj𝐻 ) ‘ 𝐴 ) ∈ ℋ → ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ℝ )
4 2 3 syl ( 𝐴 ∈ ℋ → ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ∈ ℝ )
5 4 sqge0d ( 𝐴 ∈ ℋ → 0 ≤ ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) )
6 1 pjinormi ( 𝐴 ∈ ℋ → ( ( ( proj𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) = ( ( norm ‘ ( ( proj𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) )
7 5 6 breqtrrd ( 𝐴 ∈ ℋ → 0 ≤ ( ( ( proj𝐻 ) ‘ 𝐴 ) ·ih 𝐴 ) )