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 norm op S T norm op S norm op 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 norm op S
10 1 9 ax-mp norm op S
11 nmopre T BndLinOp norm op T
12 2 11 ax-mp norm op T
13 10 12 remulcli norm op S norm op T
14 13 rexri norm op S norm op T *
15 nmopub S T : norm op S norm op T * norm op S T norm op S norm op T x norm x 1 norm S T x norm op S norm op T
16 8 14 15 mp2an norm op S T norm op S norm op T x norm x 1 norm S T x norm op S norm op T
17 0le0 0 0
18 17 a1i norm op T = 0 x 0 0
19 4 6 lnopco0i norm op T = 0 norm op S T = 0
20 7 nmlnop0iHIL norm op S T = 0 S T = 0 hop
21 19 20 sylib norm op T = 0 S T = 0 hop
22 fveq1 S T = 0 hop S T x = 0 hop x
23 22 fveq2d S T = 0 hop norm S T x = norm 0 hop x
24 ho0val x 0 hop x = 0
25 24 fveq2d x norm 0 hop x = norm 0
26 norm0 norm 0 = 0
27 25 26 syl6eq x norm 0 hop x = 0
28 23 27 sylan9eq S T = 0 hop x norm S T x = 0
29 21 28 sylan norm op T = 0 x norm S T x = 0
30 oveq2 norm op T = 0 norm op S norm op T = norm op S 0
31 10 recni norm op S
32 31 mul01i norm op S 0 = 0
33 30 32 syl6eq norm op T = 0 norm op S norm op T = 0
34 33 adantr norm op T = 0 x norm op S norm op T = 0
35 18 29 34 3brtr4d norm op T = 0 x norm S T x norm op S norm op T
36 35 adantrr norm op T = 0 x norm x 1 norm S T x norm op S norm op T
37 df-ne norm op T 0 ¬ norm op T = 0
38 8 ffvelrni 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 norm op T
43 divrec2 norm S T x norm op T norm op T 0 norm S T x norm op T = 1 norm op T norm S T x
44 42 43 mp3an2 norm S T x norm op T 0 norm S T x norm op T = 1 norm op T norm S T x
45 41 44 sylan x norm op T 0 norm S T x norm op T = 1 norm op T norm S T x
46 45 ancoms norm op T 0 x norm S T x norm op T = 1 norm op T norm S T x
47 12 rerecclzi norm op T 0 1 norm op T
48 bdopf T BndLinOp T :
49 2 48 ax-mp T :
50 nmopgt0 T : norm op T 0 0 < norm op T
51 49 50 ax-mp norm op T 0 0 < norm op T
52 12 recgt0i 0 < norm op T 0 < 1 norm op T
53 51 52 sylbi norm op T 0 0 < 1 norm op T
54 0re 0
55 ltle 0 1 norm op T 0 < 1 norm op T 0 1 norm op T
56 54 55 mpan 1 norm op T 0 < 1 norm op T 0 1 norm op T
57 47 53 56 sylc norm op T 0 0 1 norm op T
58 47 57 absidd norm op T 0 1 norm op T = 1 norm op T
59 58 adantr norm op T 0 x 1 norm op T = 1 norm op T
60 59 oveq1d norm op T 0 x 1 norm op T norm S T x = 1 norm op T norm S T x
61 46 60 eqtr4d norm op T 0 x norm S T x norm op T = 1 norm op T norm S T x
62 42 recclzi norm op T 0 1 norm op T
63 norm-iii 1 norm op T S T x norm 1 norm op T S T x = 1 norm op T norm S T x
64 62 38 63 syl2an norm op T 0 x norm 1 norm op T S T x = 1 norm op T norm S T x
65 61 64 eqtr4d norm op T 0 x norm S T x norm op T = norm 1 norm op T S T x
66 49 ffvelrni x T x
67 4 lnopmuli 1 norm op T T x S 1 norm op T T x = 1 norm op T S T x
68 62 66 67 syl2an norm op T 0 x S 1 norm op T T x = 1 norm op 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 1 norm op T S T x = 1 norm op T S T x
73 72 adantl norm op T 0 x 1 norm op T S T x = 1 norm op T S T x
74 68 73 eqtr4d norm op T 0 x S 1 norm op T T x = 1 norm op T S T x
75 74 fveq2d norm op T 0 x norm S 1 norm op T T x = norm 1 norm op T S T x
76 65 75 eqtr4d norm op T 0 x norm S T x norm op T = norm S 1 norm op T T x
77 76 adantrr norm op T 0 x norm x 1 norm S T x norm op T = norm S 1 norm op T T x
78 hvmulcl 1 norm op T T x 1 norm op T T x
79 62 66 78 syl2an norm op T 0 x 1 norm op T T x
80 79 adantrr norm op T 0 x norm x 1 1 norm op T T x
81 norm-iii 1 norm op T T x norm 1 norm op T T x = 1 norm op T norm T x
82 62 66 81 syl2an norm op T 0 x norm 1 norm op T T x = 1 norm op 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 norm op T norm op T 0 norm T x norm op T = 1 norm op T norm T x
87 42 86 mp3an2 norm T x norm op T 0 norm T x norm op T = 1 norm op T norm T x
88 85 87 sylan x norm op T 0 norm T x norm op T = 1 norm op T norm T x
89 88 ancoms norm op T 0 x norm T x norm op T = 1 norm op T norm T x
90 59 oveq1d norm op T 0 x 1 norm op T norm T x = 1 norm op T norm T x
91 89 90 eqtr4d norm op T 0 x norm T x norm op T = 1 norm op T norm T x
92 82 91 eqtr4d norm op T 0 x norm 1 norm op T T x = norm T x norm op T
93 92 adantrr norm op T 0 x norm x 1 norm 1 norm op T T x = norm T x norm op T
94 nmoplb T : x norm x 1 norm T x norm op T
95 49 94 mp3an1 x norm x 1 norm T x norm op T
96 42 mulid2i 1 norm op T = norm op T
97 95 96 breqtrrdi x norm x 1 norm T x 1 norm op T
98 97 adantl norm op T 0 x norm x 1 norm T x 1 norm op T
99 84 adantr x norm op T 0 norm T x
100 1red x norm op T 0 1
101 12 a1i x norm op T 0 norm op T
102 51 biimpi norm op T 0 0 < norm op T
103 102 adantl x norm op T 0 0 < norm op T
104 ledivmul2 norm T x 1 norm op T 0 < norm op T norm T x norm op T 1 norm T x 1 norm op T
105 99 100 101 103 104 syl112anc x norm op T 0 norm T x norm op T 1 norm T x 1 norm op T
106 105 ancoms norm op T 0 x norm T x norm op T 1 norm T x 1 norm op T
107 106 adantrr norm op T 0 x norm x 1 norm T x norm op T 1 norm T x 1 norm op T
108 98 107 mpbird norm op T 0 x norm x 1 norm T x norm op T 1
109 93 108 eqbrtrd norm op T 0 x norm x 1 norm 1 norm op T T x 1
110 nmoplb S : 1 norm op T T x norm 1 norm op T T x 1 norm S 1 norm op T T x norm op S
111 70 110 mp3an1 1 norm op T T x norm 1 norm op T T x 1 norm S 1 norm op T T x norm op S
112 80 109 111 syl2anc norm op T 0 x norm x 1 norm S 1 norm op T T x norm op S
113 77 112 eqbrtrd norm op T 0 x norm x 1 norm S T x norm op T norm op S
114 40 ad2antrl norm op T 0 x norm x 1 norm S T x
115 10 a1i norm op T 0 x norm x 1 norm op S
116 102 adantr norm op T 0 x norm x 1 0 < norm op T
117 116 12 jctil norm op T 0 x norm x 1 norm op T 0 < norm op T
118 ledivmul2 norm S T x norm op S norm op T 0 < norm op T norm S T x norm op T norm op S norm S T x norm op S norm op T
119 114 115 117 118 syl3anc norm op T 0 x norm x 1 norm S T x norm op T norm op S norm S T x norm op S norm op T
120 113 119 mpbid norm op T 0 x norm x 1 norm S T x norm op S norm op T
121 37 120 sylanbr ¬ norm op T = 0 x norm x 1 norm S T x norm op S norm op T
122 36 121 pm2.61ian x norm x 1 norm S T x norm op S norm op T
123 122 ex x norm x 1 norm S T x norm op S norm op T
124 16 123 mprgbir norm op S T norm op S norm op T