Definition df-hmop 9765

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.

Assertion

Ref	Expression
df-hmop	|- HrmOp = {t | (t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((t` x) .ih y))}

Distinct variable group:   x,t,y

Detailed syntax breakdown of Definition df-hmop

Step	Hyp	Ref	Expression
1		cho 8814	. 2 class HrmOp
2		chil 8783	. . . . 5 class H~
3		vt	. . . . . 6 set t
4	3	cv 957	. . . . 5 class t
5	2, 2, 4	wf 3184	. . . 4 wff t:H~-->H~
6		vx	. . . . . . . . 9 set x
7	6	cv 957	. . . . . . . 8 class x
8		vy	. . . . . . . . . 10 set y
9	8	cv 957	. . . . . . . . 9 class y
10	9, 4	cfv 3188	. . . . . . . 8 class (t` y)
11		csp 8788	. . . . . . . 8 class .ih
12	7, 10, 11	co 3969	. . . . . . 7 class (x .ih (t` y))
13	7, 4	cfv 3188	. . . . . . . 8 class (t` x)
14	13, 9, 11	co 3969	. . . . . . 7 class ((t` x) .ih y)
15	12, 14	wceq 958	. . . . . 6 wff (x .ih (t` y)) = ((t` x) .ih y)
16	15, 8, 2	wral 1648	. . . . 5 wff A.y e. H~ (x .ih (t` y)) = ((t` x) .ih y)
17	16, 6, 2	wral 1648	. . . 4 wff A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((t` x) .ih y)
18	5, 17	wa 223	. . 3 wff (t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((t` x) .ih y))
19	18, 3	cab 1466	. 2 class {t | (t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((t` x) .ih y))}
20	1, 19	wceq 958	1 wff HrmOp = {t | (t:H~-->H~ /\ A.x e. H~ A.y e. H~ (x .ih (t` y)) = ((t` x) .ih y))}

This definition is referenced by:  elhmopt 9795

Copyright terms: Public domain