Definition df-unop 28702

Description: Define the set of unitary operators on Hilbert space. (Contributed by NM, 18-Jan-2006.) (New usage is discouraged.)

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 27806	. 2 class UniOp
2		chil 27776	. . . . 5 class ~H
3		vt	. . . . . 6 setvar t
4	3	cv 1482	. . . . 5 class t
5	2, 2, 4	wfo 5886	. . . 4 wff t : ~H -onto-> ~H
6		vx	. . . . . . . . . 10 setvar x
7	6	cv 1482	. . . . . . . . 9 class x
8	7, 4	cfv 5888	. . . . . . . 8 class ( t ` x )
9		vy	. . . . . . . . . 10 setvar y
10	9	cv 1482	. . . . . . . . 9 class y
11	10, 4	cfv 5888	. . . . . . . 8 class ( t ` y )
12		csp 27779	. . . . . . . 8 class .ih
13	8, 11, 12	co 6650	. . . . . . 7 class ( ( t ` x ) .ih ( t ` y ) )
14	7, 10, 12	co 6650	. . . . . . 7 class ( x .ih y )
15	13, 14	wceq 1483	. . . . . 6 wff ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y )
16	15, 9, 2	wral 2912	. . . . 5 wff A. y e. ~H ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y )
17	16, 6, 2	wral 2912	. . . 4 wff A. x e. ~H A. y e. ~H ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y )
18	5, 17	wa 384	. . 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 2608	. 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 1483	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:  elunop  28731