Theorem nmopcoadj0i

Description: An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of Beran p. 106. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nmopcoadj.1	$$⊢T\in \mathrm{BndLinOp}$$
Assertion	nmopcoadj0i	$$⊢T\circ {adj}_h\left(T\right)=0_{\mathrm{hop}}\leftrightarrow T=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		nmopcoadj.1	$$⊢T\in \mathrm{BndLinOp}$$
2	1	nmopcoadj2i	$$⊢{norm}_{\mathrm{op}}\left(T\circ {adj}_h\left(T\right)\right)={{norm}_{\mathrm{op}}\left(T\right)}^2$$
3	2	eqeq1i	$$⊢{norm}_{\mathrm{op}}\left(T\circ {adj}_h\left(T\right)\right)=0\leftrightarrow {{norm}_{\mathrm{op}}\left(T\right)}^2=0$$
4		nmopre	$$⊢T\in \mathrm{BndLinOp}\to {norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
5	1 4	ax-mp	$$⊢{norm}_{\mathrm{op}}\left(T\right)\in ℝ$$
6	5	recni	$$⊢{norm}_{\mathrm{op}}\left(T\right)\in ℂ$$
7	6	sqeq0i	$$⊢{{norm}_{\mathrm{op}}\left(T\right)}^2=0\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)=0$$
8	3 7	bitri	$$⊢{norm}_{\mathrm{op}}\left(T\circ {adj}_h\left(T\right)\right)=0\leftrightarrow {norm}_{\mathrm{op}}\left(T\right)=0$$
9		bdopln	$$⊢T\in \mathrm{BndLinOp}\to T\in \mathrm{LinOp}$$
10	1 9	ax-mp	$$⊢T\in \mathrm{LinOp}$$
11		adjbdln	$$⊢T\in \mathrm{BndLinOp}\to {adj}_h\left(T\right)\in \mathrm{BndLinOp}$$
12	1 11	ax-mp	$$⊢{adj}_h\left(T\right)\in \mathrm{BndLinOp}$$
13		bdopln	$$⊢{adj}_h\left(T\right)\in \mathrm{BndLinOp}\to {adj}_h\left(T\right)\in \mathrm{LinOp}$$
14	12 13	ax-mp	$$⊢{adj}_h\left(T\right)\in \mathrm{LinOp}$$
15	10 14	lnopcoi	$$⊢T\circ {adj}_h\left(T\right)\in \mathrm{LinOp}$$
16	15	nmlnop0iHIL	$$⊢{norm}_{\mathrm{op}}\left(T\circ {adj}_h\left(T\right)\right)=0\leftrightarrow T\circ {adj}_h\left(T\right)=0_{\mathrm{hop}}$$
17	10	nmlnop0iHIL	$$⊢{norm}_{\mathrm{op}}\left(T\right)=0\leftrightarrow T=0_{\mathrm{hop}}$$
18	8 16 17	3bitr3i	$$⊢T\circ {adj}_h\left(T\right)=0_{\mathrm{hop}}\leftrightarrow T=0_{\mathrm{hop}}$$