Metamath Proof Explorer

Theorem nmopadji

Description: Property of the norm of an adjoint. Theorem 3.11(v) of Beran p. 106. (Contributed by NM, 22-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopadjle.1 
|- T e. BndLinOp
Assertion nmopadji 
|- ( normop ` ( adjh ` T ) ) = ( normop ` T )

Proof

Step Hyp Ref Expression
1 nmopadjle.1 
 |-  T e. BndLinOp
2 1 nmopadjlem 
 |-  ( normop ` ( adjh ` T ) ) <_ ( normop ` T )
3 bdopadj 
 |-  ( T e. BndLinOp -> T e. dom adjh )
4 1 3 ax-mp 
 |-  T e. dom adjh
5 adjadj 
 |-  ( T e. dom adjh -> ( adjh ` ( adjh ` T ) ) = T )
6 4 5 ax-mp 
 |-  ( adjh ` ( adjh ` T ) ) = T
7 6 fveq2i 
 |-  ( normop ` ( adjh ` ( adjh ` T ) ) ) = ( normop ` T )
8 adjbdln 
 |-  ( T e. BndLinOp -> ( adjh ` T ) e. BndLinOp )
9 1 8 ax-mp 
 |-  ( adjh ` T ) e. BndLinOp
10 9 nmopadjlem 
 |-  ( normop ` ( adjh ` ( adjh ` T ) ) ) <_ ( normop ` ( adjh ` T ) )
11 7 10 eqbrtrri 
 |-  ( normop ` T ) <_ ( normop ` ( adjh ` T ) )
12 nmopre 
 |-  ( ( adjh ` T ) e. BndLinOp -> ( normop ` ( adjh ` T ) ) e. RR )
13 9 12 ax-mp 
 |-  ( normop ` ( adjh ` T ) ) e. RR
14 nmopre 
 |-  ( T e. BndLinOp -> ( normop ` T ) e. RR )
15 1 14 ax-mp 
 |-  ( normop ` T ) e. RR
16 13 15 letri3i 
 |-  ( ( normop ` ( adjh ` T ) ) = ( normop ` T ) <-> ( ( normop ` ( adjh ` T ) ) <_ ( normop ` T ) /\ ( normop ` T ) <_ ( normop ` ( adjh ` T ) ) ) )
17 2 11 16 mpbir2an 
 |-  ( normop ` ( adjh ` T ) ) = ( normop ` T )