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 )