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

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 ⊢ T ∈ BndLinOp
2 adjbdln ⊢ T ∈ BndLinOp → adj h ⁡ T ∈ BndLinOp
3 1 2 ax-mp ⊢ adj h ⁡ T ∈ BndLinOp
4 3 nmopcoadji ⊢ norm op ⁡ adj h ⁡ adj h ⁡ T ∘ adj h ⁡ T = norm op ⁡ adj h ⁡ T 2
5 bdopadj ⊢ T ∈ BndLinOp → T ∈ dom ⁡ adj h
6 1 5 ax-mp ⊢ T ∈ dom ⁡ adj h
7 adjadj ⊢ T ∈ dom ⁡ adj h → adj h ⁡ adj h ⁡ T = T
8 6 7 ax-mp ⊢ adj h ⁡ adj h ⁡ T = T
9 8 coeq1i ⊢ adj h ⁡ adj h ⁡ T ∘ adj h ⁡ T = T ∘ adj h ⁡ T
10 9 fveq2i ⊢ norm op ⁡ adj h ⁡ adj h ⁡ T ∘ adj h ⁡ T = norm op ⁡ T ∘ adj h ⁡ T
11 1 nmopadji ⊢ norm op ⁡ adj h ⁡ T = norm op ⁡ T
12 11 oveq1i ⊢ norm op ⁡ adj h ⁡ T 2 = norm op ⁡ T 2
13 4 10 12 3eqtr3i ⊢ norm op ⁡ T ∘ adj h ⁡ T = norm op ⁡ T 2