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 )