Metamath Proof Explorer


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 hop adj h T = 0 hop

Proof

Step Hyp Ref Expression
1 fveq2 T = 0 hop adj h T = adj h 0 hop
2 adj0 adj h 0 hop = 0 hop
3 1 2 syl6eq T = 0 hop adj h T = 0 hop
4 fveq2 adj h T = 0 hop adj h adj h T = adj h 0 hop
5 bdopssadj BndLinOp dom adj h
6 0bdop 0 hop BndLinOp
7 5 6 sselii 0 hop dom adj h
8 eleq1 adj h T = 0 hop adj h T dom adj h 0 hop dom adj h
9 7 8 mpbiri adj h T = 0 hop adj h T dom adj h
10 dmadjrnb T dom adj h adj h T dom adj h
11 9 10 sylibr adj h T = 0 hop T dom adj h
12 adjadj T dom adj h adj h adj h T = T
13 11 12 syl adj h T = 0 hop adj h adj h T = T
14 2 a1i adj h T = 0 hop adj h 0 hop = 0 hop
15 4 13 14 3eqtr3d adj h T = 0 hop T = 0 hop
16 3 15 impbii T = 0 hop adj h T = 0 hop