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 )