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 TBndLinOp
Assertion nmopadji normopadjhT=normopT

Proof

Step Hyp Ref Expression
1 nmopadjle.1 TBndLinOp
2 1 nmopadjlem normopadjhTnormopT
3 bdopadj TBndLinOpTdomadjh
4 1 3 ax-mp Tdomadjh
5 adjadj TdomadjhadjhadjhT=T
6 4 5 ax-mp adjhadjhT=T
7 6 fveq2i normopadjhadjhT=normopT
8 adjbdln TBndLinOpadjhTBndLinOp
9 1 8 ax-mp adjhTBndLinOp
10 9 nmopadjlem normopadjhadjhTnormopadjhT
11 7 10 eqbrtrri normopTnormopadjhT
12 nmopre adjhTBndLinOpnormopadjhT
13 9 12 ax-mp normopadjhT
14 nmopre TBndLinOpnormopT
15 1 14 ax-mp normopT
16 13 15 letri3i normopadjhT=normopTnormopadjhTnormopTnormopTnormopadjhT
17 2 11 16 mpbir2an normopadjhT=normopT