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

Metamath Proof Explorer

Theorem nmoptrii

Description: Triangle 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 nmoptrii ( normop ‘ ( 𝑆 +op 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 nmoptri.1 ⊢ 𝑆 ∈ BndLinOp
2 nmoptri.2 ⊢ 𝑇 ∈ BndLinOp
3 bdopf ⊢ ( 𝑆 ∈ BndLinOp → 𝑆 : ℋ ⟶ ℋ )
4 1 3 ax-mp ⊢ 𝑆 : ℋ ⟶ ℋ
5 bdopf ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
6 2 5 ax-mp ⊢ 𝑇 : ℋ ⟶ ℋ
7 4 6 hoaddcli ⊢ ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ
8 nmopre ⊢ ( 𝑆 ∈ BndLinOp → ( normop ‘ 𝑆 ) ∈ ℝ )
9 1 8 ax-mp ⊢ ( normop ‘ 𝑆 ) ∈ ℝ
10 nmopre ⊢ ( 𝑇 ∈ BndLinOp → ( normop ‘ 𝑇 ) ∈ ℝ )
11 2 10 ax-mp ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
12 9 11 readdcli ⊢ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ∈ ℝ
13 12 rexri ⊢ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ∈ ℝ*
14 nmopub ⊢ ( ( ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ ∧ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ∈ ℝ* ) → ( ( normop ‘ ( 𝑆 +op 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ) ) )
15 7 13 14 mp2an ⊢ ( ( normop ‘ ( 𝑆 +op 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ) )
16 4 6 hoscli ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ∈ ℋ )
17 normcl ⊢ ( ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ )
18 16 17 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ )
19 18 adantr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) ∈ ℝ )
20 4 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
21 normcl ⊢ ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ∈ ℝ )
22 20 21 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ∈ ℝ )
23 6 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
24 normcl ⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
25 23 24 syl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
26 22 25 readdcld ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
27 26 adantr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
28 12 a1i ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ∈ ℝ )
29 hosval ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
30 4 6 29 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
31 30 fveq2d ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) = ( normℎ ‘ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
32 norm-ii ⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( normℎ ‘ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
33 20 23 32 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
34 31 33 eqbrtrd ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
35 34 adantr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
36 nmoplb ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑆 ) )
37 4 36 mp3an1 ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑆 ) )
38 nmoplb ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) )
39 6 38 mp3an1 ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) )
40 le2add ⊢ ( ( ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ∈ ℝ ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) ∧ ( ( normop ‘ 𝑆 ) ∈ ℝ ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) ) → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑆 ) ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ) )
41 9 11 40 mpanr12 ⊢ ( ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ∈ ℝ ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑆 ) ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ) )
42 22 25 41 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑆 ) ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ) )
43 42 adantr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑆 ) ∧ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( normop ‘ 𝑇 ) ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ) )
44 37 39 43 mp2and ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝑥 ) ) + ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) )
45 19 27 28 35 44 letrd ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) )
46 45 ex ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) ) ) )
47 15 46 mprgbir ⊢ ( normop ‘ ( 𝑆 +op 𝑇 ) ) ≤ ( ( normop ‘ 𝑆 ) + ( normop ‘ 𝑇 ) )