Metamath Proof Explorer

Theorem pjorthi

Description: Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjorth.1 ⊢ A ∈ ℋ
pjorth.2 ⊢ B ∈ ℋ
Assertion pjorthi ⊢ H ∈ C ℋ → proj ℎ ⁡ H ⁡ A ⋅ ih proj ℎ ⁡ ⊥ ⁡ H ⁡ B = 0

Proof

Step Hyp Ref Expression
1 pjorth.1 ⊢ A ∈ ℋ
2 pjorth.2 ⊢ B ∈ ℋ
3 chsh ⊢ H ∈ C ℋ → H ∈ S ℋ
4 axpjcl ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ H ⁡ A ∈ H
5 1 4 mpan2 ⊢ H ∈ C ℋ → proj ℎ ⁡ H ⁡ A ∈ H
6 choccl ⊢ H ∈ C ℋ → ⊥ ⁡ H ∈ C ℋ
7 axpjcl ⊢ ⊥ ⁡ H ∈ C ℋ ∧ B ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ B ∈ ⊥ ⁡ H
8 6 2 7 sylancl ⊢ H ∈ C ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ B ∈ ⊥ ⁡ H
9 5 8 jca ⊢ H ∈ C ℋ → proj ℎ ⁡ H ⁡ A ∈ H ∧ proj ℎ ⁡ ⊥ ⁡ H ⁡ B ∈ ⊥ ⁡ H
10 shocorth ⊢ H ∈ S ℋ → proj ℎ ⁡ H ⁡ A ∈ H ∧ proj ℎ ⁡ ⊥ ⁡ H ⁡ B ∈ ⊥ ⁡ H → proj ℎ ⁡ H ⁡ A ⋅ ih proj ℎ ⁡ ⊥ ⁡ H ⁡ B = 0
11 3 9 10 sylc ⊢ H ∈ C ℋ → proj ℎ ⁡ H ⁡ A ⋅ ih proj ℎ ⁡ ⊥ ⁡ H ⁡ B = 0