Theorem elpjch

Description: Reconstruction of the subspace of a projection operator. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	elpjch	⊢ ( 𝑇 ∈ ran projℎ → ( ran 𝑇 ∈ Cℋ ∧ 𝑇 = ( projℎ ‘ ran 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfpjop	⊢ ( 𝑇 ∈ ran projℎ ↔ ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) )
2		hmopidmch	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) → ran 𝑇 ∈ Cℋ )
3		hmopidmpj	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) → 𝑇 = ( projℎ ‘ ran 𝑇 ) )
4	2 3	jca	⊢ ( ( 𝑇 ∈ HrmOp ∧ ( 𝑇 ∘ 𝑇 ) = 𝑇 ) → ( ran 𝑇 ∈ Cℋ ∧ 𝑇 = ( projℎ ‘ ran 𝑇 ) ) )
5	1 4	sylbi	⊢ ( 𝑇 ∈ ran projℎ → ( ran 𝑇 ∈ Cℋ ∧ 𝑇 = ( projℎ ‘ ran 𝑇 ) ) )