Theorem nmop0h

Description: The norm of any operator on the trivial Hilbert space is zero. (This is the reason we need ~H =/= 0H in nmopun .) (Contributed by NM, 24-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmop0h	$$⊢\left(\mathscr{H}=0_{\mathscr{H}}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to {norm}_{\mathrm{op}}\left(T\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		df-ch0	$$⊢0_{\mathscr{H}}=\left\{0_{ℎ}\right\}$$
2	1	eqeq2i	$$⊢\mathscr{H}=0_{\mathscr{H}}\leftrightarrow \mathscr{H}=\left\{0_{ℎ}\right\}$$
3		feq3	$$⊢\mathscr{H}=\left\{0_{ℎ}\right\}\to \left(T:\mathscr{H}⟶\mathscr{H}\leftrightarrow T:\mathscr{H}⟶\left\{0_{ℎ}\right\}\right)$$
4	2 3	sylbi	$$⊢\mathscr{H}=0_{\mathscr{H}}\to \left(T:\mathscr{H}⟶\mathscr{H}\leftrightarrow T:\mathscr{H}⟶\left\{0_{ℎ}\right\}\right)$$
5		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
6	5	elexi	$$⊢0_{ℎ}\in \mathrm{V}$$
7	6	fconst2	$$⊢T:\mathscr{H}⟶\left\{0_{ℎ}\right\}\leftrightarrow T=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
8		df0op2	$$⊢0_{\mathrm{hop}}=\mathscr{H}\times 0_{\mathscr{H}}$$
9	1	xpeq2i	$$⊢\mathscr{H}\times 0_{\mathscr{H}}=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
10	8 9	eqtri	$$⊢0_{\mathrm{hop}}=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
11	10	eqeq2i	$$⊢T=0_{\mathrm{hop}}\leftrightarrow T=\mathscr{H}\times \left\{0_{ℎ}\right\}$$
12	7 11	bitr4i	$$⊢T:\mathscr{H}⟶\left\{0_{ℎ}\right\}\leftrightarrow T=0_{\mathrm{hop}}$$
13	4 12	bitrdi	$$⊢\mathscr{H}=0_{\mathscr{H}}\to \left(T:\mathscr{H}⟶\mathscr{H}\leftrightarrow T=0_{\mathrm{hop}}\right)$$
14	13	biimpa	$$⊢\left(\mathscr{H}=0_{\mathscr{H}}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to T=0_{\mathrm{hop}}$$
15	14	fveq2d	$$⊢\left(\mathscr{H}=0_{\mathscr{H}}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to {norm}_{\mathrm{op}}\left(T\right)={norm}_{\mathrm{op}}\left(0_{\mathrm{hop}}\right)$$
16		nmop0	$$⊢{norm}_{\mathrm{op}}\left(0_{\mathrm{hop}}\right)=0$$
17	15 16	eqtrdi	$$⊢\left(\mathscr{H}=0_{\mathscr{H}}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to {norm}_{\mathrm{op}}\left(T\right)=0$$