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 ∈ BndLinOp
Assertion nmopadji ⊢ norm op ⁡ adj h ⁡ T = norm op ⁡ T

Proof

Step Hyp Ref Expression
1 nmopadjle.1 ⊢ T ∈ BndLinOp
2 1 nmopadjlem ⊢ norm op ⁡ adj h ⁡ T ≤ norm op ⁡ T
3 bdopadj ⊢ T ∈ BndLinOp → T ∈ dom ⁡ adj h
4 1 3 ax-mp ⊢ T ∈ dom ⁡ adj h
5 adjadj ⊢ T ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ T = T
6 4 5 ax-mp ⊢ adj h ⁡ adj h ⁡ T = T
7 6 fveq2i ⊢ norm op ⁡ adj h ⁡ adj h ⁡ T = norm op ⁡ T
8 adjbdln ⊢ T ∈ BndLinOp → adj h ⁡ T ∈ BndLinOp
9 1 8 ax-mp ⊢ adj h ⁡ T ∈ BndLinOp
10 9 nmopadjlem ⊢ norm op ⁡ adj h ⁡ adj h ⁡ T ≤ norm op ⁡ adj h ⁡ T
11 7 10 eqbrtrri ⊢ norm op ⁡ T ≤ norm op ⁡ adj h ⁡ T
12 nmopre ⊢ adj h ⁡ T ∈ BndLinOp → norm op ⁡ adj h ⁡ T ∈ ℝ
13 9 12 ax-mp ⊢ norm op ⁡ adj h ⁡ T ∈ ℝ
14 nmopre ⊢ T ∈ BndLinOp → norm op ⁡ T ∈ ℝ
15 1 14 ax-mp ⊢ norm op ⁡ T ∈ ℝ
16 13 15 letri3i ⊢ norm op ⁡ adj h ⁡ T = norm op ⁡ T ↔ norm op ⁡ adj h ⁡ T ≤ norm op ⁡ T ∧ norm op ⁡ T ≤ norm op ⁡ adj h ⁡ T
17 2 11 16 mpbir2an ⊢ norm op ⁡ adj h ⁡ T = norm op ⁡ T