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	⊢ ( 𝑇 = 0hop ↔ ( adjℎ ‘ 𝑇 ) = 0hop )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑇 = 0hop → ( adjℎ ‘ 𝑇 ) = ( adjℎ ‘ 0hop ) )
2		adj0	⊢ ( adjℎ ‘ 0hop ) = 0hop
3	1 2	eqtrdi	⊢ ( 𝑇 = 0hop → ( adjℎ ‘ 𝑇 ) = 0hop )
4		fveq2	⊢ ( ( adjℎ ‘ 𝑇 ) = 0hop → ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) = ( adjℎ ‘ 0hop ) )
5		bdopssadj	⊢ BndLinOp ⊆ dom adjℎ
6		0bdop	⊢ 0hop ∈ BndLinOp
7	5 6	sselii	⊢ 0hop ∈ dom adjℎ
8		eleq1	⊢ ( ( adjℎ ‘ 𝑇 ) = 0hop → ( ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ ↔ 0hop ∈ dom adjℎ ) )
9	7 8	mpbiri	⊢ ( ( adjℎ ‘ 𝑇 ) = 0hop → ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
10		dmadjrnb	⊢ ( 𝑇 ∈ dom adjℎ ↔ ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
11	9 10	sylibr	⊢ ( ( adjℎ ‘ 𝑇 ) = 0hop → 𝑇 ∈ dom adjℎ )
12		adjadj	⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) = 𝑇 )
13	11 12	syl	⊢ ( ( adjℎ ‘ 𝑇 ) = 0hop → ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) = 𝑇 )
14	2	a1i	⊢ ( ( adjℎ ‘ 𝑇 ) = 0hop → ( adjℎ ‘ 0hop ) = 0hop )
15	4 13 14	3eqtr3d	⊢ ( ( adjℎ ‘ 𝑇 ) = 0hop → 𝑇 = 0hop )
16	3 15	impbii	⊢ ( 𝑇 = 0hop ↔ ( adjℎ ‘ 𝑇 ) = 0hop )