This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 ∈ BndLinOp
Assertion nmopadji ( normop ‘ ( adjℎ ‘ 𝑇 ) ) = ( normop ‘ 𝑇 )

Proof

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