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 = { t e. ( ~H ^m ~H ) | A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cho	|- HrmOp
1		vt	|- t
2		chba	|- ~H
3		cmap	|- ^m
4	2 2 3	co	|- ( ~H ^m ~H )
5		vx	|- x
6		vy	|- y
7	5	cv	|- x
8		csp	|- .ih
9	1	cv	|- t
10	6	cv	|- y
11	10 9	cfv	|- ( t ` y )
12	7 11 8	co	|- ( x .ih ( t ` y ) )
13	7 9	cfv	|- ( t ` x )
14	13 10 8	co	|- ( ( t ` x ) .ih y )
15	12 14	wceq	|- ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y )
16	15 6 2	wral	|- A. y e. ~H ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y )
17	16 5 2	wral	|- A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y )
18	17 1 4	crab	|- { t e. ( ~H ^m ~H ) | A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y ) }
19	0 18	wceq	|- HrmOp = { t e. ( ~H ^m ~H ) | A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( t ` x ) .ih y ) }