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 ↔ norm fn ⁡ t ∈ ℝ
2 1 pm5.32i ⊢ t ∈ LinFn ∧ t ∈ ContFn ↔ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ
3 elin ⊢ t ∈ LinFn ∩ ContFn ↔ t ∈ LinFn ∧ t ∈ ContFn
4 ax-hilex ⊢ ℋ ∈ V
5 4 mptex ⊢ y ∈ ℋ ⟼ y ⋅ ih x ∈ V
6 df-bra ⊢ bra = x ∈ ℋ ⟼ y ∈ ℋ ⟼ y ⋅ ih x
7 5 6 fnmpti ⊢ bra Fn ℋ
8 fvelrnb ⊢ bra Fn ℋ → 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 ∈ ℋ → norm fn ⁡ bra ⁡ x ∈ ℝ
12 10 11 jca ⊢ x ∈ ℋ → bra ⁡ x ∈ LinFn ∧ norm fn ⁡ bra ⁡ x ∈ ℝ
13 eleq1 ⊢ bra ⁡ x = t → bra ⁡ x ∈ LinFn ↔ t ∈ LinFn
14 fveq2 ⊢ bra ⁡ x = t → norm fn ⁡ bra ⁡ x = norm fn ⁡ t
15 14 eleq1d ⊢ bra ⁡ x = t → norm fn ⁡ bra ⁡ x ∈ ℝ ↔ norm fn ⁡ t ∈ ℝ
16 13 15 anbi12d ⊢ bra ⁡ x = t → bra ⁡ x ∈ LinFn ∧ norm fn ⁡ bra ⁡ x ∈ ℝ ↔ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ
17 12 16 syl5ibcom ⊢ x ∈ ℋ → bra ⁡ x = t → t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ
18 17 rexlimiv ⊢ ∃ x ∈ ℋ bra ⁡ x = t → t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ
19 riesz1 ⊢ t ∈ LinFn → norm fn ⁡ t ∈ ℝ ↔ ∃ x ∈ ℋ ∀ y ∈ ℋ t ⁡ y = y ⋅ ih x
20 19 biimpa ⊢ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ → ∃ x ∈ ℋ ∀ y ∈ ℋ t ⁡ y = y ⋅ ih x
21 braval ⊢ x ∈ ℋ ∧ y ∈ ℋ → bra ⁡ x ⁡ y = y ⋅ ih x
22 eqtr3 ⊢ bra ⁡ x ⁡ y = y ⋅ ih x ∧ t ⁡ y = y ⋅ ih x → bra ⁡ x ⁡ y = t ⁡ y
23 22 ex ⊢ bra ⁡ x ⁡ y = y ⋅ ih x → t ⁡ y = y ⋅ ih x → bra ⁡ x ⁡ y = t ⁡ y
24 21 23 syl ⊢ x ∈ ℋ ∧ y ∈ ℋ → t ⁡ y = y ⋅ ih x → bra ⁡ x ⁡ y = t ⁡ y
25 24 ralimdva ⊢ x ∈ ℋ → ∀ y ∈ ℋ t ⁡ y = y ⋅ ih x → ∀ y ∈ ℋ bra ⁡ x ⁡ y = t ⁡ y
26 25 adantl ⊢ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ ∧ x ∈ ℋ → ∀ y ∈ ℋ t ⁡ y = y ⋅ ih x → ∀ y ∈ ℋ bra ⁡ x ⁡ y = t ⁡ y
27 brafn ⊢ x ∈ ℋ → bra ⁡ x : ℋ ⟶ ℂ
28 lnfnf ⊢ t ∈ LinFn → t : ℋ ⟶ ℂ
29 28 adantr ⊢ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ → t : ℋ ⟶ ℂ
30 ffn ⊢ bra ⁡ x : ℋ ⟶ ℂ → bra ⁡ x Fn ℋ
31 ffn ⊢ t : ℋ ⟶ ℂ → t Fn ℋ
32 eqfnfv ⊢ bra ⁡ x Fn ℋ ∧ t Fn ℋ → 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 ∧ norm fn ⁡ t ∈ ℝ ∧ x ∈ ℋ → bra ⁡ x = t ↔ ∀ y ∈ ℋ bra ⁡ x ⁡ y = t ⁡ y
35 26 34 sylibrd ⊢ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ ∧ x ∈ ℋ → ∀ y ∈ ℋ t ⁡ y = y ⋅ ih x → bra ⁡ x = t
36 35 reximdva ⊢ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ → ∃ x ∈ ℋ ∀ y ∈ ℋ t ⁡ y = y ⋅ ih x → ∃ x ∈ ℋ bra ⁡ x = t
37 20 36 mpd ⊢ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ → ∃ x ∈ ℋ bra ⁡ x = t
38 18 37 impbii ⊢ ∃ x ∈ ℋ bra ⁡ x = t ↔ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ
39 9 38 bitri ⊢ t ∈ ran ⁡ bra ↔ t ∈ LinFn ∧ norm fn ⁡ t ∈ ℝ
40 2 3 39 3bitr4ri ⊢ t ∈ ran ⁡ bra ↔ t ∈ LinFn ∩ ContFn
41 40 eqriv ⊢ ran ⁡ bra = LinFn ∩ ContFn