Definition df-nmfn 9711

Description: Define the norm of a Hilbert space functional.

Assertion

Ref	Expression
df-nmfn	⊢ normfn = {⟨t, y⟩∣(t: ℋ –→ℂ ⋀ y = sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (abs ‘(t ‘z)))}, ℝ*, < ))}

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-nmfn

Step	Hyp	Ref	Expression
1		cnmf 8759	. 2 class normfn
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		vz	. . . . . . . . . . . 12 set z
10	9	cv 953	. . . . . . . . . . 11 class z
11		cno 8733	. . . . . . . . . . 11 class normh
12	10, 11	cfv 3177	. . . . . . . . . 10 class (normh ‘z)
13		c1 5215	. . . . . . . . . 10 class 1
14		cle 5275	. . . . . . . . . 10 class ≤
15	12, 13, 14	wbr 2614	. . . . . . . . 9 wff (normh ‘z) ≤ 1
16		vx	. . . . . . . . . . 11 set x
17	16	cv 953	. . . . . . . . . 10 class x
18	10, 5	cfv 3177	. . . . . . . . . . 11 class (t ‘z)
19		cabs 6689	. . . . . . . . . . 11 class abs
20	18, 19	cfv 3177	. . . . . . . . . 10 class (abs ‘(t ‘z))
21	17, 20	wceq 954	. . . . . . . . 9 wff x = (abs ‘(t ‘z))
22	15, 21	wa 223	. . . . . . . 8 wff ((normh ‘z) ≤ 1 ⋀ x = (abs ‘(t ‘z)))
23	22, 9, 2	wrex 1643	. . . . . . 7 wff ∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (abs ‘(t ‘z)))
24	23, 16	cab 1461	. . . . . 6 class {x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (abs ‘(t ‘z)))}
25		cxr 5465	. . . . . 6 class ℝ*
26		clt 5466	. . . . . 6 class <
27	24, 25, 26	csup 4553	. . . . 5 class sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (abs ‘(t ‘z)))}, ℝ*, < )
28	8, 27	wceq 954	. . . 4 wff y = sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (abs ‘(t ‘z)))}, ℝ*, < )
29	6, 28	wa 223	. . 3 wff (t: ℋ –→ℂ ⋀ y = sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (abs ‘(t ‘z)))}, ℝ*, < ))
30	29, 4, 7	copab 2661	. 2 class {⟨t, y⟩∣(t: ℋ –→ℂ ⋀ y = sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (abs ‘(t ‘z)))}, ℝ*, < ))}
31	1, 30	wceq 954	1 wff normfn = {⟨t, y⟩∣(t: ℋ –→ℂ ⋀ y = sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (abs ‘(t ‘z)))}, ℝ*, < ))}

This definition is referenced by:  nmfnvalt 9743

Copyright terms: Public domain