# Metamath Proof Explorer

## Theorem pjhmop

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

Ref Expression
Assertion pjhmop ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\in \mathrm{HrmOp}$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}{H}=if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)$
2 1 eleq1d ${⊢}{H}=if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\in \mathrm{HrmOp}↔{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)\in \mathrm{HrmOp}\right)$
3 h0elch ${⊢}{0}_{ℋ}\in {\mathbf{C}}_{ℋ}$
4 3 elimel ${⊢}if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
5 4 pjhmopi ${⊢}{\mathrm{proj}}_{ℎ}\left(if\left({H}\in {\mathbf{C}}_{ℋ},{H},{0}_{ℋ}\right)\right)\in \mathrm{HrmOp}$
6 2 5 dedth ${⊢}{H}\in {\mathbf{C}}_{ℋ}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\in \mathrm{HrmOp}$