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 ( 𝑇 = 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 )