This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjocvec

Description: The set of vectors belonging to the orthocomplemented subspace of a projection. Second part of Theorem 27.3 of Halmos p. 45. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion pjocvec ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) = { 𝑥 ∈ ℋ ∣ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) = 0ℎ } )

Proof

Step Hyp Ref Expression
1 choccl ⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ∈ Cℋ )
2 chss ⊢ ( ( ⊥ ‘ 𝐻 ) ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ⊆ ℋ )
3 1 2 syl ⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ⊆ ℋ )
4 sseqin2 ⊢ ( ( ⊥ ‘ 𝐻 ) ⊆ ℋ ↔ ( ℋ ∩ ( ⊥ ‘ 𝐻 ) ) = ( ⊥ ‘ 𝐻 ) )
5 3 4 sylib ⊢ ( 𝐻 ∈ Cℋ → ( ℋ ∩ ( ⊥ ‘ 𝐻 ) ) = ( ⊥ ‘ 𝐻 ) )
6 pjoc2 ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ∈ ( ⊥ ‘ 𝐻 ) ↔ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) = 0ℎ ) )
7 6 rabbi2dva ⊢ ( 𝐻 ∈ Cℋ → ( ℋ ∩ ( ⊥ ‘ 𝐻 ) ) = { 𝑥 ∈ ℋ ∣ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) = 0ℎ } )
8 5 7 eqtr3d ⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) = { 𝑥 ∈ ℋ ∣ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) = 0ℎ } )