Metamath Proof Explorer

Theorem nmopcoi

Description: Upper bound for the norm of the composition of two 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 nmopcoi ⊢normop⁡S∘T≤normop⁡S⁢normop⁡T

Proof

Step Hyp Ref Expression
1 nmoptri.1 ⊢S∈BndLinOp
2 nmoptri.2 ⊢T∈BndLinOp
3 bdopln ⊢S∈BndLinOp→S∈LinOp
4 1 3 ax-mp ⊢S∈LinOp
5 bdopln ⊢T∈BndLinOp→T∈LinOp
6 2 5 ax-mp ⊢T∈LinOp
7 4 6 lnopcoi ⊢S∘T∈LinOp
8 7 lnopfi ⊢S∘T:ℋ⟶ℋ
9 nmopre ⊢S∈BndLinOp→normop⁡S∈ℝ
10 1 9 ax-mp ⊢normop⁡S∈ℝ
11 nmopre ⊢T∈BndLinOp→normop⁡T∈ℝ
12 2 11 ax-mp ⊢normop⁡T∈ℝ
13 10 12 remulcli ⊢normop⁡S⁢normop⁡T∈ℝ
14 13 rexri ⊢normop⁡S⁢normop⁡T∈ℝ*
15 nmopub ⊢S∘T:ℋ⟶ℋ∧normop⁡S⁢normop⁡T∈ℝ*→normop⁡S∘T≤normop⁡S⁢normop⁡T↔∀x∈ℋnormℎ⁡x≤1→normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
16 8 14 15 mp2an ⊢normop⁡S∘T≤normop⁡S⁢normop⁡T↔∀x∈ℋnormℎ⁡x≤1→normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
17 0le0 ⊢0≤0
18 17 a1i ⊢normop⁡T=0∧x∈ℋ→0≤0
19 4 6 lnopco0i ⊢normop⁡T=0→normop⁡S∘T=0
20 7 nmlnop0iHIL ⊢normop⁡S∘T=0↔S∘T=0hop
21 19 20 sylib ⊢normop⁡T=0→S∘T=0hop
22 fveq1 ⊢S∘T=0hop→S∘T⁡x=0hop⁡x
23 22 fveq2d ⊢S∘T=0hop→normℎ⁡S∘T⁡x=normℎ⁡0hop⁡x
24 ho0val ⊢x∈ℋ→0hop⁡x=0ℎ
25 24 fveq2d ⊢x∈ℋ→normℎ⁡0hop⁡x=normℎ⁡0ℎ
26 norm0 ⊢normℎ⁡0ℎ=0
27 25 26 eqtrdi ⊢x∈ℋ→normℎ⁡0hop⁡x=0
28 23 27 sylan9eq ⊢S∘T=0hop∧x∈ℋ→normℎ⁡S∘T⁡x=0
29 21 28 sylan ⊢normop⁡T=0∧x∈ℋ→normℎ⁡S∘T⁡x=0
30 oveq2 ⊢normop⁡T=0→normop⁡S⁢normop⁡T=normop⁡S⋅0
31 10 recni ⊢normop⁡S∈ℂ
32 31 mul01i ⊢normop⁡S⋅0=0
33 30 32 eqtrdi ⊢normop⁡T=0→normop⁡S⁢normop⁡T=0
34 33 adantr ⊢normop⁡T=0∧x∈ℋ→normop⁡S⁢normop⁡T=0
35 18 29 34 3brtr4d ⊢normop⁡T=0∧x∈ℋ→normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
36 35 adantrr ⊢normop⁡T=0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
37 df-ne ⊢normop⁡T≠0↔¬normop⁡T=0
38 8 ffvelcdmi ⊢x∈ℋ→S∘T⁡x∈ℋ
39 normcl ⊢S∘T⁡x∈ℋ→normℎ⁡S∘T⁡x∈ℝ
40 38 39 syl ⊢x∈ℋ→normℎ⁡S∘T⁡x∈ℝ
41 40 recnd ⊢x∈ℋ→normℎ⁡S∘T⁡x∈ℂ
42 12 recni ⊢normop⁡T∈ℂ
43 divrec2 ⊢normℎ⁡S∘T⁡x∈ℂ∧normop⁡T∈ℂ∧normop⁡T≠0→normℎ⁡S∘T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡S∘T⁡x
44 42 43 mp3an2 ⊢normℎ⁡S∘T⁡x∈ℂ∧normop⁡T≠0→normℎ⁡S∘T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡S∘T⁡x
45 41 44 sylan ⊢x∈ℋ∧normop⁡T≠0→normℎ⁡S∘T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡S∘T⁡x
46 45 ancoms ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡S∘T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡S∘T⁡x
47 12 rerecclzi ⊢normop⁡T≠0→1normop⁡T∈ℝ
48 bdopf ⊢T∈BndLinOp→T:ℋ⟶ℋ
49 2 48 ax-mp ⊢T:ℋ⟶ℋ
50 nmopgt0 ⊢T:ℋ⟶ℋ→normop⁡T≠0↔0<normop⁡T
51 49 50 ax-mp ⊢normop⁡T≠0↔0<normop⁡T
52 12 recgt0i ⊢0<normop⁡T→0<1normop⁡T
53 51 52 sylbi ⊢normop⁡T≠0→0<1normop⁡T
54 0re ⊢0∈ℝ
55 ltle ⊢0∈ℝ∧1normop⁡T∈ℝ→0<1normop⁡T→0≤1normop⁡T
56 54 55 mpan ⊢1normop⁡T∈ℝ→0<1normop⁡T→0≤1normop⁡T
57 47 53 56 sylc ⊢normop⁡T≠0→0≤1normop⁡T
58 47 57 absidd ⊢normop⁡T≠0→1normop⁡T=1normop⁡T
59 58 adantr ⊢normop⁡T≠0∧x∈ℋ→1normop⁡T=1normop⁡T
60 59 oveq1d ⊢normop⁡T≠0∧x∈ℋ→1normop⁡T⁢normℎ⁡S∘T⁡x=1normop⁡T⁢normℎ⁡S∘T⁡x
61 46 60 eqtr4d ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡S∘T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡S∘T⁡x
62 42 recclzi ⊢normop⁡T≠0→1normop⁡T∈ℂ
63 norm-iii ⊢1normop⁡T∈ℂ∧S∘T⁡x∈ℋ→normℎ⁡1normop⁡T⋅ℎS∘T⁡x=1normop⁡T⁢normℎ⁡S∘T⁡x
64 62 38 63 syl2an ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡1normop⁡T⋅ℎS∘T⁡x=1normop⁡T⁢normℎ⁡S∘T⁡x
65 61 64 eqtr4d ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡S∘T⁡xnormop⁡T=normℎ⁡1normop⁡T⋅ℎS∘T⁡x
66 49 ffvelcdmi ⊢x∈ℋ→T⁡x∈ℋ
67 4 lnopmuli ⊢1normop⁡T∈ℂ∧T⁡x∈ℋ→S⁡1normop⁡T⋅ℎT⁡x=1normop⁡T⋅ℎS⁡T⁡x
68 62 66 67 syl2an ⊢normop⁡T≠0∧x∈ℋ→S⁡1normop⁡T⋅ℎT⁡x=1normop⁡T⋅ℎS⁡T⁡x
69 bdopf ⊢S∈BndLinOp→S:ℋ⟶ℋ
70 1 69 ax-mp ⊢S:ℋ⟶ℋ
71 70 49 hocoi ⊢x∈ℋ→S∘T⁡x=S⁡T⁡x
72 71 oveq2d ⊢x∈ℋ→1normop⁡T⋅ℎS∘T⁡x=1normop⁡T⋅ℎS⁡T⁡x
73 72 adantl ⊢normop⁡T≠0∧x∈ℋ→1normop⁡T⋅ℎS∘T⁡x=1normop⁡T⋅ℎS⁡T⁡x
74 68 73 eqtr4d ⊢normop⁡T≠0∧x∈ℋ→S⁡1normop⁡T⋅ℎT⁡x=1normop⁡T⋅ℎS∘T⁡x
75 74 fveq2d ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡S⁡1normop⁡T⋅ℎT⁡x=normℎ⁡1normop⁡T⋅ℎS∘T⁡x
76 65 75 eqtr4d ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡S∘T⁡xnormop⁡T=normℎ⁡S⁡1normop⁡T⋅ℎT⁡x
77 76 adantrr ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡S∘T⁡xnormop⁡T=normℎ⁡S⁡1normop⁡T⋅ℎT⁡x
78 hvmulcl ⊢1normop⁡T∈ℂ∧T⁡x∈ℋ→1normop⁡T⋅ℎT⁡x∈ℋ
79 62 66 78 syl2an ⊢normop⁡T≠0∧x∈ℋ→1normop⁡T⋅ℎT⁡x∈ℋ
80 79 adantrr ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→1normop⁡T⋅ℎT⁡x∈ℋ
81 norm-iii ⊢1normop⁡T∈ℂ∧T⁡x∈ℋ→normℎ⁡1normop⁡T⋅ℎT⁡x=1normop⁡T⁢normℎ⁡T⁡x
82 62 66 81 syl2an ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡1normop⁡T⋅ℎT⁡x=1normop⁡T⁢normℎ⁡T⁡x
83 normcl ⊢T⁡x∈ℋ→normℎ⁡T⁡x∈ℝ
84 66 83 syl ⊢x∈ℋ→normℎ⁡T⁡x∈ℝ
85 84 recnd ⊢x∈ℋ→normℎ⁡T⁡x∈ℂ
86 divrec2 ⊢normℎ⁡T⁡x∈ℂ∧normop⁡T∈ℂ∧normop⁡T≠0→normℎ⁡T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡T⁡x
87 42 86 mp3an2 ⊢normℎ⁡T⁡x∈ℂ∧normop⁡T≠0→normℎ⁡T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡T⁡x
88 85 87 sylan ⊢x∈ℋ∧normop⁡T≠0→normℎ⁡T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡T⁡x
89 88 ancoms ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡T⁡x
90 59 oveq1d ⊢normop⁡T≠0∧x∈ℋ→1normop⁡T⁢normℎ⁡T⁡x=1normop⁡T⁢normℎ⁡T⁡x
91 89 90 eqtr4d ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡T⁡xnormop⁡T=1normop⁡T⁢normℎ⁡T⁡x
92 82 91 eqtr4d ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡1normop⁡T⋅ℎT⁡x=normℎ⁡T⁡xnormop⁡T
93 92 adantrr ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡1normop⁡T⋅ℎT⁡x=normℎ⁡T⁡xnormop⁡T
94 nmoplb ⊢T:ℋ⟶ℋ∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡T
95 49 94 mp3an1 ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤normop⁡T
96 42 mullidi ⊢1⁢normop⁡T=normop⁡T
97 95 96 breqtrrdi ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤1⁢normop⁡T
98 97 adantl ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡x≤1⁢normop⁡T
99 84 adantr ⊢x∈ℋ∧normop⁡T≠0→normℎ⁡T⁡x∈ℝ
100 1red ⊢x∈ℋ∧normop⁡T≠0→1∈ℝ
101 12 a1i ⊢x∈ℋ∧normop⁡T≠0→normop⁡T∈ℝ
102 51 biimpi ⊢normop⁡T≠0→0<normop⁡T
103 102 adantl ⊢x∈ℋ∧normop⁡T≠0→0<normop⁡T
104 ledivmul2 ⊢normℎ⁡T⁡x∈ℝ∧1∈ℝ∧normop⁡T∈ℝ∧0<normop⁡T→normℎ⁡T⁡xnormop⁡T≤1↔normℎ⁡T⁡x≤1⁢normop⁡T
105 99 100 101 103 104 syl112anc ⊢x∈ℋ∧normop⁡T≠0→normℎ⁡T⁡xnormop⁡T≤1↔normℎ⁡T⁡x≤1⁢normop⁡T
106 105 ancoms ⊢normop⁡T≠0∧x∈ℋ→normℎ⁡T⁡xnormop⁡T≤1↔normℎ⁡T⁡x≤1⁢normop⁡T
107 106 adantrr ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡xnormop⁡T≤1↔normℎ⁡T⁡x≤1⁢normop⁡T
108 98 107 mpbird ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡T⁡xnormop⁡T≤1
109 93 108 eqbrtrd ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡1normop⁡T⋅ℎT⁡x≤1
110 nmoplb ⊢S:ℋ⟶ℋ∧1normop⁡T⋅ℎT⁡x∈ℋ∧normℎ⁡1normop⁡T⋅ℎT⁡x≤1→normℎ⁡S⁡1normop⁡T⋅ℎT⁡x≤normop⁡S
111 70 110 mp3an1 ⊢1normop⁡T⋅ℎT⁡x∈ℋ∧normℎ⁡1normop⁡T⋅ℎT⁡x≤1→normℎ⁡S⁡1normop⁡T⋅ℎT⁡x≤normop⁡S
112 80 109 111 syl2anc ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡S⁡1normop⁡T⋅ℎT⁡x≤normop⁡S
113 77 112 eqbrtrd ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡S∘T⁡xnormop⁡T≤normop⁡S
114 40 ad2antrl ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡S∘T⁡x∈ℝ
115 10 a1i ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normop⁡S∈ℝ
116 102 adantr ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→0<normop⁡T
117 116 12 jctil ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normop⁡T∈ℝ∧0<normop⁡T
118 ledivmul2 ⊢normℎ⁡S∘T⁡x∈ℝ∧normop⁡S∈ℝ∧normop⁡T∈ℝ∧0<normop⁡T→normℎ⁡S∘T⁡xnormop⁡T≤normop⁡S↔normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
119 114 115 117 118 syl3anc ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡S∘T⁡xnormop⁡T≤normop⁡S↔normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
120 113 119 mpbid ⊢normop⁡T≠0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
121 37 120 sylanbr ⊢¬normop⁡T=0∧x∈ℋ∧normℎ⁡x≤1→normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
122 36 121 pm2.61ian ⊢x∈ℋ∧normℎ⁡x≤1→normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
123 122 ex ⊢x∈ℋ→normℎ⁡x≤1→normℎ⁡S∘T⁡x≤normop⁡S⁢normop⁡T
124 16 123 mprgbir ⊢normop⁡S∘T≤normop⁡S⁢normop⁡T