Theorem adjeq0

Description: An operator is zero iff its adjoint is zero. Theorem 3.11(i) of Beran p. 106. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adjeq0	$$⊢T=0_{\mathrm{hop}}\leftrightarrow {adj}_h\left(T\right)=0_{\mathrm{hop}}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢T=0_{\mathrm{hop}}\to {adj}_h\left(T\right)={adj}_h\left(0_{\mathrm{hop}}\right)$$
2		adj0	$$⊢{adj}_h\left(0_{\mathrm{hop}}\right)=0_{\mathrm{hop}}$$
3	1 2	eqtrdi	$$⊢T=0_{\mathrm{hop}}\to {adj}_h\left(T\right)=0_{\mathrm{hop}}$$
4		fveq2	$$⊢{adj}_h\left(T\right)=0_{\mathrm{hop}}\to {adj}_h\left({adj}_h\left(T\right)\right)={adj}_h\left(0_{\mathrm{hop}}\right)$$
5		bdopssadj	$$⊢\mathrm{BndLinOp}\subseteq \mathrm{dom}{adj}_h$$
6		0bdop	$$⊢0_{\mathrm{hop}}\in \mathrm{BndLinOp}$$
7	5 6	sselii	$$⊢0_{\mathrm{hop}}\in \mathrm{dom}{adj}_h$$
8		eleq1	$$⊢{adj}_h\left(T\right)=0_{\mathrm{hop}}\to \left({adj}_h\left(T\right)\in \mathrm{dom}{adj}_h\leftrightarrow 0_{\mathrm{hop}}\in \mathrm{dom}{adj}_h\right)$$
9	7 8	mpbiri	$$⊢{adj}_h\left(T\right)=0_{\mathrm{hop}}\to {adj}_h\left(T\right)\in \mathrm{dom}{adj}_h$$
10		dmadjrnb	$$⊢T\in \mathrm{dom}{adj}_h\leftrightarrow {adj}_h\left(T\right)\in \mathrm{dom}{adj}_h$$
11	9 10	sylibr	$$⊢{adj}_h\left(T\right)=0_{\mathrm{hop}}\to T\in \mathrm{dom}{adj}_h$$
12		adjadj	$$⊢T\in \mathrm{dom}{adj}_h\to {adj}_h\left({adj}_h\left(T\right)\right)=T$$
13	11 12	syl	$$⊢{adj}_h\left(T\right)=0_{\mathrm{hop}}\to {adj}_h\left({adj}_h\left(T\right)\right)=T$$
14	2	a1i	$$⊢{adj}_h\left(T\right)=0_{\mathrm{hop}}\to {adj}_h\left(0_{\mathrm{hop}}\right)=0_{\mathrm{hop}}$$
15	4 13 14	3eqtr3d	$$⊢{adj}_h\left(T\right)=0_{\mathrm{hop}}\to T=0_{\mathrm{hop}}$$
16	3 15	impbii	$$⊢T=0_{\mathrm{hop}}\leftrightarrow {adj}_h\left(T\right)=0_{\mathrm{hop}}$$