# Metamath Proof Explorer

## Theorem cnvbraval

Description: Value of the converse of the bra function. Based on the Riesz Lemma riesz4 , this very important theorem not only justifies the Dirac bra-ket notation, but allows us to extract a unique vector from any continuous linear functional from which the functional can be recovered; i.e. a single vector can "store"all of the information contained in any entire continuous linear functional (mapping from ~H to CC ). (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion cnvbraval ${⊢}{T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to {\mathrm{bra}}^{-1}\left({T}\right)=\left(\iota {y}\in ℋ|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}\right)$

### Proof

Step Hyp Ref Expression
1 bra11 ${⊢}\mathrm{bra}:ℋ\underset{1-1 onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}$
2 f1ocnvfv ${⊢}\left(\mathrm{bra}:ℋ\underset{1-1 onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}\wedge {y}\in ℋ\right)\to \left(\mathrm{bra}\left({y}\right)={T}\to {\mathrm{bra}}^{-1}\left({T}\right)={y}\right)$
3 1 2 mpan ${⊢}{y}\in ℋ\to \left(\mathrm{bra}\left({y}\right)={T}\to {\mathrm{bra}}^{-1}\left({T}\right)={y}\right)$
4 3 imp ${⊢}\left({y}\in ℋ\wedge \mathrm{bra}\left({y}\right)={T}\right)\to {\mathrm{bra}}^{-1}\left({T}\right)={y}$
5 4 oveq2d ${⊢}\left({y}\in ℋ\wedge \mathrm{bra}\left({y}\right)={T}\right)\to {x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
6 5 adantll ${⊢}\left(\left(\left({T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\wedge {x}\in ℋ\right)\wedge {y}\in ℋ\right)\wedge \mathrm{bra}\left({y}\right)={T}\right)\to {x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
7 braval ${⊢}\left({y}\in ℋ\wedge {x}\in ℋ\right)\to \mathrm{bra}\left({y}\right)\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
8 7 ancoms ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to \mathrm{bra}\left({y}\right)\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
9 8 adantll ${⊢}\left(\left({T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\wedge {x}\in ℋ\right)\wedge {y}\in ℋ\right)\to \mathrm{bra}\left({y}\right)\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
10 9 adantr ${⊢}\left(\left(\left({T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\wedge {x}\in ℋ\right)\wedge {y}\in ℋ\right)\wedge \mathrm{bra}\left({y}\right)={T}\right)\to \mathrm{bra}\left({y}\right)\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
11 fveq1 ${⊢}\mathrm{bra}\left({y}\right)={T}\to \mathrm{bra}\left({y}\right)\left({x}\right)={T}\left({x}\right)$
12 11 adantl ${⊢}\left(\left(\left({T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\wedge {x}\in ℋ\right)\wedge {y}\in ℋ\right)\wedge \mathrm{bra}\left({y}\right)={T}\right)\to \mathrm{bra}\left({y}\right)\left({x}\right)={T}\left({x}\right)$
13 6 10 12 3eqtr2rd ${⊢}\left(\left(\left({T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\wedge {x}\in ℋ\right)\wedge {y}\in ℋ\right)\wedge \mathrm{bra}\left({y}\right)={T}\right)\to {T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)$
14 rnbra ${⊢}\mathrm{ran}\mathrm{bra}=\mathrm{LinFn}\cap \mathrm{ContFn}$
15 14 eleq2i ${⊢}{T}\in \mathrm{ran}\mathrm{bra}↔{T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)$
16 f1of ${⊢}\mathrm{bra}:ℋ\underset{1-1 onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}\to \mathrm{bra}:ℋ⟶\mathrm{LinFn}\cap \mathrm{ContFn}$
17 1 16 ax-mp ${⊢}\mathrm{bra}:ℋ⟶\mathrm{LinFn}\cap \mathrm{ContFn}$
18 ffn ${⊢}\mathrm{bra}:ℋ⟶\mathrm{LinFn}\cap \mathrm{ContFn}\to \mathrm{bra}Fnℋ$
19 17 18 ax-mp ${⊢}\mathrm{bra}Fnℋ$
20 fvelrnb ${⊢}\mathrm{bra}Fnℋ\to \left({T}\in \mathrm{ran}\mathrm{bra}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\mathrm{bra}\left({y}\right)={T}\right)$
21 19 20 ax-mp ${⊢}{T}\in \mathrm{ran}\mathrm{bra}↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\mathrm{bra}\left({y}\right)={T}$
22 15 21 sylbb1 ${⊢}{T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\mathrm{bra}\left({y}\right)={T}$
23 22 adantr ${⊢}\left({T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\wedge {x}\in ℋ\right)\to \exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\mathrm{bra}\left({y}\right)={T}$
24 13 23 r19.29a ${⊢}\left({T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\wedge {x}\in ℋ\right)\to {T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)$
25 24 ralrimiva ${⊢}{T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)$
26 f1ocnvdm ${⊢}\left(\mathrm{bra}:ℋ\underset{1-1 onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}\wedge {T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\right)\to {\mathrm{bra}}^{-1}\left({T}\right)\in ℋ$
27 1 26 mpan ${⊢}{T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to {\mathrm{bra}}^{-1}\left({T}\right)\in ℋ$
28 riesz4 ${⊢}{T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \exists !{y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
29 oveq2 ${⊢}{y}={\mathrm{bra}}^{-1}\left({T}\right)\to {x}{\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)$
30 29 eqeq2d ${⊢}{y}={\mathrm{bra}}^{-1}\left({T}\right)\to \left({T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}↔{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)\right)$
31 30 ralbidv ${⊢}{y}={\mathrm{bra}}^{-1}\left({T}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)\right)$
32 31 riota2 ${⊢}\left({\mathrm{bra}}^{-1}\left({T}\right)\in ℋ\wedge \exists !{y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)↔\left(\iota {y}\in ℋ|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}\right)={\mathrm{bra}}^{-1}\left({T}\right)\right)$
33 27 28 32 syl2anc ${⊢}{T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{\mathrm{bra}}^{-1}\left({T}\right)↔\left(\iota {y}\in ℋ|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}\right)={\mathrm{bra}}^{-1}\left({T}\right)\right)$
34 25 33 mpbid ${⊢}{T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \left(\iota {y}\in ℋ|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}\right)={\mathrm{bra}}^{-1}\left({T}\right)$
35 34 eqcomd ${⊢}{T}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to {\mathrm{bra}}^{-1}\left({T}\right)=\left(\iota {y}\in ℋ|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{y}\right)$