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