Theorem pjhmop

Description: A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjhmop	|- ( H e. CH -> ( projh ` H ) e. HrmOp )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( H = if ( H e. CH , H , 0H ) -> ( projh ` H ) = ( projh ` if ( H e. CH , H , 0H ) ) )
2	1	eleq1d	|- ( H = if ( H e. CH , H , 0H ) -> ( ( projh ` H ) e. HrmOp <-> ( projh ` if ( H e. CH , H , 0H ) ) e. HrmOp ) )
3		h0elch	|- 0H e. CH
4	3	elimel	|- if ( H e. CH , H , 0H ) e. CH
5	4	pjhmopi	|- ( projh ` if ( H e. CH , H , 0H ) ) e. HrmOp
6	2 5	dedth	|- ( H e. CH -> ( projh ` H ) e. HrmOp )