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