Theorem nmoptri2i

Description: Triangle-type inequality for the norms of bounded linear operators. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmoptri.1	⊢ 𝑆 ∈ BndLinOp
	nmoptri.2	⊢ 𝑇 ∈ BndLinOp
Assertion	nmoptri2i	⊢ ( ( normop ‘ 𝑆 ) − ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ ( 𝑆 +op 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		nmoptri.1	⊢ 𝑆 ∈ BndLinOp
2		nmoptri.2	⊢ 𝑇 ∈ BndLinOp
3	1 2	bdophsi	⊢ ( 𝑆 +op 𝑇 ) ∈ BndLinOp
4		neg1cn	⊢ - 1 ∈ ℂ
5	2	bdophmi	⊢ ( - 1 ∈ ℂ → ( - 1 ·op 𝑇 ) ∈ BndLinOp )
6	4 5	ax-mp	⊢ ( - 1 ·op 𝑇 ) ∈ BndLinOp
7	3 6	nmoptrii	⊢ ( normop ‘ ( ( 𝑆 +op 𝑇 ) +op ( - 1 ·op 𝑇 ) ) ) ≤ ( ( normop ‘ ( 𝑆 +op 𝑇 ) ) + ( normop ‘ ( - 1 ·op 𝑇 ) ) )
8		bdopf	⊢ ( 𝑆 ∈ BndLinOp → 𝑆 : ℋ ⟶ ℋ )
9	1 8	ax-mp	⊢ 𝑆 : ℋ ⟶ ℋ
10		bdopf	⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
11	2 10	ax-mp	⊢ 𝑇 : ℋ ⟶ ℋ
12	9 11	hoaddcli	⊢ ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ
13	12 11	honegsubi	⊢ ( ( 𝑆 +op 𝑇 ) +op ( - 1 ·op 𝑇 ) ) = ( ( 𝑆 +op 𝑇 ) −op 𝑇 )
14	9 11	hopncani	⊢ ( ( 𝑆 +op 𝑇 ) −op 𝑇 ) = 𝑆
15	13 14	eqtri	⊢ ( ( 𝑆 +op 𝑇 ) +op ( - 1 ·op 𝑇 ) ) = 𝑆
16	15	fveq2i	⊢ ( normop ‘ ( ( 𝑆 +op 𝑇 ) +op ( - 1 ·op 𝑇 ) ) ) = ( normop ‘ 𝑆 )
17	11	nmopnegi	⊢ ( normop ‘ ( - 1 ·op 𝑇 ) ) = ( normop ‘ 𝑇 )
18	17	oveq2i	⊢ ( ( normop ‘ ( 𝑆 +op 𝑇 ) ) + ( normop ‘ ( - 1 ·op 𝑇 ) ) ) = ( ( normop ‘ ( 𝑆 +op 𝑇 ) ) + ( normop ‘ 𝑇 ) )
19	7 16 18	3brtr3i	⊢ ( normop ‘ 𝑆 ) ≤ ( ( normop ‘ ( 𝑆 +op 𝑇 ) ) + ( normop ‘ 𝑇 ) )
20		nmopre	⊢ ( 𝑆 ∈ BndLinOp → ( normop ‘ 𝑆 ) ∈ ℝ )
21	1 20	ax-mp	⊢ ( normop ‘ 𝑆 ) ∈ ℝ
22		nmopre	⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )
23	2 22	ax-mp	⊢ ( normop ‘ 𝑇 ) ∈ ℝ
24		nmopre	⊢ ( ( 𝑆 +op 𝑇 ) ∈ BndLinOp → ( normop ‘ ( 𝑆 +op 𝑇 ) ) ∈ ℝ )
25	3 24	ax-mp	⊢ ( normop ‘ ( 𝑆 +op 𝑇 ) ) ∈ ℝ
26	21 23 25	lesubaddi	⊢ ( ( ( normop ‘ 𝑆 ) − ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ ( 𝑆 +op 𝑇 ) ) ↔ ( normop ‘ 𝑆 ) ≤ ( ( normop ‘ ( 𝑆 +op 𝑇 ) ) + ( normop ‘ 𝑇 ) ) )
27	19 26	mpbir	⊢ ( ( normop ‘ 𝑆 ) − ( normop ‘ 𝑇 ) ) ≤ ( normop ‘ ( 𝑆 +op 𝑇 ) )