This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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