# Metamath Proof Explorer

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}}↔{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 syl6eq ${⊢}{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}↔{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}↔{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}}↔{adj}_{h}\left({T}\right)={0}_{\mathrm{hop}}$