Definition df-unop 9900

Description: Define the set of unitary operators on Hilbert space.

Assertion

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

Distinct variable group:   x,t,y

Detailed syntax breakdown of Definition df-unop

Step	Hyp	Ref	Expression
1		cuo 8998	. 2 class UniOp
2		chil 8968	. . . . 5 class H~
3		vt	. . . . . 6 set t
4	3	cv 1098	. . . . 5 class t
5	2, 2, 4	wfo 3143	. . . 4 wff t:H~-onto->H~
6		vx	. . . . . . . . . 10 set x
7	6	cv 1098	. . . . . . . . 9 class x
8	7, 4	cfv 3145	. . . . . . . 8 class (t` x)
9		vy	. . . . . . . . . 10 set y
10	9	cv 1098	. . . . . . . . 9 class y
11	10, 4	cfv 3145	. . . . . . . 8 class (t` y)
12		csp 8973	. . . . . . . 8 class .ih
13	8, 11, 12	co 3902	. . . . . . 7 class ((t` x) .ih (t` y))
14	7, 10, 12	co 3902	. . . . . . 7 class (x .ih y)
15	13, 14	wceq 1099	. . . . . 6 wff ((t` x) .ih (t` y)) = (x .ih y)
16	15, 9, 2	wral 1621	. . . . 5 wff A.y e. H~ ((t` x) .ih (t` y)) = (x .ih y)
17	16, 6, 2	wral 1621	. . . 4 wff A.x e. H~ A.y e. H~ ((t` x) .ih (t` y)) = (x .ih y)
18	5, 17	wa 223	. . 3 wff (t:H~-onto->H~ /\ A.x e. H~ A.y e. H~ ((t` x) .ih (t` y)) = (x .ih y))
19	18, 3	cab 1440	. 2 class {t | (t:H~-onto->H~ /\ A.x e. H~ A.y e. H~ ((t` x) .ih (t` y)) = (x .ih y))}
20	1, 19	wceq 1099	1 wff UniOp = {t | (t:H~-onto->H~ /\ A.x e. H~ A.y e. H~ ((t` x) .ih (t` y)) = (x .ih y))}

This definition is referenced by:  elunopt 9930

Copyright terms: Public domain