Definition df-nlfn 10052

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 9096	. 2 class null
2		chil 9063	. . . . 5 class H~
3		cc 5386	. . . . 5 class CC
4		vt	. . . . . 6 set t
5	4	cv 991	. . . . 5 class t
6	2, 3, 5	wf 3259	. . . 4 wff t:H~-->CC
7		vy	. . . . . 6 set y
8	7	cv 991	. . . . 5 class y
9		vx	. . . . . . . . 9 set x
10	9	cv 991	. . . . . . . 8 class x
11	10, 5	cfv 3263	. . . . . . 7 class (t` x)
12		cc0 5388	. . . . . . 7 class 0
13	11, 12	wceq 992	. . . . . 6 wff (t` x) = 0
14	13, 9, 2	crab 1694	. . . . 5 class {x e. H~ | (t` x) = 0}
15	8, 14	wceq 992	. . . 4 wff y = {x e. H~ | (t` x) = 0}
16	6, 15	wa 221	. . 3 wff (t:H~-->CC /\ y = {x e. H~ | (t` x) = 0})
17	16, 4, 7	copab 2740	. 2 class {<.t, y>. | (t:H~-->CC /\ y = {x e. H~ | (t` x) = 0})}
18	1, 17	wceq 992	1 wff null = {<.t, y>. | (t:H~-->CC /\ y = {x e. H~ | (t` x) = 0})}

This definition is referenced by:  nlfnval 10088

Copyright terms: Public domain