Metamath Proof Explorer

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 ${⊢}{norm}_{\mathrm{op}}=\left({t}\in \left({ℋ}^{ℋ}\right)⟼sup\left(\left\{{x}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {x}={norm}_{ℎ}\left({t}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnop ${class}{norm}_{\mathrm{op}}$
1 vt ${setvar}{t}$
2 chba ${class}ℋ$
3 cmap ${class}{↑}_{𝑚}$
4 2 2 3 co ${class}\left({ℋ}^{ℋ}\right)$
5 vx ${setvar}{x}$
6 vz ${setvar}{z}$
7 cno ${class}{norm}_{ℎ}$
8 6 cv ${setvar}{z}$
9 8 7 cfv ${class}{norm}_{ℎ}\left({z}\right)$
10 cle ${class}\le$
11 c1 ${class}1$
12 9 11 10 wbr ${wff}{norm}_{ℎ}\left({z}\right)\le 1$
13 5 cv ${setvar}{x}$
14 1 cv ${setvar}{t}$
15 8 14 cfv ${class}{t}\left({z}\right)$
16 15 7 cfv ${class}{norm}_{ℎ}\left({t}\left({z}\right)\right)$
17 13 16 wceq ${wff}{x}={norm}_{ℎ}\left({t}\left({z}\right)\right)$
18 12 17 wa ${wff}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {x}={norm}_{ℎ}\left({t}\left({z}\right)\right)\right)$
19 18 6 2 wrex ${wff}\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {x}={norm}_{ℎ}\left({t}\left({z}\right)\right)\right)$
20 19 5 cab ${class}\left\{{x}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {x}={norm}_{ℎ}\left({t}\left({z}\right)\right)\right)\right\}$
21 cxr ${class}{ℝ}^{*}$
22 clt ${class}<$
23 20 21 22 csup ${class}sup\left(\left\{{x}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {x}={norm}_{ℎ}\left({t}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
24 1 4 23 cmpt ${class}\left({t}\in \left({ℋ}^{ℋ}\right)⟼sup\left(\left\{{x}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {x}={norm}_{ℎ}\left({t}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$
25 0 24 wceq ${wff}{norm}_{\mathrm{op}}=\left({t}\in \left({ℋ}^{ℋ}\right)⟼sup\left(\left\{{x}|\exists {z}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({z}\right)\le 1\wedge {x}={norm}_{ℎ}\left({t}\left({z}\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$