Metamath Proof Explorer

Theorem pjop

Description: Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion pjop ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A = A - ℎ proj ℎ ⁡ H ⁡ A

Proof

Step Hyp Ref Expression
1 axpjpj ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A = proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A
2 1 eqcomd ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A = A
3 simpr ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A ∈ ℋ
4 pjhcl ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ H ⁡ A ∈ ℋ
5 choccl ⊢ H ∈ C ℋ → ⊥ ⁡ H ∈ C ℋ
6 pjhcl ⊢ ⊥ ⁡ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ℋ
7 5 6 sylan ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ℋ
8 hvsubadd ⊢ A ∈ ℋ ∧ proj ℎ ⁡ H ⁡ A ∈ ℋ ∧ proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ℋ → A - ℎ proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ ⊥ ⁡ H ⁡ A ↔ proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A = A
9 3 4 7 8 syl3anc ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A - ℎ proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ ⊥ ⁡ H ⁡ A ↔ proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A = A
10 2 9 mpbird ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A - ℎ proj ℎ ⁡ H ⁡ A = proj ℎ ⁡ ⊥ ⁡ H ⁡ A
11 10 eqcomd ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A = A - ℎ proj ℎ ⁡ H ⁡ A