Theorem pjvec

Description: The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjvec	⊢ ( 𝐻 ∈ Cℋ → 𝐻 = { 𝑥 ∈ ℋ ∣ ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) = 𝑥 } )

Proof

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