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

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

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 ⊢ 𝑇 ∈ BndLinOp
2 adjbdln ⊢ ( 𝑇 ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) ∈ BndLinOp )
3 1 2 ax-mp ⊢ ( adjℎ ‘ 𝑇 ) ∈ BndLinOp
4 3 nmopcoadji ⊢ ( normop ‘ ( ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) ∘ ( adjℎ ‘ 𝑇 ) ) ) = ( ( normop ‘ ( adjℎ ‘ 𝑇 ) ) ↑ 2 )
5 bdopadj ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ )
6 1 5 ax-mp ⊢ 𝑇 ∈ dom adjℎ
7 adjadj ⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) = 𝑇 )
8 6 7 ax-mp ⊢ ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) = 𝑇
9 8 coeq1i ⊢ ( ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) ∘ ( adjℎ ‘ 𝑇 ) ) = ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) )
10 9 fveq2i ⊢ ( normop ‘ ( ( adjℎ ‘ ( adjℎ ‘ 𝑇 ) ) ∘ ( adjℎ ‘ 𝑇 ) ) ) = ( normop ‘ ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) )
11 1 nmopadji ⊢ ( normop ‘ ( adjℎ ‘ 𝑇 ) ) = ( normop ‘ 𝑇 )
12 11 oveq1i ⊢ ( ( normop ‘ ( adjℎ ‘ 𝑇 ) ) ↑ 2 ) = ( ( normop ‘ 𝑇 ) ↑ 2 )
13 4 10 12 3eqtr3i ⊢ ( normop ‘ ( 𝑇 ∘ ( adjℎ ‘ 𝑇 ) ) ) = ( ( normop ‘ 𝑇 ) ↑ 2 )