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

Metamath Proof Explorer

Definition df-hmop

Description: Define the set of Hermitian operators on Hilbert space. Some books call these "symmetric operators" and others call them "self-adjoint operators", sometimes with slightly different technical meanings. (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion df-hmop HrmOp = { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cho ⊢ HrmOp
1 vt ⊢ 𝑡
2 chba ⊢ ℋ
3 cmap ⊢ ↑m
4 2 2 3 co ⊢ ( ℋ ↑m ℋ )
5 vx ⊢ 𝑥
6 vy ⊢ 𝑦
7 5 cv ⊢ 𝑥
8 csp ⊢ ·ih
9 1 cv ⊢ 𝑡
10 6 cv ⊢ 𝑦
11 10 9 cfv ⊢ ( 𝑡 ‘ 𝑦 )
12 7 11 8 co ⊢ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) )
13 7 9 cfv ⊢ ( 𝑡 ‘ 𝑥 )
14 13 10 8 co ⊢ ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 )
15 12 14 wceq ⊢ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 )
16 15 6 2 wral ⊢ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 )
17 16 5 2 wral ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 )
18 17 1 4 crab ⊢ { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) }
19 0 18 wceq ⊢ HrmOp = { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) }