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

Metamath Proof Explorer

Theorem bra11

Description: The bra function maps vectors one-to-one onto the set of continuous linear functionals. (Contributed by NM, 26-May-2006) (Proof shortened by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion bra11 bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn )

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 1 mptex ⊢ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) ∈ V
3 df-bra ⊢ bra = ( 𝑥 ∈ ℋ ↦ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) )
4 2 3 fnmpti ⊢ bra Fn ℋ
5 rnbra ⊢ ran bra = ( LinFn ∩ ContFn )
6 fveq1 ⊢ ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → ( ( bra ‘ 𝑥 ) ‘ 𝑧 ) = ( ( bra ‘ 𝑦 ) ‘ 𝑧 ) )
7 braval ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) ‘ 𝑧 ) = ( 𝑧 ·ih 𝑥 ) )
8 7 adantlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) ‘ 𝑧 ) = ( 𝑧 ·ih 𝑥 ) )
9 braval ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑦 ) ‘ 𝑧 ) = ( 𝑧 ·ih 𝑦 ) )
10 9 adantll ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑦 ) ‘ 𝑧 ) = ( 𝑧 ·ih 𝑦 ) )
11 8 10 eqeq12d ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( ( bra ‘ 𝑥 ) ‘ 𝑧 ) = ( ( bra ‘ 𝑦 ) ‘ 𝑧 ) ↔ ( 𝑧 ·ih 𝑥 ) = ( 𝑧 ·ih 𝑦 ) ) )
12 6 11 imbitrid ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → ( 𝑧 ·ih 𝑥 ) = ( 𝑧 ·ih 𝑦 ) ) )
13 12 ralrimdva ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → ∀ 𝑧 ∈ ℋ ( 𝑧 ·ih 𝑥 ) = ( 𝑧 ·ih 𝑦 ) ) )
14 hial2eq2 ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ∀ 𝑧 ∈ ℋ ( 𝑧 ·ih 𝑥 ) = ( 𝑧 ·ih 𝑦 ) ↔ 𝑥 = 𝑦 ) )
15 13 14 sylibd ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
16 15 rgen2 ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → 𝑥 = 𝑦 )
17 dff1o6 ⊢ ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) ↔ ( bra Fn ℋ ∧ ran bra = ( LinFn ∩ ContFn ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
18 4 5 16 17 mpbir3an ⊢ bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn )