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 syl5ib ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 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 )