Theorem bra11 31170

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	⊢ bra: ℋ–1-1-onto→(LinFn ∩ ContFn)

Proof of Theorem bra11

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-hilex 30061	. . . 4 ⊢ ℋ ∈ V
2	1	mptex 7204	. . 3 ⊢ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)) ∈ V
3		df-bra 30912	. . 3 ⊢ bra = (𝑥 ∈ ℋ ↦ (𝑦 ∈ ℋ ↦ (𝑦 ·ih 𝑥)))
4	2, 3	fnmpti 6675	. 2 ⊢ bra Fn ℋ
5		rnbra 31169	. 2 ⊢ ran bra = (LinFn ∩ ContFn)
6		fveq1 6872	. . . . . 6 ⊢ ((bra‘𝑥) = (bra‘𝑦) → ((bra‘𝑥)‘𝑧) = ((bra‘𝑦)‘𝑧))
7		braval 31006	. . . . . . . 8 ⊢ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((bra‘𝑥)‘𝑧) = (𝑧 ·ih 𝑥))
8	7	adantlr 713	. . . . . . 7 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((bra‘𝑥)‘𝑧) = (𝑧 ·ih 𝑥))
9		braval 31006	. . . . . . . 8 ⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((bra‘𝑦)‘𝑧) = (𝑧 ·ih 𝑦))
10	9	adantll 712	. . . . . . 7 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((bra‘𝑦)‘𝑧) = (𝑧 ·ih 𝑦))
11	8, 10	eqeq12d 2747	. . . . . 6 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (((bra‘𝑥)‘𝑧) = ((bra‘𝑦)‘𝑧) ↔ (𝑧 ·ih 𝑥) = (𝑧 ·ih 𝑦)))
12	6, 11	imbitrid 243	. . . . 5 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((bra‘𝑥) = (bra‘𝑦) → (𝑧 ·ih 𝑥) = (𝑧 ·ih 𝑦)))
13	12	ralrimdva 3153	. . . 4 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((bra‘𝑥) = (bra‘𝑦) → ∀𝑧 ∈ ℋ (𝑧 ·ih 𝑥) = (𝑧 ·ih 𝑦)))
14		hial2eq2 30169	. . . 4 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (∀𝑧 ∈ ℋ (𝑧 ·ih 𝑥) = (𝑧 ·ih 𝑦) ↔ 𝑥 = 𝑦))
15	13, 14	sylibd 238	. . 3 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((bra‘𝑥) = (bra‘𝑦) → 𝑥 = 𝑦))
16	15	rgen2 3196	. 2 ⊢ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((bra‘𝑥) = (bra‘𝑦) → 𝑥 = 𝑦)
17		dff1o6 7252	. 2 ⊢ (bra: ℋ–1-1-onto→(LinFn ∩ ContFn) ↔ (bra Fn ℋ ∧ ran bra = (LinFn ∩ ContFn) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ ((bra‘𝑥) = (bra‘𝑦) → 𝑥 = 𝑦)))
18	4, 5, 16, 17	mpbir3an 1341	1 ⊢ bra: ℋ–1-1-onto→(LinFn ∩ ContFn)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3060   ∩ cin 3938   ↦ cmpt 5219  ran crn 5665   Fn wfn 6522  –1-1-onto→wf1o 6526  ‘cfv 6527  (class class class)co 7388   ℋchba 29981   ·_ih csp 29984  ContFnccnfn 30015  LinFnclf 30016  bracbr 30018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5273  ax-sep 5287  ax-nul 5294  ax-pow 5351  ax-pr 5415  ax-un 7703  ax-inf2 9613  ax-cc 10407  ax-cnex 11143  ax-resscn 11144  ax-1cn 11145  ax-icn 11146  ax-addcl 11147  ax-addrcl 11148  ax-mulcl 11149  ax-mulrcl 11150  ax-mulcom 11151  ax-addass 11152  ax-mulass 11153  ax-distr 11154  ax-i2m1 11155  ax-1ne0 11156  ax-1rid 11157  ax-rnegex 11158  ax-rrecex 11159  ax-cnre 11160  ax-pre-lttri 11161  ax-pre-lttrn 11162  ax-pre-ltadd 11163  ax-pre-mulgt0 11164  ax-pre-sup 11165  ax-addf 11166  ax-mulf 11167  ax-hilex 30061  ax-hfvadd 30062  ax-hvcom 30063  ax-hvass 30064  ax-hv0cl 30065  ax-hvaddid 30066  ax-hfvmul 30067  ax-hvmulid 30068  ax-hvmulass 30069  ax-hvdistr1 30070  ax-hvdistr2 30071  ax-hvmul0 30072  ax-hfi 30141  ax-his1 30144  ax-his2 30145  ax-his3 30146  ax-his4 30147  ax-hcompl 30264

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3374  df-reu 3375  df-rab 3429  df-v 3471  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3958  df-nul 4314  df-if 4518  df-pw 4593  df-sn 4618  df-pr 4620  df-tp 4622  df-op 4624  df-uni 4897  df-int 4939  df-iun 4987  df-iin 4988  df-br 5137  df-opab 5199  df-mpt 5220  df-tr 5254  df-id 5562  df-eprel 5568  df-po 5576  df-so 5577  df-fr 5619  df-se 5620  df-we 5621  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6284  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-isom 6536  df-riota 7344  df-ov 7391  df-oprab 7392  df-mpo 7393  df-of 7648  df-om 7834  df-1st 7952  df-2nd 7953  df-supp 8124  df-frecs 8243  df-wrecs 8274  df-recs 8348  df-rdg 8387  df-1o 8443  df-2o 8444  df-oadd 8447  df-omul 8448  df-er 8681  df-map 8800  df-pm 8801  df-ixp 8870  df-en 8918  df-dom 8919  df-sdom 8920  df-fin 8921  df-fsupp 9340  df-fi 9383  df-sup 9414  df-inf 9415  df-oi 9482  df-card 9911  df-acn 9914  df-pnf 11227  df-mnf 11228  df-xr 11229  df-ltxr 11230  df-le 11231  df-sub 11423  df-neg 11424  df-div 11849  df-nn 12190  df-2 12252  df-3 12253  df-4 12254  df-5 12255  df-6 12256  df-7 12257  df-8 12258  df-9 12259  df-n0 12450  df-z 12536  df-dec 12655  df-uz 12800  df-q 12910  df-rp 12952  df-xneg 13069  df-xadd 13070  df-xmul 13071  df-ioo 13305  df-ico 13307  df-icc 13308  df-fz 13462  df-fzo 13605  df-fl 13734  df-seq 13944  df-exp 14005  df-hash 14268  df-cj 15023  df-re 15024  df-im 15025  df-sqrt 15159  df-abs 15160  df-clim 15409  df-rlim 15410  df-sum 15610  df-struct 17057  df-sets 17074  df-slot 17092  df-ndx 17104  df-base 17122  df-ress 17151  df-plusg 17187  df-mulr 17188  df-starv 17189  df-sca 17190  df-vsca 17191  df-ip 17192  df-tset 17193  df-ple 17194  df-ds 17196  df-unif 17197  df-hom 17198  df-cco 17199  df-rest 17345  df-topn 17346  df-0g 17364  df-gsum 17365  df-topgen 17366  df-pt 17367  df-prds 17370  df-xrs 17425  df-qtop 17430  df-imas 17431  df-xps 17433  df-mre 17507  df-mrc 17508  df-acs 17510  df-mgm 18538  df-sgrp 18587  df-mnd 18598  df-submnd 18643  df-mulg 18918  df-cntz 19142  df-cmn 19609  df-psmet 20863  df-xmet 20864  df-met 20865  df-bl 20866  df-mopn 20867  df-fbas 20868  df-fg 20869  df-cnfld 20872  df-top 22318  df-topon 22335  df-topsp 22357  df-bases 22371  df-cld 22445  df-ntr 22446  df-cls 22447  df-nei 22524  df-cn 22653  df-cnp 22654  df-lm 22655  df-t1 22740  df-haus 22741  df-tx 22988  df-hmeo 23181  df-fil 23272  df-fm 23364  df-flim 23365  df-flf 23366  df-xms 23748  df-ms 23749  df-tms 23750  df-cfil 24694  df-cau 24695  df-cmet 24696  df-grpo 29555  df-gid 29556  df-ginv 29557  df-gdiv 29558  df-ablo 29607  df-vc 29621  df-nv 29654  df-va 29657  df-ba 29658  df-sm 29659  df-0v 29660  df-vs 29661  df-nmcv 29662  df-ims 29663  df-dip 29763  df-ssp 29784  df-ph 29875  df-cbn 29925  df-hnorm 30030  df-hba 30031  df-hvsub 30033  df-hlim 30034  df-hcau 30035  df-sh 30269  df-ch 30283  df-oc 30314  df-ch0 30315  df-nmfn 30907  df-nlfn 30908  df-cnfn 30909  df-lnfn 30910  df-bra 30912

This theorem is referenced by:  bracnln  31171  cnvbraval  31172  cnvbracl  31173  cnvbrabra  31174  bracnvbra  31175  bracnlnval  31176