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 | ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjop | ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) = ( 𝐴 −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) | |
2 | choccl | ⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ∈ Cℋ ) | |
3 | axpjcl | ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) | |
4 | 2 3 | sylan | ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) |
5 | 1 4 | eqeltrrd | ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) |