Definition df-lnop 28700

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

Assertion

Ref	Expression
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 ) ) }

Distinct variable group:   x, t, y, z

Detailed syntax breakdown of Definition df-lnop

Step	Hyp	Ref	Expression
1		clo 27804	. 2 class LinOp
2		vx	. . . . . . . . . . 11 setvar x
3	2	cv 1482	. . . . . . . . . 10 class x
4		vy	. . . . . . . . . . 11 setvar y
5	4	cv 1482	. . . . . . . . . 10 class y
6		csm 27778	. . . . . . . . . 10 class .h
7	3, 5, 6	co 6650	. . . . . . . . 9 class ( x .h y )
8		vz	. . . . . . . . . 10 setvar z
9	8	cv 1482	. . . . . . . . 9 class z
10		cva 27777	. . . . . . . . 9 class +h
11	7, 9, 10	co 6650	. . . . . . . 8 class ( ( x .h y ) +h z )
12		vt	. . . . . . . . 9 setvar t
13	12	cv 1482	. . . . . . . 8 class t
14	11, 13	cfv 5888	. . . . . . 7 class ( t ` ( ( x .h y ) +h z ) )
15	5, 13	cfv 5888	. . . . . . . . 9 class ( t ` y )
16	3, 15, 6	co 6650	. . . . . . . 8 class ( x .h ( t ` y ) )
17	9, 13	cfv 5888	. . . . . . . 8 class ( t ` z )
18	16, 17, 10	co 6650	. . . . . . 7 class ( ( x .h ( t ` y ) ) +h ( t ` z ) )
19	14, 18	wceq 1483	. . . . . 6 wff ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) )
20		chil 27776	. . . . . 6 class ~H
21	19, 8, 20	wral 2912	. . . . 5 wff A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) )
22	21, 4, 20	wral 2912	. . . 4 wff A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x .h ( t ` y ) ) +h ( t ` z ) )
23		cc 9934	. . . 4 class CC
24	22, 2, 23	wral 2912	. . 3 wff 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 ) )
25		cmap 7857	. . . 4 class ^m
26	20, 20, 25	co 6650	. . 3 class ( ~H ^m ~H )
27	24, 12, 26	crab 2916	. 2 class { 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 ) ) }
28	1, 27	wceq 1483	1 wff 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 ) ) }

This definition is referenced by:  ellnop  28717  hhlnoi  28759