Theorem idhmop

Description: The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	idhmop	⊢ Iop ∈ HrmOp

Proof

Step	Hyp	Ref	Expression
1		hoif	⊢ Iop : ℋ –1-1-onto→ ℋ
2		f1of	⊢ ( Iop : ℋ –1-1-onto→ ℋ → Iop : ℋ ⟶ ℋ )
3	1 2	ax-mp	⊢ Iop : ℋ ⟶ ℋ
4		hoival	⊢ ( 𝑥 ∈ ℋ → ( Iop ‘ 𝑥 ) = 𝑥 )
5	4	eqcomd	⊢ ( 𝑥 ∈ ℋ → 𝑥 = ( Iop ‘ 𝑥 ) )
6		hoival	⊢ ( 𝑦 ∈ ℋ → ( Iop ‘ 𝑦 ) = 𝑦 )
7	5 6	oveqan12d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( Iop ‘ 𝑦 ) ) = ( ( Iop ‘ 𝑥 ) ·ih 𝑦 ) )
8	7	rgen2	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( Iop ‘ 𝑦 ) ) = ( ( Iop ‘ 𝑥 ) ·ih 𝑦 )
9		elhmop	⊢ ( Iop ∈ HrmOp ↔ ( Iop : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( Iop ‘ 𝑦 ) ) = ( ( Iop ‘ 𝑥 ) ·ih 𝑦 ) ) )
10	3 8 9	mpbir2an	⊢ Iop ∈ HrmOp