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

Metamath Proof Explorer

Theorem pjige0

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

Ref Expression
Assertion pjige0 ⊢ H ∈ C ℋ ∧ A ∈ ℋ → 0 ≤ proj ℎ ⁡ H ⁡ A ⋅ ih A

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ H = if H ∈ C ℋ H 0 ℋ → proj ℎ ⁡ H = proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ
2 1 fveq1d ⊢ H = if H ∈ C ℋ H 0 ℋ → proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A
3 2 oveq1d ⊢ H = if H ∈ C ℋ H 0 ℋ → proj ℎ ⁡ H ⁡ A ⋅ ih A = proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A ⋅ ih A
4 3 breq2d ⊢ H = if H ∈ C ℋ H 0 ℋ → 0 ≤ proj ℎ ⁡ H ⁡ A ⋅ ih A ↔ 0 ≤ proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A ⋅ ih A
5 4 imbi2d ⊢ H = if H ∈ C ℋ H 0 ℋ → A ∈ ℋ → 0 ≤ proj ℎ ⁡ H ⁡ A ⋅ ih A ↔ A ∈ ℋ → 0 ≤ proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A ⋅ ih A
6 h0elch ⊢ 0 ℋ ∈ C ℋ
7 6 elimel ⊢ if H ∈ C ℋ H 0 ℋ ∈ C ℋ
8 7 pjige0i ⊢ A ∈ ℋ → 0 ≤ proj ℎ ⁡ if H ∈ C ℋ H 0 ℋ ⁡ A ⋅ ih A
9 5 8 dedth ⊢ H ∈ C ℋ → A ∈ ℋ → 0 ≤ proj ℎ ⁡ H ⁡ A ⋅ ih A
10 9 imp ⊢ H ∈ C ℋ ∧ A ∈ ℋ → 0 ≤ proj ℎ ⁡ H ⁡ A ⋅ ih A