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 ⊢ norm op = t ∈ ℋ ℋ ⟼ sup x | ∃ z ∈ ℋ norm ℎ ⁡ z ≤ 1 ∧ x = norm ℎ ⁡ t ⁡ z ℝ * <

Detailed syntax breakdown

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