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 
|- T e. BndLinOp
Assertion nmopcoadj0i 
|- ( ( T o. ( adjh ` T ) ) = 0hop <-> T = 0hop )

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 
 |-  T e. BndLinOp
2 1 nmopcoadj2i 
 |-  ( normop ` ( T o. ( adjh ` T ) ) ) = ( ( normop ` T ) ^ 2 )
3 2 eqeq1i 
 |-  ( ( normop ` ( T o. ( adjh ` T ) ) ) = 0 <-> ( ( normop ` T ) ^ 2 ) = 0 )
4 nmopre 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )
5 1 4 ax-mp 
 |-  ( normop ` T ) e. RR
6 5 recni 
 |-  ( normop ` T ) e. CC
7 6 sqeq0i 
 |-  ( ( ( normop ` T ) ^ 2 ) = 0 <-> ( normop ` T ) = 0 )
8 3 7 bitri 
 |-  ( ( normop ` ( T o. ( adjh ` T ) ) ) = 0 <-> ( normop ` T ) = 0 )
9 bdopln 
 |-  ( T e. BndLinOp -> T e. LinOp )
10 1 9 ax-mp 
 |-  T e. LinOp
11 adjbdln 
 |-  ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )
12 1 11 ax-mp 
 |-  ( adjh ` T ) e. BndLinOp
13 bdopln 
 |-  ( ( adjh ` T ) e. BndLinOp -> ( adjh ` T ) e. LinOp )
14 12 13 ax-mp 
 |-  ( adjh ` T ) e. LinOp
15 10 14 lnopcoi 
 |-  ( T o. ( adjh ` T ) ) e. LinOp
16 15 nmlnop0iHIL 
 |-  ( ( normop ` ( T o. ( adjh ` T ) ) ) = 0 <-> ( T o. ( adjh ` T ) ) = 0hop )
17 10 nmlnop0iHIL 
 |-  ( ( normop ` T ) = 0 <-> T = 0hop )
18 8 16 17 3bitr3i 
 |-  ( ( T o. ( adjh ` T ) ) = 0hop <-> T = 0hop )