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 ⊢normop⁡S+opT≤normop⁡S+normop⁡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+opT:ℋ⟶ℋ
8 nmopre ⊢S∈BndLinOp→normop⁡S∈ℝ
9 1 8 ax-mp ⊢normop⁡S∈ℝ
10 nmopre ⊢T∈BndLinOp→normop⁡T∈ℝ
11 2 10 ax-mp ⊢normop⁡T∈ℝ
12 9 11 readdcli ⊢normop⁡S+normop⁡T∈ℝ
13 12 rexri ⊢normop⁡S+normop⁡T∈ℝ*
14 nmopub ⊢S+opT:ℋ⟶ℋ∧normop⁡S+normop⁡T∈ℝ*→normop⁡S+opT≤normop⁡S+normop⁡T↔∀x∈ℋnormℎ⁡x≤1→normℎ⁡S+opT⁡x≤normop⁡S+normop⁡T
15 7 13 14 mp2an ⊢normop⁡S+opT≤normop⁡S+normop⁡T↔∀x∈ℋnormℎ⁡x≤1→normℎ⁡S+opT⁡x≤normop⁡S+normop⁡T
16 4 6 hoscli ⊢x∈ℋ→S+opT⁡x∈ℋ
17 normcl ⊢S+opT⁡x∈ℋ→normℎ⁡S+opT⁡x∈ℝ
18 16 17 syl ⊢x∈ℋ→normℎ⁡S+opT⁡x∈ℝ
19 18 adantr ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡S+opT⁡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→normop⁡S+normop⁡T∈ℝ
29 hosval ⊢S:ℋ⟶ℋ∧T:ℋ⟶ℋ∧x∈ℋ→S+opT⁡x=S⁡x+ℎT⁡x
30 4 6 29 mp3an12 ⊢x∈ℋ→S+opT⁡x=S⁡x+ℎT⁡x
31 30 fveq2d ⊢x∈ℋ→normℎ⁡S+opT⁡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+opT⁡x≤normℎ⁡S⁡x+normℎ⁡T⁡x
35 34 adantr ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡S+opT⁡x≤normℎ⁡S⁡x+normℎ⁡T⁡x
36 nmoplb ⊢S:ℋ⟶ℋ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡S⁡x≤normop⁡S
37 4 36 mp3an1 ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡S⁡x≤normop⁡S
38 nmoplb ⊢T:ℋ⟶ℋ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡T
39 6 38 mp3an1 ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡T
40 le2add ⊢normℎ⁡S⁡x∈ℝ∧normℎ⁡T⁡x∈ℝ∧normop⁡S∈ℝ∧normop⁡T∈ℝ→normℎ⁡S⁡x≤normop⁡S∧normℎ⁡T⁡x≤normop⁡T→normℎ⁡S⁡x+normℎ⁡T⁡x≤normop⁡S+normop⁡T
41 9 11 40 mpanr12 ⊢normℎ⁡S⁡x∈ℝ∧normℎ⁡T⁡x∈ℝ→normℎ⁡S⁡x≤normop⁡S∧normℎ⁡T⁡x≤normop⁡T→normℎ⁡S⁡x+normℎ⁡T⁡x≤normop⁡S+normop⁡T
42 22 25 41 syl2anc ⊢x∈ℋ→normℎ⁡S⁡x≤normop⁡S∧normℎ⁡T⁡x≤normop⁡T→normℎ⁡S⁡x+normℎ⁡T⁡x≤normop⁡S+normop⁡T
43 42 adantr ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡S⁡x≤normop⁡S∧normℎ⁡T⁡x≤normop⁡T→normℎ⁡S⁡x+normℎ⁡T⁡x≤normop⁡S+normop⁡T
44 37 39 43 mp2and ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡S⁡x+normℎ⁡T⁡x≤normop⁡S+normop⁡T
45 19 27 28 35 44 letrd ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡S+opT⁡x≤normop⁡S+normop⁡T
46 45 ex ⊢x∈ℋ→normℎ⁡x≤1→normℎ⁡S+opT⁡x≤normop⁡S+normop⁡T
47 15 46 mprgbir ⊢normop⁡S+opT≤normop⁡S+normop⁡T