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 ⊢ y ∈ ℋ ⟼ y ⋅ ih x ∈ V
3 df-bra ⊢ bra = x ∈ ℋ ⟼ y ∈ ℋ ⟼ y ⋅ ih x
4 2 3 fnmpti ⊢ bra Fn ℋ
5 rnbra ⊢ ran ⁡ bra = LinFn ∩ ContFn
6 fveq1 ⊢ bra ⁡ x = bra ⁡ y → bra ⁡ x ⁡ z = bra ⁡ y ⁡ z
7 braval ⊢ x ∈ ℋ ∧ z ∈ ℋ → bra ⁡ x ⁡ z = z ⋅ ih x
8 7 adantlr ⊢ x ∈ ℋ ∧ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ x ⁡ z = z ⋅ ih x
9 braval ⊢ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ y ⁡ z = z ⋅ ih y
10 9 adantll ⊢ x ∈ ℋ ∧ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ y ⁡ z = z ⋅ ih y
11 8 10 eqeq12d ⊢ x ∈ ℋ ∧ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ x ⁡ z = bra ⁡ y ⁡ z ↔ z ⋅ ih x = z ⋅ ih y
12 6 11 imbitrid ⊢ x ∈ ℋ ∧ y ∈ ℋ ∧ z ∈ ℋ → bra ⁡ x = bra ⁡ y → z ⋅ ih x = z ⋅ ih y
13 12 ralrimdva ⊢ x ∈ ℋ ∧ y ∈ ℋ → bra ⁡ x = bra ⁡ y → ∀ z ∈ ℋ z ⋅ ih x = z ⋅ ih y
14 hial2eq2 ⊢ x ∈ ℋ ∧ y ∈ ℋ → ∀ z ∈ ℋ z ⋅ ih x = z ⋅ ih y ↔ x = y
15 13 14 sylibd ⊢ x ∈ ℋ ∧ y ∈ ℋ → bra ⁡ x = bra ⁡ y → x = y
16 15 rgen2 ⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ bra ⁡ x = bra ⁡ y → x = y
17 dff1o6 ⊢ bra : ℋ ⟶ 1-1 onto LinFn ∩ ContFn ↔ bra Fn ℋ ∧ ran ⁡ bra = LinFn ∩ ContFn ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ bra ⁡ x = bra ⁡ y → x = y
18 4 5 16 17 mpbir3an ⊢ bra : ℋ ⟶ 1-1 onto LinFn ∩ ContFn