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 𝑦 ) }