Metamath Proof Explorer

Definition df-nmop

Description: Define the norm of a Hilbert space operator. (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion df-nmop ⊢normop=t∈ℋℋ⟼supx|∃z∈ℋnormℎ⁡z≤1∧x=normℎ⁡t⁡zℝ*<

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnop classnormop
1 vt setvart
2 chba classℋ
3 cmap class↑𝑚
4 2 2 3 co classℋℋ
5 vx setvarx
6 vz setvarz
7 cno classnormℎ
8 6 cv setvarz
9 8 7 cfv classnormℎ⁡z
10 cle class≤
11 c1 class1
12 9 11 10 wbr wffnormℎ⁡z≤1
13 5 cv setvarx
14 1 cv setvart
15 8 14 cfv classt⁡z
16 15 7 cfv classnormℎ⁡t⁡z
17 13 16 wceq wffx=normℎ⁡t⁡z
18 12 17 wa wffnormℎ⁡z≤1∧x=normℎ⁡t⁡z
19 18 6 2 wrex wff∃z∈ℋnormℎ⁡z≤1∧x=normℎ⁡t⁡z
20 19 5 cab classx|∃z∈ℋnormℎ⁡z≤1∧x=normℎ⁡t⁡z
21 cxr classℝ*
22 clt class<
23 20 21 22 csup classsupx|∃z∈ℋnormℎ⁡z≤1∧x=normℎ⁡t⁡zℝ*<
24 1 4 23 cmpt classt∈ℋℋ⟼supx|∃z∈ℋnormℎ⁡z≤1∧x=normℎ⁡t⁡zℝ*<
25 0 24 wceq wffnormop=t∈ℋℋ⟼supx|∃z∈ℋnormℎ⁡z≤1∧x=normℎ⁡t⁡zℝ*<