Metamath Proof Explorer

Definition df-unop

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuo 
 |-  UniOp
1 vt 
 |-  t
2 1 cv 
 |-  t
3 chba 
 |-  ~H
4 3 3 2 wfo 
 |-  t : ~H -onto-> ~H
5 vx 
 |-  x
6 vy 
 |-  y
7 5 cv 
 |-  x
8 7 2 cfv 
 |-  ( t ` x )
9 csp 
 |-  .ih
10 6 cv 
 |-  y
11 10 2 cfv 
 |-  ( t ` y )
12 8 11 9 co 
 |-  ( ( t ` x ) .ih ( t ` y ) )
13 7 10 9 co 
 |-  ( x .ih y )
14 12 13 wceq 
 |-  ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y )
15 14 6 3 wral 
 |-  A. y e. ~H ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y )
16 15 5 3 wral 
 |-  A. x e. ~H A. y e. ~H ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y )
17 4 16 wa 
 |-  ( t : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y ) )
18 17 1 cab 
 |-  { t | ( t : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y ) ) }
19 0 18 wceq 
 |-  UniOp = { t | ( t : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( t ` x ) .ih ( t ` y ) ) = ( x .ih y ) ) }