Metamath Proof Explorer

Theorem pjpo

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

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

Proof

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