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 ( 𝑇 ∈ ( LinFn ∩ ContFn ) → 𝑇 = ( bra ‘ ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 cnvbraval ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( bra ‘ 𝑇 ) = ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) )
2 cnvbracl ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( bra ‘ 𝑇 ) ∈ ℋ )
3 1 2 eqeltrrd ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ∈ ℋ )
4 bra11 bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn )
5 f1ocnvfvb ( ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) ∧ ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ∈ ℋ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ( bra ‘ ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) = 𝑇 ↔ ( bra ‘ 𝑇 ) = ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) )
6 4 5 mp3an1 ( ( ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ∈ ℋ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ( bra ‘ ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) = 𝑇 ↔ ( bra ‘ 𝑇 ) = ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) )
7 3 6 mpancom ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ( bra ‘ ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) = 𝑇 ↔ ( bra ‘ 𝑇 ) = ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) )
8 1 7 mpbird ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( bra ‘ ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) = 𝑇 )
9 8 eqcomd ( 𝑇 ∈ ( LinFn ∩ ContFn ) → 𝑇 = ( bra ‘ ( 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( 𝑥 ·ih 𝑦 ) ) ) )