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

Metamath Proof Explorer

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