This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )