Definition df-nmop 9682

Description: Define the norm of a Hilbert space operator.

Assertion

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

Distinct variable group:   x,t,y,z

Detailed syntax breakdown of Definition df-nmop

Step	Hyp	Ref	Expression
1		cnop 8753	. 2 class normop
2		chil 8727	. . . . 5 class ℋ
3		vt	. . . . . 6 set t
4	3	cv 952	. . . . 5 class t
5	2, 2, 4	wf 3168	. . . 4 wff t: ℋ –→ ℋ
6		vy	. . . . . 6 set y
7	6	cv 952	. . . . 5 class y
8		vz	. . . . . . . . . . . 12 set z
9	8	cv 952	. . . . . . . . . . 11 class z
10		cno 8733	. . . . . . . . . . 11 class normh
11	9, 10	cfv 3172	. . . . . . . . . 10 class (normh ‘z)
12		c1 5207	. . . . . . . . . 10 class 1
13		cle 5267	. . . . . . . . . 10 class ≤
14	11, 12, 13	wbr 2609	. . . . . . . . 9 wff (normh ‘z) ≤ 1
15		vx	. . . . . . . . . . 11 set x
16	15	cv 952	. . . . . . . . . 10 class x
17	9, 4	cfv 3172	. . . . . . . . . . 11 class (t ‘z)
18	17, 10	cfv 3172	. . . . . . . . . 10 class (normh ‘(t ‘z))
19	16, 18	wceq 953	. . . . . . . . 9 wff x = (normh ‘(t ‘z))
20	14, 19	wa 223	. . . . . . . 8 wff ((normh ‘z) ≤ 1 ⋀ x = (normh ‘(t ‘z)))
21	20, 8, 2	wrex 1638	. . . . . . 7 wff ∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (normh ‘(t ‘z)))
22	21, 15	cab 1456	. . . . . 6 class {x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (normh ‘(t ‘z)))}
23		cxr 5457	. . . . . 6 class ℝ*
24		clt 5458	. . . . . 6 class <
25	22, 23, 24	csup 4547	. . . . 5 class sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (normh ‘(t ‘z)))}, ℝ*, < )
26	7, 25	wceq 953	. . . 4 wff y = sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (normh ‘(t ‘z)))}, ℝ*, < )
27	5, 26	wa 223	. . 3 wff (t: ℋ –→ ℋ ⋀ y = sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (normh ‘(t ‘z)))}, ℝ*, < ))
28	27, 3, 6	copab 2656	. 2 class {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (normh ‘(t ‘z)))}, ℝ*, < ))}
29	1, 28	wceq 953	1 wff normop = {⟨t, y⟩∣(t: ℋ –→ ℋ ⋀ y = sup({x∣∃z ∈ ℋ ((normh ‘z) ≤ 1 ⋀ x = (normh ‘(t ‘z)))}, ℝ*, < ))}

This definition is referenced by:  nmopvalt 9699  hhnmo 9744

Copyright terms: Public domain