This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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