This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = 0hop <-> ( adjh ` T ) = 0hop )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( T = 0hop -> ( adjh ` T ) = ( adjh ` 0hop ) )
2 adj0 
 |-  ( adjh ` 0hop ) = 0hop
3 1 2 eqtrdi 
 |-  ( T = 0hop -> ( adjh ` T ) = 0hop )
4 fveq2 
 |-  ( ( adjh ` T ) = 0hop -> ( adjh ` ( adjh ` T ) ) = ( adjh ` 0hop ) )
5 bdopssadj 
 |-  BndLinOp C_ dom adjh
6 0bdop 
 |-  0hop e. BndLinOp
7 5 6 sselii 
 |-  0hop e. dom adjh
8 eleq1 
 |-  ( ( adjh ` T ) = 0hop -> ( ( adjh ` T ) e. dom adjh <-> 0hop e. dom adjh ) )
9 7 8 mpbiri 
 |-  ( ( adjh ` T ) = 0hop -> ( adjh ` T ) e. dom adjh )
10 dmadjrnb 
 |-  ( T e. dom adjh <-> ( adjh ` T ) e. dom adjh )
11 9 10 sylibr 
 |-  ( ( adjh ` T ) = 0hop -> T e. dom adjh )
12 adjadj 
 |-  ( T e. dom adjh -> ( adjh ` ( adjh ` T ) ) = T )
13 11 12 syl 
 |-  ( ( adjh ` T ) = 0hop -> ( adjh ` ( adjh ` T ) ) = T )
14 2 a1i 
 |-  ( ( adjh ` T ) = 0hop -> ( adjh ` 0hop ) = 0hop )
15 4 13 14 3eqtr3d 
 |-  ( ( adjh ` T ) = 0hop -> T = 0hop )
16 3 15 impbii 
 |-  ( T = 0hop <-> ( adjh ` T ) = 0hop )