Metamath Proof Explorer


Theorem elpjhmop

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

Ref Expression
Assertion elpjhmop
|- ( T e. ran projh -> T e. HrmOp )

Proof

Step Hyp Ref Expression
1 dfpjop
 |-  ( T e. ran projh <-> ( T e. HrmOp /\ ( T o. T ) = T ) )
2 1 simplbi
 |-  ( T e. ran projh -> T e. HrmOp )