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