This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-lnop

Description: Define the set of linear operators on Hilbert space. (See df-hosum for definition of operator.) (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion df-lnop 
|- LinOp = { t e. ( ~H ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clo 
 |-  LinOp
1 vt 
 |-  t
2 chba 
 |-  ~H
3 cmap 
 |-  ^m
4 2 2 3 co 
 |-  ( ~H ^m ~H )
5 vx 
 |-  x
6 cc 
 |-  CC
7 vy 
 |-  y
8 vz 
 |-  z
9 1 cv 
 |-  t
10 5 cv 
 |-  x
11 csm 
 |-  .h
12 7 cv 
 |-  y
13 10 12 11 co 
 |-  ( x .h y )
14 cva 
 |-  +h
15 8 cv 
 |-  z
16 13 15 14 co 
 |-  ( ( x .h y ) +h z )
17 16 9 cfv 
 |-  ( t ` ( ( x .h y ) +h z ) )
18 12 9 cfv 
 |-  ( t ` y )
19 10 18 11 co 
 |-  ( x .h ( t ` y ) )
20 15 9 cfv 
 |-  ( t ` z )
21 19 20 14 co 
 |-  ( ( x .h ( t ` y ) ) +h ( t ` z ) )
22 17 21 wceq 
 |-  ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) )
23 22 8 2 wral 
 |-  A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) )
24 23 7 2 wral 
 |-  A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) )
25 24 5 6 wral 
 |-  A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) )
26 25 1 4 crab 
 |-  { t e. ( ~H ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) ) }
27 0 26 wceq 
 |-  LinOp = { t e. ( ~H ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) ) }