Metamath Proof Explorer

Theorem bracnlnval

Description: The vector that a continuous linear functional is the bra of. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion bracnlnval ⊢ T ∈ LinFn ∩ ContFn → T = bra ⁡ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y

Proof

Step Hyp Ref Expression
1 cnvbraval ⊢ T ∈ LinFn ∩ ContFn → bra -1 ⁡ T = ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
2 cnvbracl ⊢ T ∈ LinFn ∩ ContFn → bra -1 ⁡ T ∈ ℋ
3 1 2 eqeltrrd ⊢ T ∈ LinFn ∩ ContFn → ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y ∈ ℋ
4 bra11 ⊢ bra : ℋ ⟶ 1-1 onto LinFn ∩ ContFn
5 f1ocnvfvb ⊢ bra : ℋ ⟶ 1-1 onto LinFn ∩ ContFn ∧ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y ∈ ℋ ∧ T ∈ LinFn ∩ ContFn → bra ⁡ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y = T ↔ bra -1 ⁡ T = ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
6 4 5 mp3an1 ⊢ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y ∈ ℋ ∧ T ∈ LinFn ∩ ContFn → bra ⁡ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y = T ↔ bra -1 ⁡ T = ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
7 3 6 mpancom ⊢ T ∈ LinFn ∩ ContFn → bra ⁡ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y = T ↔ bra -1 ⁡ T = ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y
8 1 7 mpbird ⊢ T ∈ LinFn ∩ ContFn → bra ⁡ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y = T
9 8 eqcomd ⊢ T ∈ LinFn ∩ ContFn → T = bra ⁡ ι y ∈ ℋ | ∀ x ∈ ℋ T ⁡ x = x ⋅ ih y