Definition df-nlfn 9767

Description: Define the null space of a Hilbert space functional.

Assertion

Ref	Expression
df-nlfn	|- null = {<.t, y>. | (t:H~-->CC /\ y = {x e. H~ | (t` x) = 0})}

Distinct variable group:   x,t,y

Detailed syntax breakdown of Definition df-nlfn

Step	Hyp	Ref	Expression
1		cnl 8816	. 2 class null
2		chil 8783	. . . . 5 class H~
3		cc 5244	. . . . 5 class CC
4		vt	. . . . . 6 set t
5	4	cv 957	. . . . 5 class t
6	2, 3, 5	wf 3184	. . . 4 wff t:H~-->CC
7		vy	. . . . . 6 set y
8	7	cv 957	. . . . 5 class y
9		vx	. . . . . . . . 9 set x
10	9	cv 957	. . . . . . . 8 class x
11	10, 5	cfv 3188	. . . . . . 7 class (t` x)
12		cc0 5246	. . . . . . 7 class 0
13	11, 12	wceq 958	. . . . . 6 wff (t` x) = 0
14	13, 9, 2	crab 1651	. . . . 5 class {x e. H~ | (t` x) = 0}
15	8, 14	wceq 958	. . . 4 wff y = {x e. H~ | (t` x) = 0}
16	6, 15	wa 223	. . 3 wff (t:H~-->CC /\ y = {x e. H~ | (t` x) = 0})
17	16, 4, 7	copab 2671	. 2 class {<.t, y>. | (t:H~-->CC /\ y = {x e. H~ | (t` x) = 0})}
18	1, 17	wceq 958	1 wff null = {<.t, y>. | (t:H~-->CC /\ y = {x e. H~ | (t` x) = 0})}

This definition is referenced by:  nlfnvalt 9803

Copyright terms: Public domain