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

Theorem bra11 23647
Description: The bra function maps vectors one-to-one onto the set of continuous linear functionals. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
Assertion
Ref Expression
bra11

Proof of Theorem bra11
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-hilex 22538 . . . 4
21mptex 6018 . . 3
3 df-bra 23389 . . 3
42, 3fnmpti 5624 . 2
5 rnbra 23646 . 2
6 fveq1 5778 . . . . . 6
7 braval 23483 . . . . . . . 8
87adantlr 697 . . . . . . 7
9 braval 23483 . . . . . . . 8
109adantll 696 . . . . . . 7
118, 10eqeq12d 2461 . . . . . 6
126, 11syl5ib 212 . . . . 5
1312ralrimdva 2807 . . . 4
14 hial2eq2 22645 . . . 4
1513, 14sylibd 207 . . 3
1615rgen2a 2783 . 2
17 dff1o6 6065 . 2
184, 5, 16, 17mpbir3an 1137 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  =wceq 1654  e.wcel 1728  A.wral 2716  i^icin 3312  e.cmpt 4305  rancrn 4924  Fnwfn 5500  -1-1-onto->wf1o 5504  `cfv 5505  (class class class)co 6133   chil 22458   csp 22461   ccnfn 22492   clf 22493   cbr 22495
This theorem is referenced by:  bracnln  23648  cnvbraval  23649  cnvbracl  23650  cnvbrabra  23651  bracnvbra  23652  bracnlnval  23653
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-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-nmfn 23384  df-nlfn 23385  df-cnfn 23386  df-lnfn 23387  df-bra 23389
  Copyright terms: Public domain W3C validator