Metamath Proof Explorer

Theorem elpjidm

Description: A projection operator is idempotent. Part of Theorem 26.1 of Halmos p. 43. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion elpjidm T ran proj T T = T


Step Hyp Ref Expression
1 dfpjop T ran proj T HrmOp T T = T
2 1 simprbi T ran proj T T = T