Theorem pjhmopidm

Description: Two ways to express the set of all projection operators. (Contributed by NM, 24-Apr-2006) (Proof shortened by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	pjhmopidm	⊢ ran projℎ = { 𝑡 ∈ HrmOp ∣ ( 𝑡 ∘ 𝑡 ) = 𝑡 }

Proof

Step	Hyp	Ref	Expression
1		dfpjop	⊢ ( 𝑡 ∈ ran projℎ ↔ ( 𝑡 ∈ HrmOp ∧ ( 𝑡 ∘ 𝑡 ) = 𝑡 ) )
2	1	abbi2i	⊢ ran projℎ = { 𝑡 ∣ ( 𝑡 ∈ HrmOp ∧ ( 𝑡 ∘ 𝑡 ) = 𝑡 ) }
3		df-rab	⊢ { 𝑡 ∈ HrmOp ∣ ( 𝑡 ∘ 𝑡 ) = 𝑡 } = { 𝑡 ∣ ( 𝑡 ∈ HrmOp ∧ ( 𝑡 ∘ 𝑡 ) = 𝑡 ) }
4	2 3	eqtr4i	⊢ ran projℎ = { 𝑡 ∈ HrmOp ∣ ( 𝑡 ∘ 𝑡 ) = 𝑡 }