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 ⊢ S ∈ BndLinOp
nmoptri.2 ⊢ T ∈ BndLinOp
Assertion nmoptrii ⊢ norm op ⁡ S + op T ≤ norm op ⁡ S + norm op ⁡ T

Proof

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