Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  nmopcoadj0i Structured version   Visualization version   GIF version

 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.)
Hypothesis
Ref Expression
Assertion
Ref Expression

StepHypRef Expression
1 nmopcoadj.1 . . . . 5 𝑇 ∈ BndLinOp
32eqeq1i 2615 . . 3 ((normop‘(𝑇 ∘ (adj𝑇))) = 0 ↔ ((normop𝑇)↑2) = 0)
4 nmopre 28113 . . . . . 6 (𝑇 ∈ BndLinOp → (normop𝑇) ∈ ℝ)
51, 4ax-mp 5 . . . . 5 (normop𝑇) ∈ ℝ
65recni 9931 . . . 4 (normop𝑇) ∈ ℂ
76sqeq0i 12807 . . 3 (((normop𝑇)↑2) = 0 ↔ (normop𝑇) = 0)
83, 7bitri 263 . 2 ((normop‘(𝑇 ∘ (adj𝑇))) = 0 ↔ (normop𝑇) = 0)
9 bdopln 28104 . . . . 5 (𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp)
101, 9ax-mp 5 . . . 4 𝑇 ∈ LinOp
11 adjbdln 28326 . . . . . 6 (𝑇 ∈ BndLinOp → (adj𝑇) ∈ BndLinOp)
121, 11ax-mp 5 . . . . 5 (adj𝑇) ∈ BndLinOp
13 bdopln 28104 . . . . 5 ((adj𝑇) ∈ BndLinOp → (adj𝑇) ∈ LinOp)
1412, 13ax-mp 5 . . . 4 (adj𝑇) ∈ LinOp
1510, 14lnopcoi 28246 . . 3 (𝑇 ∘ (adj𝑇)) ∈ LinOp
1615nmlnop0iHIL 28239 . 2 ((normop‘(𝑇 ∘ (adj𝑇))) = 0 ↔ (𝑇 ∘ (adj𝑇)) = 0hop )
1710nmlnop0iHIL 28239 . 2 ((normop𝑇) = 0 ↔ 𝑇 = 0hop )
188, 16, 173bitr3i 289 1 ((𝑇 ∘ (adj𝑇)) = 0hop𝑇 = 0hop )