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

Theorem nmopcoadji 24627
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 24610 . . . . . . 7
31, 2mpbi 201 . . . . . 6
4 bdopf 24388 . . . . . 6
53, 4ax-mp 5 . . . . 5
6 bdopf 24388 . . . . . 6
71, 6ax-mp 5 . . . . 5
85, 7hocofi 24292 . . . 4
9 nmopre 24396 . . . . . . 7
101, 9ax-mp 5 . . . . . 6
1110resqcli 11800 . . . . 5
12 rexr 9308 . . . . 5
1311, 12ax-mp 5 . . . 4
14 nmopub 24434 . . . 4
158, 13, 14mp2an 655 . . 3
165, 7hocoi 24290 . . . . . . . 8
1716fveq2d 5712 . . . . . . 7
1817adantr 453 . . . . . 6
197ffvelrni 5858 . . . . . . . . 9
205ffvelrni 5858 . . . . . . . . 9
21 normcl 23649 . . . . . . . . 9
2219, 20, 213syl 19 . . . . . . . 8
2322adantr 453 . . . . . . 7
24 nmopre 24396 . . . . . . . . . 10
253, 24ax-mp 5 . . . . . . . . 9
26 normcl 23649 . . . . . . . . . 10
2719, 26syl 16 . . . . . . . . 9
28 remulcl 9246 . . . . . . . . 9
2925, 27, 28sylancr 646 . . . . . . . 8
3029adantr 453 . . . . . . 7
3125, 10remulcli 9279 . . . . . . . 8
3231a1i 11 . . . . . . 7
333nmbdoplbi 24550 . . . . . . . . 9
3419, 33syl 16 . . . . . . . 8
3534adantr 453 . . . . . . 7
3627adantr 453 . . . . . . . 8
3710a1i 11 . . . . . . . 8
38 normcl 23649 . . . . . . . . . . 11
39 remulcl 9246 . . . . . . . . . . 11
4010, 38, 39sylancr 646 . . . . . . . . . 10
4140adantr 453 . . . . . . . . 9
421nmbdoplbi 24550 . . . . . . . . . 10
4342adantr 453 . . . . . . . . 9
44 1re 9264 . . . . . . . . . . . 12
45 nmopge0 24437 . . . . . . . . . . . . . . 15
461, 6, 45mp2b 10 . . . . . . . . . . . . . 14
4710, 46pm3.2i 443 . . . . . . . . . . . . 13
48 lemul2a 10053 . . . . . . . . . . . . 13
4947, 48mp3anl3 1283 . . . . . . . . . . . 12
5044, 49mpanl2 664 . . . . . . . . . . 11
5138, 50sylan 459 . . . . . . . . . 10
5210recni 9277 . . . . . . . . . . 11
5352mulid1i 9267 . . . . . . . . . 10
5451, 53syl6breq 4357 . . . . . . . . 9
5536, 41, 37, 43, 54letrd 9407 . . . . . . . 8
56 nmopge0 24437 . . . . . . . . . . 11
573, 4, 56mp2b 10 . . . . . . . . . 10
5825, 57pm3.2i 443 . . . . . . . . 9
59 lemul2a 10053 . . . . . . . . 9
6058, 59mp3anl3 1283 . . . . . . . 8
6136, 37, 55, 60syl21anc 1191 . . . . . . 7
6223, 30, 32, 35, 61letrd 9407 . . . . . 6
6318, 62eqbrtrd 4338 . . . . 5
641nmopadji 24616 . . . . . . 7
6564oveq1i 6113 . . . . . 6
6652sqvali 11794 . . . . . 6
6765, 66eqtr4i 2512 . . . . 5
6863, 67syl6breq 4357 . . . 4
6968ex 425 . . 3
7015, 69mprgbir 2830 . 2
71 nmopge0 24437 . . . . . . . 8
728, 71ax-mp 5 . . . . . . 7
733, 1bdopcoi 24624 . . . . . . . . 9
74 nmopre 24396 . . . . . . . . 9
7573, 74ax-mp 5 . . . . . . . 8
7675sqrcli 12706 . . . . . . 7
77 rexr 9308 . . . . . . 7
7872, 76, 77mp2b 10 . . . . . 6
79 nmopub 24434 . . . . . 6
807, 78, 79mp2an 655 . . . . 5
8119, 20syl 16 . . . . . . . . . . . 12
82 hicl 23604 . . . . . . . . . . . 12
8381, 82mpancom 652 . . . . . . . . . . 11
8483abscld 12769 . . . . . . . . . 10
8584adantr 453 . . . . . . . . 9
8622, 38remulcld 9293 . . . . . . . . . 10
8786adantr 453 . . . . . . . . 9
8875a1i 11 . . . . . . . . 9
89 bcs 23705 . . . . . . . . . . 11
9081, 89mpancom 652 . . . . . . . . . 10
9190adantr 453 . . . . . . . . 9
925, 7hococli 24291 . . . . . . . . . . . 12
93 normcl 23649 . . . . . . . . . . . 12
9492, 93syl 16 . . . . . . . . . . 11
9594adantr 453 . . . . . . . . . 10
9638adantr 453 . . . . . . . . . . . 12
97 normge0 23650 . . . . . . . . . . . . . . 15
9819, 20, 973syl 19 . . . . . . . . . . . . . 14
9922, 98jca 520 . . . . . . . . . . . . 13
10099adantr 453 . . . . . . . . . . . 12
101 simpr 449 . . . . . . . . . . . 12
102 lemul2a 10053 . . . . . . . . . . . . 13
10344, 102mp3anl2 1282 . . . . . . . . . . . 12
10496, 100, 101, 103syl21anc 1191 . . . . . . . . . . 11
10522recnd 9291 . . . . . . . . . . . . . 14
106105mulid1d 9282 . . . . . . . . . . . . 13
107106, 17eqtr4d 2524 . . . . . . . . . . . 12
108107adantr 453 . . . . . . . . . . 11
109104, 108breqtrd 4342 . . . . . . . . . 10
110 remulcl 9246 . . . . . . . . . . . . 13
11175, 38, 110sylancr 646 . . . . . . . . . . . 12
112111adantr 453 . . . . . . . . . . 11
11373nmbdoplbi 24550 . . . . . . . . . . . 12
114113adantr 453 . . . . . . . . . . 11
11575, 72pm3.2i 443 . . . . . . . . . . . . . . 15
116 lemul2a 10053 . . . . . . . . . . . . . . 15
117115, 116mp3anl3 1283 . . . . . . . . . . . . . 14
11844, 117mpanl2 664 . . . . . . . . . . . . 13
11938, 118sylan 459 . . . . . . . . . . . 12
12075recni 9277 . . . . . . . . . . . . 13
121120mulid1i 9267 . . . . . . . . . . . 12
122119, 121syl6breq 4357 . . . . . . . . . . 11
12395, 112, 88, 114, 122letrd 9407 . . . . . . . . . 10
12487, 95, 88, 109, 123letrd 9407 . . . . . . . . 9
12585, 87, 88, 91, 124letrd 9407 . . . . . . . 8
126 resqcl 11782 . . . . . . . . . . . 12
127 sqge0 11791 . . . . . . . . . . . 12
128126, 127absidd 12756 . . . . . . . . . . 11
12919, 26, 1283syl 19 . . . . . . . . . 10
130 normsq 23658 . . . . . . . . . . . . 13
13119, 130syl 16 . . . . . . . . . . . 12
132 bdopadj 24608 . . . . . . . . . . . . . . . 16
1333, 132ax-mp 5 . . . . . . . . . . . . . . 15
134 adj2 24460 . . . . . . . . . . . . . . 15
135133, 134mp3an1 1274 . . . . . . . . . . . . . 14
13619, 135mpancom 652 . . . . . . . . . . . . 13
137 bdopadj 24608 . . . . . . . . . . . . . . . 16
138 adjadj 24462 . . . . . . . . . . . . . . . 16
1391, 137, 138mp2b 10 . . . . . . . . . . . . . . 15
140139fveq1i 5709 . . . . . . . . . . . . . 14
141140oveq2i 6114 . . . . . . . . . . . . 13
142136, 141syl6req 2538 . . . . . . . . . . . 12
143131, 142eqtrd 2521 . . . . . . . . . . 11
144143fveq2d 5712 . . . . . . . . . 10
145129, 144eqtr3d 2523 . . . . . . . . 9
146145adantr 453 . . . . . . . 8
14775sqsqri 12710 . . . . . . . . . 10
1488, 71, 147mp2b 10 . . . . . . . . 9
149148a1i 11 . . . . . . . 8
150125, 146, 1493brtr4d 4348 . . . . . . 7
151 normge0 23650 . . . . . . . . . 10
15219, 151syl 16 . . . . . . . . 9
1538, 71, 76mp2b 10 . . . . . . . . . 10
15475sqrge0i 12711 . . . . . . . . . . 11
1558, 71, 154mp2b 10 . . . . . . . . . 10
156 le2sq 11789 . . . . . . . . . 10
157153, 155, 156mpanr12 668 . . . . . . . . 9
15827, 152, 157syl2anc 644 . . . . . . . 8
159158adantr 453 . . . . . . 7
160150, 159mpbird 225 . . . . . 6
161160ex 425 . . . . 5
16280, 161mprgbir 2830 . . . 4
16310, 153le2sqi 11804 . . . . 5
16446, 155, 163mp2an 655 . . . 4
165162, 164mpbi 201 . . 3
166165, 148breqtri 4341 . 2
16775, 11letri3i 9369 . 2
16870, 166, 167mpbir2an 888 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  =wceq 1670  e.wcel 1732  A.wral 2759   class class class wbr 4318  domcdm 4862  o.ccom 4866  -->wf 5434  `cfv 5438  (class class class)co 6103   cc 9159   cr 9160  0cc0 9161  1c1 9162   cmul 9166   cxr 9296   cle 9298  2c2 10237   cexp 11714   csqr 12569   cabs 12570   chil 23443   csp 23446   cno 23447   cnop 23469   cbo 23472   cado 23479
This theorem is referenced by:  nmopcoadj2i  24628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-rep 4429  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382  ax-inf2 7763  ax-cc 8486  ax-cnex 9217  ax-resscn 9218  ax-1cn 9219  ax-icn 9220  ax-addcl 9221  ax-addrcl 9222  ax-mulcl 9223  ax-mulrcl 9224  ax-mulcom 9225  ax-addass 9226  ax-mulass 9227  ax-distr 9228  ax-i2m1 9229  ax-1ne0 9230  ax-1rid 9231  ax-rnegex 9232  ax-rrecex 9233  ax-cnre 9234  ax-pre-lttri 9235  ax-pre-lttrn 9236  ax-pre-ltadd 9237  ax-pre-mulgt0 9238  ax-pre-sup 9239  ax-addf 9240  ax-mulf 9241  ax-hilex 23523  ax-hfvadd 23524  ax-hvcom 23525  ax-hvass 23526  ax-hv0cl 23527  ax-hvaddid 23528  ax-hfvmul 23529  ax-hvmulid 23530  ax-hvmulass 23531  ax-hvdistr1 23532  ax-hvdistr2 23533  ax-hvmul0 23534  ax-hfi 23603  ax-his1 23606  ax-his2 23607  ax-his3 23608  ax-his4 23609  ax-hcompl 23726
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-fal 1339  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-nel 2655  df-ral 2764  df-rex 2765  df-reu 2766  df-rmo 2767  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-int 4155  df-iun 4199  df-iin 4200  df-br 4319  df-opab 4377  df-mpt 4378  df-tr 4412  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-isom 5447  df-riota 6062  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-of 6330  df-om 6487  df-1st 6583  df-2nd 6584  df-recs 6795  df-rdg 6830  df-1o 6886  df-2o 6887  df-oadd 6890  df-omul 6891  df-er 7067  df-map 7182  df-pm 7183  df-ixp 7227  df-en 7274  df-dom 7275  df-sdom 7276  df-fin 7277  df-fi 7583  df-sup 7613  df-oi 7646  df-card 7995  df-acn 7998  df-cda 8219  df-pnf 9299  df-mnf 9300  df-xr 9301  df-ltxr 9302  df-le 9303  df-sub 9474  df-neg 9475  df-div 9865  df-nn 10189  df-2 10246  df-3 10247  df-4 10248  df-5 10249  df-6 10250  df-7 10251  df-8 10252  df-9 10253  df-10 10254  df-n0 10446  df-z 10511  df-dec 10620  df-uz 10726  df-q 10818  df-rp 10856  df-xneg 10953  df-xadd 10954  df-xmul 10955  df-ioo 11168  df-ico 11170  df-icc 11171  df-fz 11294  df-fzo 11401  df-fl 11491  df-seq 11656  df-exp 11715  df-hash 11953  df-cj 12435  df-re 12436  df-im 12437  df-sqr 12571  df-abs 12572  df-clim 12813  df-rlim 12814  df-sum 13011  df-struct 14023  df-ndx 14024  df-slot 14025  df-base 14026  df-sets 14027  df-ress 14028  df-plusg 14096  df-mulr 14097  df-starv 14098  df-sca 14099  df-vsca 14100  df-tset 14102  df-ple 14103  df-ds 14105  df-unif 14106  df-hom 14107  df-cco 14108  df-rest 14204  df-topn 14205  df-topgen 14221  df-pt 14222  df-prds 14225  df-xrs 14280  df-0g 14281  df-gsum 14282  df-qtop 14287  df-imas 14288  df-xps 14290  df-mre 14365  df-mrc 14366  df-acs 14368  df-mnd 15256  df-submnd 15305  df-mulg 15386  df-cntz 15725  df-cmn 16023  df-psmet 17319  df-xmet 17320  df-met 17321  df-bl 17322  df-mopn 17323  df-fbas 17324  df-fg 17325  df-cnfld 17329  df-top 17977  df-bases 17979  df-topon 17980  df-topsp 17981  df-cld 18097  df-ntr 18098  df-cls 18099  df-nei 18176  df-cn 18305  df-cnp 18306  df-lm 18307  df-t1 18392  df-haus 18393  df-tx 18609  df-hmeo 18802  df-fil 18893  df-fm 18985  df-flim 18986  df-flf 18987  df-xms 19365  df-ms 19366  df-tms 19367  df-cfil 20223  df-cau 20224  df-cmet 20225  df-grpo 22800  df-gid 22801  df-ginv 22802  df-gdiv 22803  df-ablo 22891  df-subgo 22911  df-vc 23046  df-nv 23092  df-va 23095  df-ba 23096  df-sm 23097  df-0v 23098  df-vs 23099  df-nmcv 23100  df-ims 23101  df-dip 23218  df-ssp 23242  df-lno 23266  df-nmoo 23267  df-0o 23269  df-ph 23335  df-cbn 23386  df-hnorm 23492  df-hba 23493  df-hvsub 23495  df-hlim 23496  df-hcau 23497  df-sh 23731  df-ch 23746  df-oc 23777  df-ch0 23778  df-shs 23833  df-pjh 23920  df-h0op 24274  df-nmop 24365  df-cnop 24366  df-lnop 24367  df-bdop 24368  df-unop 24369  df-hmop 24370  df-nmfn 24371  df-nlfn 24372  df-cnfn 24373  df-lnfn 24374  df-adjh 24375
  Copyright terms: Public domain W3C validator