Theorem hhnmoi

Description: The norm of an operator in Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhnmo.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	hhnmo.2	$$⊢N=U{normOp}_{\mathrm{OLD}}U$$
Assertion	hhnmoi	$$⊢{norm}_{\mathrm{op}}=N$$

Proof

Step	Hyp	Ref	Expression
1		hhnmo.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		hhnmo.2	$$⊢N=U{normOp}_{\mathrm{OLD}}U$$
3		df-nmop	$$⊢{norm}_{\mathrm{op}}=\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼sup\left(\left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(t\left(y\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$$
4	1	hhnv	$$⊢U\in \mathrm{NrmCVec}$$
5	1	hhba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
6	1	hhnm	$$⊢{norm}_{ℎ}={norm}_{CV}\left(U\right)$$
7	5 5 6 6 2	nmoofval	$$⊢\left(U\in \mathrm{NrmCVec}\wedge U\in \mathrm{NrmCVec}\right)\to N=\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼sup\left(\left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(t\left(y\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$$
8	4 4 7	mp2an	$$⊢N=\left(t\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼sup\left(\left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x={norm}_{ℎ}\left(t\left(y\right)\right)\right)\right\},{ℝ}^{*},<\right)\right)$$
9	3 8	eqtr4i	$$⊢{norm}_{\mathrm{op}}=N$$