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 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )