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 )