This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 normfn = ( 𝑡 ∈ ( ℂ ↑m ℋ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnmf ⊢ normfn
1 vt ⊢ 𝑡
2 cc ⊢ ℂ
3 cmap ⊢ ↑m
4 chba ⊢ ℋ
5 2 4 3 co ⊢ ( ℂ ↑m ℋ )
6 vx ⊢ 𝑥
7 vz ⊢ 𝑧
8 cno ⊢ normℎ
9 7 cv ⊢ 𝑧
10 9 8 cfv ⊢ ( normℎ ‘ 𝑧 )
11 cle ⊢ ≤
12 c1 ⊢ 1
13 10 12 11 wbr ⊢ ( normℎ ‘ 𝑧 ) ≤ 1
14 6 cv ⊢ 𝑥
15 cabs ⊢ abs
16 1 cv ⊢ 𝑡
17 9 16 cfv ⊢ ( 𝑡 ‘ 𝑧 )
18 17 15 cfv ⊢ ( abs ‘ ( 𝑡 ‘ 𝑧 ) )
19 14 18 wceq ⊢ 𝑥 = ( abs ‘ ( 𝑡 ‘ 𝑧 ) )
20 13 19 wa ⊢ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑡 ‘ 𝑧 ) ) )
21 20 7 4 wrex ⊢ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑡 ‘ 𝑧 ) ) )
22 21 6 cab ⊢ { 𝑥 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑡 ‘ 𝑧 ) ) ) }
23 cxr ⊢ ℝ*
24 clt ⊢ <
25 22 23 24 csup ⊢ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < )
26 1 5 25 cmpt ⊢ ( 𝑡 ∈ ( ℂ ↑m ℋ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
27 0 26 wceq ⊢ normfn = ( 𝑡 ∈ ( ℂ ↑m ℋ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( abs ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )