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