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 | |
|
Assertion | nmopadji | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmopadjle.1 | |
|
2 | 1 | nmopadjlem | |
3 | bdopadj | |
|
4 | 1 3 | ax-mp | |
5 | adjadj | |
|
6 | 4 5 | ax-mp | |
7 | 6 | fveq2i | |
8 | adjbdln | |
|
9 | 1 8 | ax-mp | |
10 | 9 | nmopadjlem | |
11 | 7 10 | eqbrtrri | |
12 | nmopre | |
|
13 | 9 12 | ax-mp | |
14 | nmopre | |
|
15 | 1 14 | ax-mp | |
16 | 13 15 | letri3i | |
17 | 2 11 16 | mpbir2an | |