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 e. ( LinFn i^i ContFn ) -> ( `' bra ` T ) = ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) )

Proof

Step Hyp Ref Expression
1 bra11 
 |-  bra : ~H -1-1-onto-> ( LinFn i^i ContFn )
2 f1ocnvfv 
 |-  ( ( bra : ~H -1-1-onto-> ( LinFn i^i ContFn ) /\ y e. ~H ) -> ( ( bra ` y ) = T -> ( `' bra ` T ) = y ) )
3 1 2 mpan 
 |-  ( y e. ~H -> ( ( bra ` y ) = T -> ( `' bra ` T ) = y ) )
4 3 imp 
 |-  ( ( y e. ~H /\ ( bra ` y ) = T ) -> ( `' bra ` T ) = y )
5 4 oveq2d 
 |-  ( ( y e. ~H /\ ( bra ` y ) = T ) -> ( x .ih ( `' bra ` T ) ) = ( x .ih y ) )
6 5 adantll 
 |-  ( ( ( ( T e. ( LinFn i^i ContFn ) /\ x e. ~H ) /\ y e. ~H ) /\ ( bra ` y ) = T ) -> ( x .ih ( `' bra ` T ) ) = ( x .ih y ) )
7 braval 
 |-  ( ( y e. ~H /\ x e. ~H ) -> ( ( bra ` y ) ` x ) = ( x .ih y ) )
8 7 ancoms 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( bra ` y ) ` x ) = ( x .ih y ) )
9 8 adantll 
 |-  ( ( ( T e. ( LinFn i^i ContFn ) /\ x e. ~H ) /\ y e. ~H ) -> ( ( bra ` y ) ` x ) = ( x .ih y ) )
10 9 adantr 
 |-  ( ( ( ( T e. ( LinFn i^i ContFn ) /\ x e. ~H ) /\ y e. ~H ) /\ ( bra ` y ) = T ) -> ( ( bra ` y ) ` x ) = ( x .ih y ) )
11 fveq1 
 |-  ( ( bra ` y ) = T -> ( ( bra ` y ) ` x ) = ( T ` x ) )
12 11 adantl 
 |-  ( ( ( ( T e. ( LinFn i^i ContFn ) /\ x e. ~H ) /\ y e. ~H ) /\ ( bra ` y ) = T ) -> ( ( bra ` y ) ` x ) = ( T ` x ) )
13 6 10 12 3eqtr2rd 
 |-  ( ( ( ( T e. ( LinFn i^i ContFn ) /\ x e. ~H ) /\ y e. ~H ) /\ ( bra ` y ) = T ) -> ( T ` x ) = ( x .ih ( `' bra ` T ) ) )
14 rnbra 
 |-  ran bra = ( LinFn i^i ContFn )
15 14 eleq2i 
 |-  ( T e. ran bra <-> T e. ( LinFn i^i ContFn ) )
16 f1of 
 |-  ( bra : ~H -1-1-onto-> ( LinFn i^i ContFn ) -> bra : ~H --> ( LinFn i^i ContFn ) )
17 1 16 ax-mp 
 |-  bra : ~H --> ( LinFn i^i ContFn )
18 ffn 
 |-  ( bra : ~H --> ( LinFn i^i ContFn ) -> bra Fn ~H )
19 17 18 ax-mp 
 |-  bra Fn ~H
20 fvelrnb 
 |-  ( bra Fn ~H -> ( T e. ran bra <-> E. y e. ~H ( bra ` y ) = T ) )
21 19 20 ax-mp 
 |-  ( T e. ran bra <-> E. y e. ~H ( bra ` y ) = T )
22 15 21 sylbb1 
 |-  ( T e. ( LinFn i^i ContFn ) -> E. y e. ~H ( bra ` y ) = T )
23 22 adantr 
 |-  ( ( T e. ( LinFn i^i ContFn ) /\ x e. ~H ) -> E. y e. ~H ( bra ` y ) = T )
24 13 23 r19.29a 
 |-  ( ( T e. ( LinFn i^i ContFn ) /\ x e. ~H ) -> ( T ` x ) = ( x .ih ( `' bra ` T ) ) )
25 24 ralrimiva 
 |-  ( T e. ( LinFn i^i ContFn ) -> A. x e. ~H ( T ` x ) = ( x .ih ( `' bra ` T ) ) )
26 f1ocnvdm 
 |-  ( ( bra : ~H -1-1-onto-> ( LinFn i^i ContFn ) /\ T e. ( LinFn i^i ContFn ) ) -> ( `' bra ` T ) e. ~H )
27 1 26 mpan 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( `' bra ` T ) e. ~H )
28 riesz4 
 |-  ( T e. ( LinFn i^i ContFn ) -> E! y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) )
29 oveq2 
 |-  ( y = ( `' bra ` T ) -> ( x .ih y ) = ( x .ih ( `' bra ` T ) ) )
30 29 eqeq2d 
 |-  ( y = ( `' bra ` T ) -> ( ( T ` x ) = ( x .ih y ) <-> ( T ` x ) = ( x .ih ( `' bra ` T ) ) ) )
31 30 ralbidv 
 |-  ( y = ( `' bra ` T ) -> ( A. x e. ~H ( T ` x ) = ( x .ih y ) <-> A. x e. ~H ( T ` x ) = ( x .ih ( `' bra ` T ) ) ) )
32 31 riota2 
 |-  ( ( ( `' bra ` T ) e. ~H /\ E! y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) -> ( A. x e. ~H ( T ` x ) = ( x .ih ( `' bra ` T ) ) <-> ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) = ( `' bra ` T ) ) )
33 27 28 32 syl2anc 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( A. x e. ~H ( T ` x ) = ( x .ih ( `' bra ` T ) ) <-> ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) = ( `' bra ` T ) ) )
34 25 33 mpbid 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) = ( `' bra ` T ) )
35 34 eqcomd 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( `' bra ` T ) = ( iota_ y e. ~H A. x e. ~H ( T ` x ) = ( x .ih y ) ) )