Theorem pjhmopi

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

	Ref	Expression
Hypothesis	pjhmop.1	|- H e. CH
Assertion	pjhmopi	|- ( projh ` H ) e. HrmOp

Proof

Step	Hyp	Ref	Expression
1		pjhmop.1	|- H e. CH
2	1	pjfi	|- ( projh ` H ) : ~H --> ~H
3	1	pjadji	|- ( ( x e. ~H /\ y e. ~H ) -> ( ( ( projh ` H ) ` x ) .ih y ) = ( x .ih ( ( projh ` H ) ` y ) ) )
4	3	eqcomd	|- ( ( x e. ~H /\ y e. ~H ) -> ( x .ih ( ( projh ` H ) ` y ) ) = ( ( ( projh ` H ) ` x ) .ih y ) )
5	4	rgen2	|- A. x e. ~H A. y e. ~H ( x .ih ( ( projh ` H ) ` y ) ) = ( ( ( projh ` H ) ` x ) .ih y )
6		elhmop	|- ( ( projh ` H ) e. HrmOp <-> ( ( projh ` H ) : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( ( projh ` H ) ` y ) ) = ( ( ( projh ` H ) ` x ) .ih y ) ) )
7	2 5 6	mpbir2an	|- ( projh ` H ) e. HrmOp