Definition df-nlfn 9712

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

Assertion

Ref	Expression
df-nlfn	⊢ null = {⟨t, y⟩∣(t: ℋ –→ℂ ⋀ y = {x ∈ ℋ ∣(t ‘x) = 0})}

Distinct variable group:   x,t,y

Detailed syntax breakdown of Definition df-nlfn

Step	Hyp	Ref	Expression
1		cnl 8760	. 2 class null
2		chil 8727	. . . . 5 class ℋ
3		cc 5212	. . . . 5 class ℂ
4		vt	. . . . . 6 set t
5	4	cv 953	. . . . 5 class t
6	2, 3, 5	wf 3173	. . . 4 wff t: ℋ –→ℂ
7		vy	. . . . . 6 set y
8	7	cv 953	. . . . 5 class y
9		vx	. . . . . . . . 9 set x
10	9	cv 953	. . . . . . . 8 class x
11	10, 5	cfv 3177	. . . . . . 7 class (t ‘x)
12		cc0 5214	. . . . . . 7 class 0
13	11, 12	wceq 954	. . . . . 6 wff (t ‘x) = 0
14	13, 9, 2	crab 1645	. . . . 5 class {x ∈ ℋ ∣(t ‘x) = 0}
15	8, 14	wceq 954	. . . 4 wff y = {x ∈ ℋ ∣(t ‘x) = 0}
16	6, 15	wa 223	. . 3 wff (t: ℋ –→ℂ ⋀ y = {x ∈ ℋ ∣(t ‘x) = 0})
17	16, 4, 7	copab 2661	. 2 class {⟨t, y⟩∣(t: ℋ –→ℂ ⋀ y = {x ∈ ℋ ∣(t ‘x) = 0})}
18	1, 17	wceq 954	1 wff null = {⟨t, y⟩∣(t: ℋ –→ℂ ⋀ y = {x ∈ ℋ ∣(t ‘x) = 0})}

This definition is referenced by:  nlfnvalt 9748

Copyright terms: Public domain