Metamath Proof Explorer

Theorem rnbra

Description: The set of bras equals the set of continuous linear functionals. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion rnbra ⊢ran⁡bra=LinFn∩ContFn

Proof

Step Hyp Ref Expression
1 lnfncnbd ⊢t∈LinFn→t∈ContFn↔normfn⁡t∈ℝ
2 1 pm5.32i ⊢t∈LinFn∧t∈ContFn↔t∈LinFn∧normfn⁡t∈ℝ
3 elin ⊢t∈LinFn∩ContFn↔t∈LinFn∧t∈ContFn
4 ax-hilex ⊢ℋ∈V
5 4 mptex ⊢y∈ℋ⟼y⋅ihx∈V
6 df-bra ⊢bra=x∈ℋ⟼y∈ℋ⟼y⋅ihx
7 5 6 fnmpti ⊢braFnℋ
8 fvelrnb ⊢braFnℋ→t∈ran⁡bra↔∃x∈ℋbra⁡x=t
9 7 8 ax-mp ⊢t∈ran⁡bra↔∃x∈ℋbra⁡x=t
10 bralnfn ⊢x∈ℋ→bra⁡x∈LinFn
11 brabn ⊢x∈ℋ→normfn⁡bra⁡x∈ℝ
12 10 11 jca ⊢x∈ℋ→bra⁡x∈LinFn∧normfn⁡bra⁡x∈ℝ
13 eleq1 ⊢bra⁡x=t→bra⁡x∈LinFn↔t∈LinFn
14 fveq2 ⊢bra⁡x=t→normfn⁡bra⁡x=normfn⁡t
15 14 eleq1d ⊢bra⁡x=t→normfn⁡bra⁡x∈ℝ↔normfn⁡t∈ℝ
16 13 15 anbi12d ⊢bra⁡x=t→bra⁡x∈LinFn∧normfn⁡bra⁡x∈ℝ↔t∈LinFn∧normfn⁡t∈ℝ
17 12 16 syl5ibcom ⊢x∈ℋ→bra⁡x=t→t∈LinFn∧normfn⁡t∈ℝ
18 17 rexlimiv ⊢∃x∈ℋbra⁡x=t→t∈LinFn∧normfn⁡t∈ℝ
19 riesz1 ⊢t∈LinFn→normfn⁡t∈ℝ↔∃x∈ℋ∀y∈ℋt⁡y=y⋅ihx
20 19 biimpa ⊢t∈LinFn∧normfn⁡t∈ℝ→∃x∈ℋ∀y∈ℋt⁡y=y⋅ihx
21 braval ⊢x∈ℋ∧y∈ℋ→bra⁡x⁡y=y⋅ihx
22 eqtr3 ⊢bra⁡x⁡y=y⋅ihx∧t⁡y=y⋅ihx→bra⁡x⁡y=t⁡y
23 22 ex ⊢bra⁡x⁡y=y⋅ihx→t⁡y=y⋅ihx→bra⁡x⁡y=t⁡y
24 21 23 syl ⊢x∈ℋ∧y∈ℋ→t⁡y=y⋅ihx→bra⁡x⁡y=t⁡y
25 24 ralimdva ⊢x∈ℋ→∀y∈ℋt⁡y=y⋅ihx→∀y∈ℋbra⁡x⁡y=t⁡y
26 25 adantl ⊢t∈LinFn∧normfn⁡t∈ℝ∧x∈ℋ→∀y∈ℋt⁡y=y⋅ihx→∀y∈ℋbra⁡x⁡y=t⁡y
27 brafn ⊢x∈ℋ→bra⁡x:ℋ⟶ℂ
28 lnfnf ⊢t∈LinFn→t:ℋ⟶ℂ
29 28 adantr ⊢t∈LinFn∧normfn⁡t∈ℝ→t:ℋ⟶ℂ
30 ffn ⊢bra⁡x:ℋ⟶ℂ→bra⁡xFnℋ
31 ffn ⊢t:ℋ⟶ℂ→tFnℋ
32 eqfnfv ⊢bra⁡xFnℋ∧tFnℋ→bra⁡x=t↔∀y∈ℋbra⁡x⁡y=t⁡y
33 30 31 32 syl2an ⊢bra⁡x:ℋ⟶ℂ∧t:ℋ⟶ℂ→bra⁡x=t↔∀y∈ℋbra⁡x⁡y=t⁡y
34 27 29 33 syl2anr ⊢t∈LinFn∧normfn⁡t∈ℝ∧x∈ℋ→bra⁡x=t↔∀y∈ℋbra⁡x⁡y=t⁡y
35 26 34 sylibrd ⊢t∈LinFn∧normfn⁡t∈ℝ∧x∈ℋ→∀y∈ℋt⁡y=y⋅ihx→bra⁡x=t
36 35 reximdva ⊢t∈LinFn∧normfn⁡t∈ℝ→∃x∈ℋ∀y∈ℋt⁡y=y⋅ihx→∃x∈ℋbra⁡x=t
37 20 36 mpd ⊢t∈LinFn∧normfn⁡t∈ℝ→∃x∈ℋbra⁡x=t
38 18 37 impbii ⊢∃x∈ℋbra⁡x=t↔t∈LinFn∧normfn⁡t∈ℝ
39 9 38 bitri ⊢t∈ran⁡bra↔t∈LinFn∧normfn⁡t∈ℝ
40 2 3 39 3bitr4ri ⊢t∈ran⁡bra↔t∈LinFn∩ContFn
41 40 eqriv ⊢ran⁡bra=LinFn∩ContFn