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

Step	Hyp	Ref	Expression
0		cnop	⊢ norm_op
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	⊢ norm_op = ( 𝑡 ∈ ( ℋ ↑_m ℋ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ℋ ( ( norm_ℎ ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( norm_ℎ ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ^* , < ) )

Metamath Proof Explorer