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 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 ∈ LinFn ∩ ContFn → bra -1 ⁡ T = ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y

Proof

Step Hyp Ref Expression
1 bra11 ⊢ bra : ℋ ⟶ 1-1 onto LinFn ∩ ContFn
2 f1ocnvfv ⊢ bra : ℋ ⟶ 1-1 onto LinFn ∩ ContFn ∧ y ∈ ℋ → bra ⁡ y = T → bra -1 ⁡ T = y
3 1 2 mpan ⊢ y ∈ ℋ → bra ⁡ y = T → bra -1 ⁡ T = y
4 3 imp ⊢ y ∈ ℋ ∧ bra ⁡ y = T → bra -1 ⁡ T = y
5 4 oveq2d ⊢ y ∈ ℋ ∧ bra ⁡ y = T → x ⋅ ih bra -1 ⁡ T = x ⋅ ih y
6 5 adantll ⊢ T ∈ LinFn ∩ ContFn ∧ x ∈ ℋ ∧ y ∈ ℋ ∧ bra ⁡ y = T → x ⋅ ih bra -1 ⁡ T = x ⋅ ih y
7 braval ⊢ y ∈ ℋ ∧ x ∈ ℋ → bra ⁡ y ⁡ x = x ⋅ ih y
8 7 ancoms ⊢ x ∈ ℋ ∧ y ∈ ℋ → bra ⁡ y ⁡ x = x ⋅ ih y
9 8 adantll ⊢ T ∈ LinFn ∩ ContFn ∧ x ∈ ℋ ∧ y ∈ ℋ → bra ⁡ y ⁡ x = x ⋅ ih y
10 9 adantr ⊢ T ∈ LinFn ∩ ContFn ∧ x ∈ ℋ ∧ y ∈ ℋ ∧ bra ⁡ y = T → bra ⁡ y ⁡ x = x ⋅ ih y
11 fveq1 ⊢ bra ⁡ y = T → bra ⁡ y ⁡ x = T ⁡ x
12 11 adantl ⊢ T ∈ LinFn ∩ ContFn ∧ x ∈ ℋ ∧ y ∈ ℋ ∧ bra ⁡ y = T → bra ⁡ y ⁡ x = T ⁡ x
13 6 10 12 3eqtr2rd ⊢ T ∈ LinFn ∩ ContFn ∧ x ∈ ℋ ∧ y ∈ ℋ ∧ bra ⁡ y = T → T ⁡ x = x ⋅ ih bra -1 ⁡ T
14 rnbra ⊢ ran ⁡ bra = LinFn ∩ ContFn
15 14 eleq2i ⊢ T ∈ ran ⁡ bra ↔ T ∈ 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 ℋ → T ∈ ran ⁡ bra ↔ ∃ y ∈ ℋ bra ⁡ y = T
21 19 20 ax-mp ⊢ T ∈ ran ⁡ bra ↔ ∃ y ∈ ℋ bra ⁡ y = T
22 15 21 sylbb1 ⊢ T ∈ LinFn ∩ ContFn → ∃ y ∈ ℋ bra ⁡ y = T
23 22 adantr ⊢ T ∈ LinFn ∩ ContFn ∧ x ∈ ℋ → ∃ y ∈ ℋ bra ⁡ y = T
24 13 23 r19.29a ⊢ T ∈ LinFn ∩ ContFn ∧ x ∈ ℋ → T ⁡ x = x ⋅ ih bra -1 ⁡ T
25 24 ralrimiva ⊢ T ∈ LinFn ∩ ContFn → ∀ x ∈ ℋ T ⁡ x = x ⋅ ih bra -1 ⁡ T
26 f1ocnvdm ⊢ bra : ℋ ⟶ 1-1 onto LinFn ∩ ContFn ∧ T ∈ LinFn ∩ ContFn → bra -1 ⁡ T ∈ ℋ
27 1 26 mpan ⊢ T ∈ LinFn ∩ ContFn → bra -1 ⁡ T ∈ ℋ
28 riesz4 ⊢ T ∈ LinFn ∩ ContFn → ∃! y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
29 oveq2 ⊢ y = bra -1 ⁡ T → x ⋅ ih y = x ⋅ ih bra -1 ⁡ T
30 29 eqeq2d ⊢ y = bra -1 ⁡ T → T ⁡ x = x ⋅ ih y ↔ T ⁡ x = x ⋅ ih bra -1 ⁡ T
31 30 ralbidv ⊢ y = bra -1 ⁡ T → ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y ↔ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih bra -1 ⁡ T
32 31 riota2 ⊢ bra -1 ⁡ T ∈ ℋ ∧ ∃! y ∈ ℋ ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y → ∀ x ∈ ℋ T ⁡ x = x ⋅ ih bra -1 ⁡ T ↔ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y = bra -1 ⁡ T
33 27 28 32 syl2anc ⊢ T ∈ LinFn ∩ ContFn → ∀ x ∈ ℋ T ⁡ x = x ⋅ ih bra -1 ⁡ T ↔ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y = bra -1 ⁡ T
34 25 33 mpbid ⊢ T ∈ LinFn ∩ ContFn → ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y = bra -1 ⁡ T
35 34 eqcomd ⊢ T ∈ LinFn ∩ ContFn → bra -1 ⁡ T = ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y