Theorem pjhmop

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

	Ref	Expression
Assertion	pjhmop	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) ∈ HrmOp )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( projℎ ‘ 𝐻 ) = ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) )
2	1	eleq1d	⊢ ( 𝐻 = if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) → ( ( projℎ ‘ 𝐻 ) ∈ HrmOp ↔ ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ∈ HrmOp ) )
3		h0elch	⊢ 0ℋ ∈ Cℋ
4	3	elimel	⊢ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ∈ Cℋ
5	4	pjhmopi	⊢ ( projℎ ‘ if ( 𝐻 ∈ Cℋ , 𝐻 , 0ℋ ) ) ∈ HrmOp
6	2 5	dedth	⊢ ( 𝐻 ∈ Cℋ → ( projℎ ‘ 𝐻 ) ∈ HrmOp )