This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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