HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  nmopcoadji Unicode version

Theorem nmopcoadji 23640
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.)
Hypothesis
Ref Expression
nmopcoadj.1
Assertion
Ref Expression
nmopcoadji

Proof of Theorem nmopcoadji
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nmopcoadj.1 . . . . . . 7
2 adjbdlnb 23623 . . . . . . 7
31, 2mpbi 201 . . . . . 6
4 bdopf 23401 . . . . . 6
53, 4ax-mp 5 . . . . 5
6 bdopf 23401 . . . . . 6
71, 6ax-mp 5 . . . . 5
85, 7hocofi 23305 . . . 4
9 nmopre 23409 . . . . . . 7
101, 9ax-mp 5 . . . . . 6
1110resqcli 11522 . . . . 5
12 rexr 9185 . . . . 5
1311, 12ax-mp 5 . . . 4
14 nmopub 23447 . . . 4
158, 13, 14mp2an 655 . . 3
165, 7hocoi 23303 . . . . . . . 8
1716fveq2d 5783 . . . . . . 7
1817adantr 453 . . . . . 6
197ffvelrni 5921 . . . . . . . . 9
205ffvelrni 5921 . . . . . . . . 9
21 normcl 22663 . . . . . . . . 9
2219, 20, 213syl 19 . . . . . . . 8
2322adantr 453 . . . . . . 7
24 nmopre 23409 . . . . . . . . . 10
253, 24ax-mp 5 . . . . . . . . 9
26 normcl 22663 . . . . . . . . . 10
2719, 26syl 16 . . . . . . . . 9
28 remulcl 9130 . . . . . . . . 9
2925, 27, 28sylancr 646 . . . . . . . 8
3029adantr 453 . . . . . . 7
3125, 10remulcli 9159 . . . . . . . 8
3231a1i 11 . . . . . . 7
333nmbdoplbi 23563 . . . . . . . . 9
3419, 33syl 16 . . . . . . . 8
3534adantr 453 . . . . . . 7
3627adantr 453 . . . . . . . 8
3710a1i 11 . . . . . . . 8
38 normcl 22663 . . . . . . . . . . 11
39 remulcl 9130 . . . . . . . . . . 11
4010, 38, 39sylancr 646 . . . . . . . . . 10
4140adantr 453 . . . . . . . . 9
421nmbdoplbi 23563 . . . . . . . . . 10
4342adantr 453 . . . . . . . . 9
44 1re 9145 . . . . . . . . . . . 12
45 nmopge0 23450 . . . . . . . . . . . . . . 15
461, 6, 45mp2b 10 . . . . . . . . . . . . . 14
4710, 46pm3.2i 443 . . . . . . . . . . . . 13
48 lemul2a 9920 . . . . . . . . . . . . 13
4947, 48mp3anl3 1276 . . . . . . . . . . . 12
5044, 49mpanl2 664 . . . . . . . . . . 11
5138, 50sylan 459 . . . . . . . . . 10
5210recni 9157 . . . . . . . . . . 11
5352mulid1i 9147 . . . . . . . . . 10
5451, 53syl6breq 4286 . . . . . . . . 9
5536, 41, 37, 43, 54letrd 9282 . . . . . . . 8
56 nmopge0 23450 . . . . . . . . . . 11
573, 4, 56mp2b 10 . . . . . . . . . 10
5825, 57pm3.2i 443 . . . . . . . . 9
59 lemul2a 9920 . . . . . . . . 9
6058, 59mp3anl3 1276 . . . . . . . 8
6136, 37, 55, 60syl21anc 1184 . . . . . . 7
6223, 30, 32, 35, 61letrd 9282 . . . . . 6
6318, 62eqbrtrd 4267 . . . . 5
641nmopadji 23629 . . . . . . 7
6564oveq1i 6143 . . . . . 6
6652sqvali 11516 . . . . . 6
6765, 66eqtr4i 2470 . . . . 5
6863, 67syl6breq 4286 . . . 4
6968ex 425 . . 3
7015, 69mprgbir 2787 . 2
71 nmopge0 23450 . . . . . . . 8
728, 71ax-mp 5 . . . . . . 7
733, 1bdopcoi 23637 . . . . . . . . 9
74 nmopre 23409 . . . . . . . . 9
7573, 74ax-mp 5 . . . . . . . 8
7675sqrcli 12230 . . . . . . 7
77 rexr 9185 . . . . . . 7
7872, 76, 77mp2b 10 . . . . . 6
79 nmopub 23447 . . . . . 6
807, 78, 79mp2an 655 . . . . 5
8119, 20syl 16 . . . . . . . . . . . 12
82 hicl 22618 . . . . . . . . . . . 12
8381, 82mpancom 652 . . . . . . . . . . 11
8483abscld 12293 . . . . . . . . . 10
8584adantr 453 . . . . . . . . 9
8622, 38remulcld 9171 . . . . . . . . . 10
8786adantr 453 . . . . . . . . 9
8875a1i 11 . . . . . . . . 9
89 bcs 22719 . . . . . . . . . . 11
9081, 89mpancom 652 . . . . . . . . . 10
9190adantr 453 . . . . . . . . 9
925, 7hococli 23304 . . . . . . . . . . . 12
93 normcl 22663 . . . . . . . . . . . 12
9492, 93syl 16 . . . . . . . . . . 11
9594adantr 453 . . . . . . . . . 10
9638adantr 453 . . . . . . . . . . . 12
97 normge0 22664 . . . . . . . . . . . . . . 15
9819, 20, 973syl 19 . . . . . . . . . . . . . 14
9922, 98jca 520 . . . . . . . . . . . . 13
10099adantr 453 . . . . . . . . . . . 12
101 simpr 449 . . . . . . . . . . . 12
102 lemul2a 9920 . . . . . . . . . . . . 13
10344, 102mp3anl2 1275 . . . . . . . . . . . 12
10496, 100, 101, 103syl21anc 1184 . . . . . . . . . . 11
10522recnd 9169 . . . . . . . . . . . . . 14
106105mulid1d 9160 . . . . . . . . . . . . 13
107106, 17eqtr4d 2482 . . . . . . . . . . . 12
108107adantr 453 . . . . . . . . . . 11
109104, 108breqtrd 4271 . . . . . . . . . 10
110 remulcl 9130 . . . . . . . . . . . . 13
11175, 38, 110sylancr 646 . . . . . . . . . . . 12
112111adantr 453 . . . . . . . . . . 11
11373nmbdoplbi 23563 . . . . . . . . . . . 12
114113adantr 453 . . . . . . . . . . 11
11575, 72pm3.2i 443 . . . . . . . . . . . . . . 15
116 lemul2a 9920 . . . . . . . . . . . . . . 15
117115, 116mp3anl3 1276 . . . . . . . . . . . . . 14
11844, 117mpanl2 664 . . . . . . . . . . . . 13
11938, 118sylan 459 . . . . . . . . . . . 12
12075recni 9157 . . . . . . . . . . . . 13
121120mulid1i 9147 . . . . . . . . . . . 12
122119, 121syl6breq 4286 . . . . . . . . . . 11
12395, 112, 88, 114, 122letrd 9282 . . . . . . . . . 10
12487, 95, 88, 109, 123letrd 9282 . . . . . . . . 9
12585, 87, 88, 91, 124letrd 9282 . . . . . . . 8
126 resqcl 11504 . . . . . . . . . . . 12
127 sqge0 11513 . . . . . . . . . . . 12
128126, 127absidd 12280 . . . . . . . . . . 11
12919, 26, 1283syl 19 . . . . . . . . . 10
130 normsq 22672 . . . . . . . . . . . . 13
13119, 130syl 16 . . . . . . . . . . . 12
132 bdopadj 23621 . . . . . . . . . . . . . . . 16
1333, 132ax-mp 5 . . . . . . . . . . . . . . 15
134 adj2 23473 . . . . . . . . . . . . . . 15
135133, 134mp3an1 1267 . . . . . . . . . . . . . 14
13619, 135mpancom 652 . . . . . . . . . . . . 13
137 bdopadj 23621 . . . . . . . . . . . . . . . 16
138 adjadj 23475 . . . . . . . . . . . . . . . 16
1391, 137, 138mp2b 10 . . . . . . . . . . . . . . 15
140139fveq1i 5780 . . . . . . . . . . . . . 14
141140oveq2i 6144 . . . . . . . . . . . . 13
142136, 141syl6req 2496 . . . . . . . . . . . 12
143131, 142eqtrd 2479 . . . . . . . . . . 11
144143fveq2d 5783 . . . . . . . . . 10
145129, 144eqtr3d 2481 . . . . . . . . 9
146145adantr 453 . . . . . . . 8
14775sqsqri 12234 . . . . . . . . . 10
1488, 71, 147mp2b 10 . . . . . . . . 9
149148a1i 11 . . . . . . . 8
150125, 146, 1493brtr4d 4277 . . . . . . 7
151 normge0 22664 . . . . . . . . . 10
15219, 151syl 16 . . . . . . . . 9
1538, 71, 76mp2b 10 . . . . . . . . . 10
15475sqrge0i 12235 . . . . . . . . . . 11
1558, 71, 154mp2b 10 . . . . . . . . . 10
156 le2sq 11511 . . . . . . . . . 10
157153, 155, 156mpanr12 668 . . . . . . . . 9
15827, 152, 157syl2anc 644 . . . . . . . 8
159158adantr 453 . . . . . . 7
160150, 159mpbird 225 . . . . . 6
161160ex 425 . . . . 5
16280, 161mprgbir 2787 . . . 4
16310, 153le2sqi 11526 . . . . 5
16446, 155, 163mp2an 655 . . . 4
165162, 164mpbi 201 . . 3
166165, 148breqtri 4270 . 2
16775, 11letri3i 9244 . 2
16870, 166, 167mpbir2an 888 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  =wceq 1654  e.wcel 1728  A.wral 2716   class class class wbr 4247  domcdm 4923  o.ccom 4927  -->wf 5501  `cfv 5505  (class class class)co 6133   cc 9043   cr 9044  0cc0 9045  1c1 9046   cmul 9050   cxr 9174   cle 9176  2c2 10104   cexp 11437   csqr 12093   cabs 12094   chil 22458   csp 22461   cno 22462   cnop 22484   cbo 22487   cado 22494
This theorem is referenced by:  nmopcoadj2i  23641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1955  ax-ext 2428  ax-rep 4358  ax-sep 4368  ax-nul 4376  ax-pow 4420  ax-pr 4446  ax-un 4746  ax-inf2 7649  ax-cc 8370  ax-cnex 9101  ax-resscn 9102  ax-1cn 9103  ax-icn 9104  ax-addcl 9105  ax-addrcl 9106  ax-mulcl 9107  ax-mulrcl 9108  ax-mulcom 9109  ax-addass 9110  ax-mulass 9111  ax-distr 9112  ax-i2m1 9113  ax-1ne0 9114  ax-1rid 9115  ax-rnegex 9116  ax-rrecex 9117  ax-cnre 9118  ax-pre-lttri 9119  ax-pre-lttrn 9120  ax-pre-ltadd 9121  ax-pre-mulgt0 9122  ax-pre-sup 9123  ax-addf 9124  ax-mulf 9125  ax-hilex 22538  ax-hfvadd 22539  ax-hvcom 22540  ax-hvass 22541  ax-hv0cl 22542  ax-hvaddid 22543  ax-hfvmul 22544  ax-hvmulid 22545  ax-hvmulass 22546  ax-hvdistr1 22547  ax-hvdistr2 22548  ax-hvmul0 22549  ax-hfi 22617  ax-his1 22620  ax-his2 22621  ax-his3 22622  ax-his4 22623  ax-hcompl 22740
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-fal 1330  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2296  df-mo 2297  df-clab 2434  df-cleq 2440  df-clel 2443  df-nfc 2572  df-ne 2612  df-nel 2613  df-ral 2721  df-rex 2722  df-reu 2723  df-rmo 2724  df-rab 2725  df-v 2971  df-sbc 3175  df-csb 3275  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3621  df-if 3770  df-pw 3832  df-sn 3851  df-pr 3852  df-tp 3853  df-op 3854  df-uni 4048  df-int 4084  df-iun 4128  df-iin 4129  df-br 4248  df-opab 4306  df-mpt 4307  df-tr 4341  df-eprel 4539  df-id 4543  df-po 4548  df-so 4549  df-fr 4586  df-se 4587  df-we 4588  df-ord 4629  df-on 4630  df-lim 4631  df-suc 4632  df-om 4891  df-xp 4929  df-rel 4930  df-cnv 4931  df-co 4932  df-dm 4933  df-rn 4934  df-res 4935  df-ima 4936  df-iota 5468  df-fun 5507  df-fn 5508  df-f 5509  df-f1 5510  df-fo 5511  df-f1o 5512  df-fv 5513  df-isom 5514  df-ov 6136  df-oprab 6137  df-mpt2 6138  df-of 6359  df-1st 6403  df-2nd 6404  df-riota 6603  df-recs 6686  df-rdg 6721  df-1o 6777  df-2o 6778  df-oadd 6781  df-omul 6782  df-er 6958  df-map 7073  df-pm 7074  df-ixp 7117  df-en 7163  df-dom 7164  df-sdom 7165  df-fin 7166  df-fi 7469  df-sup 7499  df-oi 7532  df-card 7881  df-acn 7884  df-cda 8103  df-pnf 9177  df-mnf 9178  df-xr 9179  df-ltxr 9180  df-le 9181  df-sub 9348  df-neg 9349  df-div 9733  df-nn 10056  df-2 10113  df-3 10114  df-4 10115  df-5 10116  df-6 10117  df-7 10118  df-8 10119  df-9 10120  df-10 10121  df-n0 10277  df-z 10338  df-dec 10438  df-uz 10544  df-q 10630  df-rp 10668  df-xneg 10765  df-xadd 10766  df-xmul 10767  df-ioo 10975  df-ico 10977  df-icc 10978  df-fz 11099  df-fzo 11191  df-fl 11257  df-seq 11379  df-exp 11438  df-hash 11674  df-cj 11959  df-re 11960  df-im 11961  df-sqr 12095  df-abs 12096  df-clim 12337  df-rlim 12338  df-sum 12535  df-struct 13526  df-ndx 13527  df-slot 13528  df-base 13529  df-sets 13530  df-ress 13531  df-plusg 13597  df-mulr 13598  df-starv 13599  df-sca 13600  df-vsca 13601  df-tset 13603  df-ple 13604  df-ds 13606  df-unif 13607  df-hom 13608  df-cco 13609  df-rest 13705  df-topn 13706  df-topgen 13722  df-pt 13723  df-prds 13726  df-xrs 13781  df-0g 13782  df-gsum 13783  df-qtop 13788  df-imas 13789  df-xps 13791  df-mre 13866  df-mrc 13867  df-acs 13869  df-mnd 14726  df-submnd 14775  df-mulg 14851  df-cntz 15152  df-cmn 15450  df-psmet 16730  df-xmet 16731  df-met 16732  df-bl 16733  df-mopn 16734  df-fbas 16735  df-fg 16736  df-cnfld 16740  df-top 16999  df-bases 17001  df-topon 17002  df-topsp 17003  df-cld 17119  df-ntr 17120  df-cls 17121  df-nei 17198  df-cn 17327  df-cnp 17328  df-lm 17329  df-t1 17414  df-haus 17415  df-tx 17630  df-hmeo 17823  df-fil 17914  df-fm 18006  df-flim 18007  df-flf 18008  df-xms 18386  df-ms 18387  df-tms 18388  df-cfil 19244  df-cau 19245  df-cmet 19246  df-grpo 21815  df-gid 21816  df-ginv 21817  df-gdiv 21818  df-ablo 21906  df-subgo 21926  df-vc 22061  df-nv 22107  df-va 22110  df-ba 22111  df-sm 22112  df-0v 22113  df-vs 22114  df-nmcv 22115  df-ims 22116  df-dip 22233  df-ssp 22257  df-lno 22281  df-nmoo 22282  df-0o 22284  df-ph 22350  df-cbn 22401  df-hnorm 22507  df-hba 22508  df-hvsub 22510  df-hlim 22511  df-hcau 22512  df-sh 22745  df-ch 22760  df-oc 22790  df-ch0 22791  df-shs 22846  df-pjh 22933  df-h0op 23287  df-nmop 23378  df-cnop 23379  df-lnop 23380  df-bdop 23381  df-unop 23382  df-hmop 23383  df-nmfn 23384  df-nlfn 23385  df-cnfn 23386  df-lnfn 23387  df-adjh 23388
  Copyright terms: Public domain W3C validator