Theorem pjhmopi

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

	Ref	Expression
Hypothesis	pjhmop.1	⊢ 𝐻 ∈ Cℋ
Assertion	pjhmopi	⊢ ( projℎ ‘ 𝐻 ) ∈ HrmOp

Proof

Step	Hyp	Ref	Expression
1		pjhmop.1	⊢ 𝐻 ∈ Cℋ
2	1	pjfi	⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
3	1	pjadji	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) )
4	3	eqcomd	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ·ih 𝑦 ) )
5	4	rgen2	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ·ih 𝑦 )
6		elhmop	⊢ ( ( projℎ ‘ 𝐻 ) ∈ HrmOp ↔ ( ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝑦 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝑥 ) ·ih 𝑦 ) ) )
7	2 5 6	mpbir2an	⊢ ( projℎ ‘ 𝐻 ) ∈ HrmOp