Theorem ho0coi

Description: Composition of the zero operator and a Hilbert space operator. (Contributed by NM, 9-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hoaddid1.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	ho0coi	$$⊢0_{\mathrm{hop}}\circ T=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		hoaddid1.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2	1	ffvelrni	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
3		ho0val	$$⊢T\left(x\right)\in \mathscr{H}\to 0_{\mathrm{hop}}\left(T\left(x\right)\right)=0_{ℎ}$$
4	2 3	syl	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(T\left(x\right)\right)=0_{ℎ}$$
5		ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$
6	5 1	hocoi	$$⊢x\in \mathscr{H}\to \left(0_{\mathrm{hop}}\circ T\right)\left(x\right)=0_{\mathrm{hop}}\left(T\left(x\right)\right)$$
7		ho0val	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
8	4 6 7	3eqtr4d	$$⊢x\in \mathscr{H}\to \left(0_{\mathrm{hop}}\circ T\right)\left(x\right)=0_{\mathrm{hop}}\left(x\right)$$
9	8	rgen	$$⊢\forall x\in \mathscr{H}\left(0_{\mathrm{hop}}\circ T\right)\left(x\right)=0_{\mathrm{hop}}\left(x\right)$$
10	5 1	hocofi	$$⊢\left(0_{\mathrm{hop}}\circ T\right):\mathscr{H}⟶\mathscr{H}$$
11	10 5	hoeqi	$$⊢\forall x\in \mathscr{H}\left(0_{\mathrm{hop}}\circ T\right)\left(x\right)=0_{\mathrm{hop}}\left(x\right)\leftrightarrow 0_{\mathrm{hop}}\circ T=0_{\mathrm{hop}}$$
12	9 11	mpbi	$$⊢0_{\mathrm{hop}}\circ T=0_{\mathrm{hop}}$$