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 = 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 eqtrdi ⊢ 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