Metamath Proof Explorer

Definition df-nmfn

Description: Define the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion df-nmfn ⊢ norm fn = t ∈ ℂ ℋ ⟼ sup x | ∃ z ∈ ℋ norm ℎ ⁡ z ≤ 1 ∧ x = t ⁡ z ℝ * <

Detailed syntax breakdown

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