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

Metamath Proof Explorer

Theorem nmopcoadj0i

Description: An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of Beran p. 106. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopcoadj.1 ⊢ 𝑇 ∈ BndLinOp
Assertion nmopcoadj0i ( ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) = 0hop ↔ 𝑇 = 0hop )

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 ⊢ 𝑇 ∈ BndLinOp
2 1 nmopcoadj2i ⊢ ( normop ‘ ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) ) = ( ( normop ‘ 𝑇 ) ↑ 2 )
3 2 eqeq1i ⊢ ( ( normop ‘ ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) ) = 0 ↔ ( ( normop ‘ 𝑇 ) ↑ 2 ) = 0 )
4 nmopre ⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )
5 1 4 ax-mp ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
6 5 recni ⊢ ( normop ‘ 𝑇 ) ∈ ℂ
7 6 sqeq0i ⊢ ( ( ( normop ‘ 𝑇 ) ↑ 2 ) = 0 ↔ ( normop ‘ 𝑇 ) = 0 )
8 3 7 bitri ⊢ ( ( normop ‘ ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) ) = 0 ↔ ( normop ‘ 𝑇 ) = 0 )
9 bdopln ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )
10 1 9 ax-mp ⊢ 𝑇 ∈ LinOp
11 adjbdln ⊢ ( 𝑇 ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) ∈ BndLinOp )
12 1 11 ax-mp ⊢ ( adjℎ ‘ 𝑇 ) ∈ BndLinOp
13 bdopln ⊢ ( ( adjℎ ‘ 𝑇 ) ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) ∈ LinOp )
14 12 13 ax-mp ⊢ ( adjℎ ‘ 𝑇 ) ∈ LinOp
15 10 14 lnopcoi ⊢ ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) ∈ LinOp
16 15 nmlnop0iHIL ⊢ ( ( normop ‘ ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) ) = 0 ↔ ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) = 0hop )
17 10 nmlnop0iHIL ⊢ ( ( normop ‘ 𝑇 ) = 0 ↔ 𝑇 = 0hop )
18 8 16 17 3bitr3i ⊢ ( ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) = 0hop ↔ 𝑇 = 0hop )