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 TBndLinOp
Assertion nmopcoadj2i normopTadjhT=normopT2

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 TBndLinOp
2 adjbdln TBndLinOpadjhTBndLinOp
3 1 2 ax-mp adjhTBndLinOp
4 3 nmopcoadji normopadjhadjhTadjhT=normopadjhT2
5 bdopadj TBndLinOpTdomadjh
6 1 5 ax-mp Tdomadjh
7 adjadj TdomadjhadjhadjhT=T
8 6 7 ax-mp adjhadjhT=T
9 8 coeq1i adjhadjhTadjhT=TadjhT
10 9 fveq2i normopadjhadjhTadjhT=normopTadjhT
11 1 nmopadji normopadjhT=normopT
12 11 oveq1i normopadjhT2=normopT2
13 4 10 12 3eqtr3i normopTadjhT=normopT2