Theorem nmopcoadj2i

Description: The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of Beran p. 106. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nmopcoadj.1	|- T e. BndLinOp
Assertion	nmopcoadj2i	|- ( normop ` ( T o. ( adjh ` T ) ) ) = ( ( normop ` T ) ^ 2 )

Proof

Step	Hyp	Ref	Expression
1		nmopcoadj.1	|- T e. BndLinOp
2		adjbdln	|- ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )
3	1 2	ax-mp	|- ( adjh ` T ) e. BndLinOp
4	3	nmopcoadji	|- ( normop ` ( ( adjh ` ( adjh ` T ) ) o. ( adjh ` T ) ) ) = ( ( normop ` ( adjh ` T ) ) ^ 2 )
5		bdopadj	|- ( T e. BndLinOp -> T e. dom adjh )
6	1 5	ax-mp	|- T e. dom adjh
7		adjadj	|- ( T e. dom adjh -> ( adjh ` ( adjh ` T ) ) = T )
8	6 7	ax-mp	|- ( adjh ` ( adjh ` T ) ) = T
9	8	coeq1i	|- ( ( adjh ` ( adjh ` T ) ) o. ( adjh ` T ) ) = ( T o. ( adjh ` T ) )
10	9	fveq2i	|- ( normop ` ( ( adjh ` ( adjh ` T ) ) o. ( adjh ` T ) ) ) = ( normop ` ( T o. ( adjh ` T ) ) )
11	1	nmopadji	|- ( normop ` ( adjh ` T ) ) = ( normop ` T )
12	11	oveq1i	|- ( ( normop ` ( adjh ` T ) ) ^ 2 ) = ( ( normop ` T ) ^ 2 )
13	4 10 12	3eqtr3i	|- ( normop ` ( T o. ( adjh ` T ) ) ) = ( ( normop ` T ) ^ 2 )