Metamath Proof Explorer


Theorem nmopcoadji

Description: The norm of an operator composed with its adjoint. Part of Theorem 3.11(vi) of Beran p. 106. (Contributed by NM, 8-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopcoadj.1 T BndLinOp
Assertion nmopcoadji norm op adj h T T = norm op T 2

Proof

Step Hyp Ref Expression
1 nmopcoadj.1 T BndLinOp
2 adjbdlnb T BndLinOp adj h T BndLinOp
3 1 2 mpbi adj h T BndLinOp
4 bdopf adj h T BndLinOp adj h T :
5 3 4 ax-mp adj h T :
6 bdopf T BndLinOp T :
7 1 6 ax-mp T :
8 5 7 hocofi adj h T T :
9 nmopre T BndLinOp norm op T
10 1 9 ax-mp norm op T
11 10 resqcli norm op T 2
12 rexr norm op T 2 norm op T 2 *
13 11 12 ax-mp norm op T 2 *
14 nmopub adj h T T : norm op T 2 * norm op adj h T T norm op T 2 x norm x 1 norm adj h T T x norm op T 2
15 8 13 14 mp2an norm op adj h T T norm op T 2 x norm x 1 norm adj h T T x norm op T 2
16 5 7 hocoi x adj h T T x = adj h T T x
17 16 fveq2d x norm adj h T T x = norm adj h T T x
18 17 adantr x norm x 1 norm adj h T T x = norm adj h T T x
19 7 ffvelrni x T x
20 5 ffvelrni T x adj h T T x
21 normcl adj h T T x norm adj h T T x
22 19 20 21 3syl x norm adj h T T x
23 22 adantr x norm x 1 norm adj h T T x
24 nmopre adj h T BndLinOp norm op adj h T
25 3 24 ax-mp norm op adj h T
26 normcl T x norm T x
27 19 26 syl x norm T x
28 remulcl norm op adj h T norm T x norm op adj h T norm T x
29 25 27 28 sylancr x norm op adj h T norm T x
30 29 adantr x norm x 1 norm op adj h T norm T x
31 25 10 remulcli norm op adj h T norm op T
32 31 a1i x norm x 1 norm op adj h T norm op T
33 3 nmbdoplbi T x norm adj h T T x norm op adj h T norm T x
34 19 33 syl x norm adj h T T x norm op adj h T norm T x
35 34 adantr x norm x 1 norm adj h T T x norm op adj h T norm T x
36 27 adantr x norm x 1 norm T x
37 10 a1i x norm x 1 norm op T
38 normcl x norm x
39 remulcl norm op T norm x norm op T norm x
40 10 38 39 sylancr x norm op T norm x
41 40 adantr x norm x 1 norm op T norm x
42 1 nmbdoplbi x norm T x norm op T norm x
43 42 adantr x norm x 1 norm T x norm op T norm x
44 1re 1
45 nmopge0 T : 0 norm op T
46 1 6 45 mp2b 0 norm op T
47 10 46 pm3.2i norm op T 0 norm op T
48 lemul2a norm x 1 norm op T 0 norm op T norm x 1 norm op T norm x norm op T 1
49 47 48 mp3anl3 norm x 1 norm x 1 norm op T norm x norm op T 1
50 44 49 mpanl2 norm x norm x 1 norm op T norm x norm op T 1
51 38 50 sylan x norm x 1 norm op T norm x norm op T 1
52 10 recni norm op T
53 52 mulid1i norm op T 1 = norm op T
54 51 53 breqtrdi x norm x 1 norm op T norm x norm op T
55 36 41 37 43 54 letrd x norm x 1 norm T x norm op T
56 nmopge0 adj h T : 0 norm op adj h T
57 3 4 56 mp2b 0 norm op adj h T
58 25 57 pm3.2i norm op adj h T 0 norm op adj h T
59 lemul2a norm T x norm op T norm op adj h T 0 norm op adj h T norm T x norm op T norm op adj h T norm T x norm op adj h T norm op T
60 58 59 mp3anl3 norm T x norm op T norm T x norm op T norm op adj h T norm T x norm op adj h T norm op T
61 36 37 55 60 syl21anc x norm x 1 norm op adj h T norm T x norm op adj h T norm op T
62 23 30 32 35 61 letrd x norm x 1 norm adj h T T x norm op adj h T norm op T
63 18 62 eqbrtrd x norm x 1 norm adj h T T x norm op adj h T norm op T
64 1 nmopadji norm op adj h T = norm op T
65 64 oveq1i norm op adj h T norm op T = norm op T norm op T
66 52 sqvali norm op T 2 = norm op T norm op T
67 65 66 eqtr4i norm op adj h T norm op T = norm op T 2
68 63 67 breqtrdi x norm x 1 norm adj h T T x norm op T 2
69 68 ex x norm x 1 norm adj h T T x norm op T 2
70 15 69 mprgbir norm op adj h T T norm op T 2
71 nmopge0 adj h T T : 0 norm op adj h T T
72 8 71 ax-mp 0 norm op adj h T T
73 3 1 bdopcoi adj h T T BndLinOp
74 nmopre adj h T T BndLinOp norm op adj h T T
75 73 74 ax-mp norm op adj h T T
76 75 sqrtcli 0 norm op adj h T T norm op adj h T T
77 rexr norm op adj h T T norm op adj h T T *
78 72 76 77 mp2b norm op adj h T T *
79 nmopub T : norm op adj h T T * norm op T norm op adj h T T x norm x 1 norm T x norm op adj h T T
80 7 78 79 mp2an norm op T norm op adj h T T x norm x 1 norm T x norm op adj h T T
81 19 20 syl x adj h T T x
82 hicl adj h T T x x adj h T T x ih x
83 81 82 mpancom x adj h T T x ih x
84 83 abscld x adj h T T x ih x
85 84 adantr x norm x 1 adj h T T x ih x
86 22 38 remulcld x norm adj h T T x norm x
87 86 adantr x norm x 1 norm adj h T T x norm x
88 75 a1i x norm x 1 norm op adj h T T
89 bcs adj h T T x x adj h T T x ih x norm adj h T T x norm x
90 81 89 mpancom x adj h T T x ih x norm adj h T T x norm x
91 90 adantr x norm x 1 adj h T T x ih x norm adj h T T x norm x
92 5 7 hococli x adj h T T x
93 normcl adj h T T x norm adj h T T x
94 92 93 syl x norm adj h T T x
95 94 adantr x norm x 1 norm adj h T T x
96 38 adantr x norm x 1 norm x
97 normge0 adj h T T x 0 norm adj h T T x
98 19 20 97 3syl x 0 norm adj h T T x
99 22 98 jca x norm adj h T T x 0 norm adj h T T x
100 99 adantr x norm x 1 norm adj h T T x 0 norm adj h T T x
101 simpr x norm x 1 norm x 1
102 lemul2a norm x 1 norm adj h T T x 0 norm adj h T T x norm x 1 norm adj h T T x norm x norm adj h T T x 1
103 44 102 mp3anl2 norm x norm adj h T T x 0 norm adj h T T x norm x 1 norm adj h T T x norm x norm adj h T T x 1
104 96 100 101 103 syl21anc x norm x 1 norm adj h T T x norm x norm adj h T T x 1
105 22 recnd x norm adj h T T x
106 105 mulid1d x norm adj h T T x 1 = norm adj h T T x
107 106 17 eqtr4d x norm adj h T T x 1 = norm adj h T T x
108 107 adantr x norm x 1 norm adj h T T x 1 = norm adj h T T x
109 104 108 breqtrd x norm x 1 norm adj h T T x norm x norm adj h T T x
110 remulcl norm op adj h T T norm x norm op adj h T T norm x
111 75 38 110 sylancr x norm op adj h T T norm x
112 111 adantr x norm x 1 norm op adj h T T norm x
113 73 nmbdoplbi x norm adj h T T x norm op adj h T T norm x
114 113 adantr x norm x 1 norm adj h T T x norm op adj h T T norm x
115 75 72 pm3.2i norm op adj h T T 0 norm op adj h T T
116 lemul2a norm x 1 norm op adj h T T 0 norm op adj h T T norm x 1 norm op adj h T T norm x norm op adj h T T 1
117 115 116 mp3anl3 norm x 1 norm x 1 norm op adj h T T norm x norm op adj h T T 1
118 44 117 mpanl2 norm x norm x 1 norm op adj h T T norm x norm op adj h T T 1
119 38 118 sylan x norm x 1 norm op adj h T T norm x norm op adj h T T 1
120 75 recni norm op adj h T T
121 120 mulid1i norm op adj h T T 1 = norm op adj h T T
122 119 121 breqtrdi x norm x 1 norm op adj h T T norm x norm op adj h T T
123 95 112 88 114 122 letrd x norm x 1 norm adj h T T x norm op adj h T T
124 87 95 88 109 123 letrd x norm x 1 norm adj h T T x norm x norm op adj h T T
125 85 87 88 91 124 letrd x norm x 1 adj h T T x ih x norm op adj h T T
126 resqcl norm T x norm T x 2
127 sqge0 norm T x 0 norm T x 2
128 126 127 absidd norm T x norm T x 2 = norm T x 2
129 19 26 128 3syl x norm T x 2 = norm T x 2
130 normsq T x norm T x 2 = T x ih T x
131 19 130 syl x norm T x 2 = T x ih T x
132 bdopadj adj h T BndLinOp adj h T dom adj h
133 3 132 ax-mp adj h T dom adj h
134 adj2 adj h T dom adj h T x x adj h T T x ih x = T x ih adj h adj h T x
135 133 134 mp3an1 T x x adj h T T x ih x = T x ih adj h adj h T x
136 19 135 mpancom x adj h T T x ih x = T x ih adj h adj h T x
137 bdopadj T BndLinOp T dom adj h
138 adjadj T dom adj h adj h adj h T = T
139 1 137 138 mp2b adj h adj h T = T
140 139 fveq1i adj h adj h T x = T x
141 140 oveq2i T x ih adj h adj h T x = T x ih T x
142 136 141 eqtr2di x T x ih T x = adj h T T x ih x
143 131 142 eqtrd x norm T x 2 = adj h T T x ih x
144 143 fveq2d x norm T x 2 = adj h T T x ih x
145 129 144 eqtr3d x norm T x 2 = adj h T T x ih x
146 145 adantr x norm x 1 norm T x 2 = adj h T T x ih x
147 75 sqsqrti 0 norm op adj h T T norm op adj h T T 2 = norm op adj h T T
148 8 71 147 mp2b norm op adj h T T 2 = norm op adj h T T
149 148 a1i x norm x 1 norm op adj h T T 2 = norm op adj h T T
150 125 146 149 3brtr4d x norm x 1 norm T x 2 norm op adj h T T 2
151 normge0 T x 0 norm T x
152 19 151 syl x 0 norm T x
153 8 71 76 mp2b norm op adj h T T
154 75 sqrtge0i 0 norm op adj h T T 0 norm op adj h T T
155 8 71 154 mp2b 0 norm op adj h T T
156 le2sq norm T x 0 norm T x norm op adj h T T 0 norm op adj h T T norm T x norm op adj h T T norm T x 2 norm op adj h T T 2
157 153 155 156 mpanr12 norm T x 0 norm T x norm T x norm op adj h T T norm T x 2 norm op adj h T T 2
158 27 152 157 syl2anc x norm T x norm op adj h T T norm T x 2 norm op adj h T T 2
159 158 adantr x norm x 1 norm T x norm op adj h T T norm T x 2 norm op adj h T T 2
160 150 159 mpbird x norm x 1 norm T x norm op adj h T T
161 160 ex x norm x 1 norm T x norm op adj h T T
162 80 161 mprgbir norm op T norm op adj h T T
163 10 153 le2sqi 0 norm op T 0 norm op adj h T T norm op T norm op adj h T T norm op T 2 norm op adj h T T 2
164 46 155 163 mp2an norm op T norm op adj h T T norm op T 2 norm op adj h T T 2
165 162 164 mpbi norm op T 2 norm op adj h T T 2
166 165 148 breqtri norm op T 2 norm op adj h T T
167 75 11 letri3i norm op adj h T T = norm op T 2 norm op adj h T T norm op T 2 norm op T 2 norm op adj h T T
168 70 166 167 mpbir2an norm op adj h T T = norm op T 2