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

Detailed syntax breakdown

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