Definition df-lnfn 25387

Description: Define the set of linear functionals on Hilbert space. (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)

Assertion

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

Distinct variable group:   x, t, y, z

Detailed syntax breakdown of Definition df-lnfn

Step	Hyp	Ref	Expression
1		clf 24491	. 2 class LinFn
2		vx	. . . . . . . . . . 11 setvar x
3	2	cv 1369	. . . . . . . . . 10 class x
4		vy	. . . . . . . . . . 11 setvar y
5	4	cv 1369	. . . . . . . . . 10 class y
6		csm 24458	. . . . . . . . . 10 class .h
7	3, 5, 6	co 6190	. . . . . . . . 9 class ( x .h y )
8		vz	. . . . . . . . . 10 setvar z
9	8	cv 1369	. . . . . . . . 9 class z
10		cva 24457	. . . . . . . . 9 class +h
11	7, 9, 10	co 6190	. . . . . . . 8 class ( ( x .h y ) +h z )
12		vt	. . . . . . . . 9 setvar t
13	12	cv 1369	. . . . . . . 8 class t
14	11, 13	cfv 5516	. . . . . . 7 class ( t ` ( ( x .h y ) +h z ) )
15	5, 13	cfv 5516	. . . . . . . . 9 class ( t ` y )
16		cmul 9388	. . . . . . . . 9 class x.
17	3, 15, 16	co 6190	. . . . . . . 8 class ( x x. ( t ` y ) )
18	9, 13	cfv 5516	. . . . . . . 8 class ( t ` z )
19		caddc 9386	. . . . . . . 8 class +
20	17, 18, 19	co 6190	. . . . . . 7 class ( ( x x. ( t ` y ) ) + ( t ` z ) )
21	14, 20	wceq 1370	. . . . . 6 wff ( t ` ( ( x .h y ) +h z ) ) = ( ( x x. ( t ` y ) ) + ( t ` z ) )
22		chil 24456	. . . . . 6 class ~H
23	21, 8, 22	wral 2795	. . . . 5 wff A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x x. ( t ` y ) ) + ( t ` z ) )
24	23, 4, 22	wral 2795	. . . 4 wff A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x x. ( t ` y ) ) + ( t ` z ) )
25		cc 9381	. . . 4 class CC
26	24, 2, 25	wral 2795	. . 3 wff A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x x. ( t ` y ) ) + ( t ` z ) )
27		cmap 7314	. . . 4 class ^m
28	25, 22, 27	co 6190	. . 3 class ( CC ^m ~H )
29	26, 12, 28	crab 2799	. 2 class { t e. ( CC ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x x. ( t ` y ) ) + ( t ` z ) ) }
30	1, 29	wceq 1370	1 wff LinFn = { t e. ( CC ^m ~H ) | A. x e. CC A. y e. ~H A. z e. ~H ( t ` ( ( x .h y ) +h z ) ) = ( ( x x. ( t ` y ) ) + ( t ` z ) ) }

This definition is referenced by:  ellnfn  25422