Theorem pjidmcoi

Description: A projection is idempotent. Property (ii) of Beran p. 109. (Contributed by NM, 1-Oct-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjidmco.1	⊢ 𝐻 ∈ Cℋ
Assertion	pjidmcoi	⊢ ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		pjidmco.1	⊢ 𝐻 ∈ Cℋ
2		ssid	⊢ 𝐻 ⊆ 𝐻
3	1 1	pjss2coi	⊢ ( 𝐻 ⊆ 𝐻 ↔ ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 ) )
4	2 3	mpbi	⊢ ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐻 )