Theorem lnopco0i

Description: The composition of a linear operator with one whose norm is zero. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lnopco.1	$$⊢S\in \mathrm{LinOp}$$
	lnopco.2	$$⊢T\in \mathrm{LinOp}$$
Assertion	lnopco0i	$$⊢{norm}_{\mathrm{op}}\left(T\right)=0\to {norm}_{\mathrm{op}}\left(S\circ T\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		lnopco.1	$$⊢S\in \mathrm{LinOp}$$
2		lnopco.2	$$⊢T\in \mathrm{LinOp}$$
3		coeq2	$$⊢T=0_{\mathrm{hop}}\to S\circ T=S\circ 0_{\mathrm{hop}}$$
4		0lnop	$$⊢0_{\mathrm{hop}}\in \mathrm{LinOp}$$
5	1 4	lnopcoi	$$⊢S\circ 0_{\mathrm{hop}}\in \mathrm{LinOp}$$
6	5	lnopfi	$$⊢\left(S\circ 0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}$$
7		ffn	$$⊢\left(S\circ 0_{\mathrm{hop}}\right):\mathscr{H}⟶\mathscr{H}\to \left(S\circ 0_{\mathrm{hop}}\right)Fn\mathscr{H}$$
8	6 7	ax-mp	$$⊢\left(S\circ 0_{\mathrm{hop}}\right)Fn\mathscr{H}$$
9		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
10		ffn	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\to 0_{\mathrm{hop}}Fn\mathscr{H}$$
11	9 10	ax-mp	$$⊢0_{\mathrm{hop}}Fn\mathscr{H}$$
12		eqfnfv	$$⊢\left(\left(S\circ 0_{\mathrm{hop}}\right)Fn\mathscr{H}\wedge 0_{\mathrm{hop}}Fn\mathscr{H}\right)\to \left(S\circ 0_{\mathrm{hop}}=0_{\mathrm{hop}}\leftrightarrow \forall x\in \mathscr{H}\left(S\circ 0_{\mathrm{hop}}\right)\left(x\right)=0_{\mathrm{hop}}\left(x\right)\right)$$
13	8 11 12	mp2an	$$⊢S\circ 0_{\mathrm{hop}}=0_{\mathrm{hop}}\leftrightarrow \forall x\in \mathscr{H}\left(S\circ 0_{\mathrm{hop}}\right)\left(x\right)=0_{\mathrm{hop}}\left(x\right)$$
14		ho0val	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
15	14	fveq2d	$$⊢x\in \mathscr{H}\to S\left(0_{\mathrm{hop}}\left(x\right)\right)=S\left(0_{ℎ}\right)$$
16	1	lnop0i	$$⊢S\left(0_{ℎ}\right)=0_{ℎ}$$
17	15 16	eqtrdi	$$⊢x\in \mathscr{H}\to S\left(0_{\mathrm{hop}}\left(x\right)\right)=0_{ℎ}$$
18	1	lnopfi	$$⊢S:\mathscr{H}⟶\mathscr{H}$$
19	18 9	hocoi	$$⊢x\in \mathscr{H}\to \left(S\circ 0_{\mathrm{hop}}\right)\left(x\right)=S\left(0_{\mathrm{hop}}\left(x\right)\right)$$
20	17 19 14	3eqtr4d	$$⊢x\in \mathscr{H}\to \left(S\circ 0_{\mathrm{hop}}\right)\left(x\right)=0_{\mathrm{hop}}\left(x\right)$$
21	13 20	mprgbir	$$⊢S\circ 0_{\mathrm{hop}}=0_{\mathrm{hop}}$$
22	3 21	eqtrdi	$$⊢T=0_{\mathrm{hop}}\to S\circ T=0_{\mathrm{hop}}$$
23	2	nmlnop0iHIL	$$⊢{norm}_{\mathrm{op}}\left(T\right)=0\leftrightarrow T=0_{\mathrm{hop}}$$
24	1 2	lnopcoi	$$⊢S\circ T\in \mathrm{LinOp}$$
25	24	nmlnop0iHIL	$$⊢{norm}_{\mathrm{op}}\left(S\circ T\right)=0\leftrightarrow S\circ T=0_{\mathrm{hop}}$$
26	22 23 25	3imtr4i	$$⊢{norm}_{\mathrm{op}}\left(T\right)=0\to {norm}_{\mathrm{op}}\left(S\circ T\right)=0$$