Metamath Proof Explorer

Theorem pjoccl

Description: The part of a vector that belongs to the orthocomplemented space. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjop ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A = A - ℎ proj ℎ ⁡ H ⁡ A
2 choccl ⊢ H ∈ C ℋ → ⊥ ⁡ H ∈ C ℋ
3 axpjcl ⊢ ⊥ ⁡ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ⊥ ⁡ H
4 2 3 sylan ⊢ H ∈ C ℋ ∧ A ∈ ℋ → proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ⊥ ⁡ H
5 1 4 eqeltrrd ⊢ H ∈ C ℋ ∧ A ∈ ℋ → A - ℎ proj ℎ ⁡ H ⁡ A ∈ ⊥ ⁡ H