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 ‘ 𝑇 )