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 𝑦 ) ) ) )