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

Metamath Proof Explorer

Theorem pjinormi

Description: The inner product of a projection and its argument is the square of the norm of the projection. Remark in Halmos p. 44. (Contributed by NM, 2-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis pjadjt.1 ⊢ H ∈ C ℋ
Assertion pjinormi ⊢ A ∈ ℋ → proj ℎ ⁡ H ⁡ A ⋅ ih A = norm ℎ ⁡ proj ℎ ⁡ H ⁡ A 2

Proof

Step Hyp Ref Expression
1 pjadjt.1 ⊢ H ∈ C ℋ
2 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ
3 id ⊢ A = if A ∈ ℋ A 0 ℎ → A = if A ∈ ℋ A 0 ℎ
4 2 3 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ H ⁡ A ⋅ ih A = proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
5 2fveq3 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ proj ℎ ⁡ H ⁡ A = norm ℎ ⁡ proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ
6 5 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ proj ℎ ⁡ H ⁡ A 2 = norm ℎ ⁡ proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ 2
7 4 6 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → proj ℎ ⁡ H ⁡ A ⋅ ih A = norm ℎ ⁡ proj ℎ ⁡ H ⁡ A 2 ↔ proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ = norm ℎ ⁡ proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ 2
8 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
9 1 8 pjinormii ⊢ proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ = norm ℎ ⁡ proj ℎ ⁡ H ⁡ if A ∈ ℋ A 0 ℎ 2
10 7 9 dedth ⊢ A ∈ ℋ → proj ℎ ⁡ H ⁡ A ⋅ ih A = norm ℎ ⁡ proj ℎ ⁡ H ⁡ A 2