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 ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ◡ bra ‘ 𝑇 ) = ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 bra11 ⊢ bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn )
2 f1ocnvfv ⊢ ( ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝑦 ) = 𝑇 → ( ◡ bra ‘ 𝑇 ) = 𝑦 ) )
3 1 2 mpan ⊢ ( 𝑦 ∈ ℋ → ( ( bra ‘ 𝑦 ) = 𝑇 → ( ◡ bra ‘ 𝑇 ) = 𝑦 ) )
4 3 imp ⊢ ( ( 𝑦 ∈ ℋ ∧ ( bra ‘ 𝑦 ) = 𝑇 ) → ( ◡ bra ‘ 𝑇 ) = 𝑦 )
5 4 oveq2d ⊢ ( ( 𝑦 ∈ ℋ ∧ ( bra ‘ 𝑦 ) = 𝑇 ) → ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) = ( 𝑥 ·ih 𝑦 ) )
6 5 adantll ⊢ ( ( ( ( 𝑇 ∈ ( LinFn ∩ ContFn ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( bra ‘ 𝑦 ) = 𝑇 ) → ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) = ( 𝑥 ·ih 𝑦 ) )
7 braval ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )
8 7 ancoms ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )
9 8 adantll ⊢ ( ( ( 𝑇 ∈ ( LinFn ∩ ContFn ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )
10 9 adantr ⊢ ( ( ( ( 𝑇 ∈ ( LinFn ∩ ContFn ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( bra ‘ 𝑦 ) = 𝑇 ) → ( ( bra ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )
11 fveq1 ⊢ ( ( bra ‘ 𝑦 ) = 𝑇 → ( ( bra ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
12 11 adantl ⊢ ( ( ( ( 𝑇 ∈ ( LinFn ∩ ContFn ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( bra ‘ 𝑦 ) = 𝑇 ) → ( ( bra ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
13 6 10 12 3eqtr2rd ⊢ ( ( ( ( 𝑇 ∈ ( LinFn ∩ ContFn ) ∧ 𝑥 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) ∧ ( bra ‘ 𝑦 ) = 𝑇 ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) )
14 rnbra ⊢ ran bra = ( LinFn ∩ ContFn )
15 14 eleq2i ⊢ ( 𝑇 ∈ ran bra ↔ 𝑇 ∈ ( LinFn ∩ ContFn ) )
16 f1of ⊢ ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) → bra : ℋ ⟶ ( LinFn ∩ ContFn ) )
17 1 16 ax-mp ⊢ bra : ℋ ⟶ ( LinFn ∩ ContFn )
18 ffn ⊢ ( bra : ℋ ⟶ ( LinFn ∩ ContFn ) → bra Fn ℋ )
19 17 18 ax-mp ⊢ bra Fn ℋ
20 fvelrnb ⊢ ( bra Fn ℋ → ( 𝑇 ∈ ran bra ↔ ∃ 𝑦 ∈ ℋ ( bra ‘ 𝑦 ) = 𝑇 ) )
21 19 20 ax-mp ⊢ ( 𝑇 ∈ ran bra ↔ ∃ 𝑦 ∈ ℋ ( bra ‘ 𝑦 ) = 𝑇 )
22 15 21 sylbb1 ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ∃ 𝑦 ∈ ℋ ( bra ‘ 𝑦 ) = 𝑇 )
23 22 adantr ⊢ ( ( 𝑇 ∈ ( LinFn ∩ ContFn ) ∧ 𝑥 ∈ ℋ ) → ∃ 𝑦 ∈ ℋ ( bra ‘ 𝑦 ) = 𝑇 )
24 13 23 r19.29a ⊢ ( ( 𝑇 ∈ ( LinFn ∩ ContFn ) ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) )
25 24 ralrimiva ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) )
26 f1ocnvdm ⊢ ( ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ◡ bra ‘ 𝑇 ) ∈ ℋ )
27 1 26 mpan ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ◡ bra ‘ 𝑇 ) ∈ ℋ )
28 riesz4 ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ∃! 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) )
29 oveq2 ⊢ ( 𝑦 = ( ◡ bra ‘ 𝑇 ) → ( 𝑥 ·ih 𝑦 ) = ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) )
30 29 eqeq2d ⊢ ( 𝑦 = ( ◡ bra ‘ 𝑇 ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ↔ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) ) )
31 30 ralbidv ⊢ ( 𝑦 = ( ◡ bra ‘ 𝑇 ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) ) )
32 31 riota2 ⊢ ( ( ( ◡ bra ‘ 𝑇 ) ∈ ℋ ∧ ∃! 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) ↔ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) = ( ◡ bra ‘ 𝑇 ) ) )
33 27 28 32 syl2anc ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih ( ◡ bra ‘ 𝑇 ) ) ↔ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) = ( ◡ bra ‘ 𝑇 ) ) )
34 25 33 mpbid ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) = ( ◡ bra ‘ 𝑇 ) )
35 34 eqcomd ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ◡ bra ‘ 𝑇 ) = ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) )