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	⊢ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) ∈ V
3		df-bra	⊢ bra = ( 𝑥 ∈ ℋ ↦ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) )
4	2 3	fnmpti	⊢ bra Fn ℋ
5		rnbra	⊢ ran bra = ( LinFn ∩ ContFn )
6		fveq1	⊢ ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → ( ( bra ‘ 𝑥 ) ‘ 𝑧 ) = ( ( bra ‘ 𝑦 ) ‘ 𝑧 ) )
7		braval	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) ‘ 𝑧 ) = ( 𝑧 ·ih 𝑥 ) )
8	7	adantlr	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) ‘ 𝑧 ) = ( 𝑧 ·ih 𝑥 ) )
9		braval	⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑦 ) ‘ 𝑧 ) = ( 𝑧 ·ih 𝑦 ) )
10	9	adantll	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑦 ) ‘ 𝑧 ) = ( 𝑧 ·ih 𝑦 ) )
11	8 10	eqeq12d	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( ( bra ‘ 𝑥 ) ‘ 𝑧 ) = ( ( bra ‘ 𝑦 ) ‘ 𝑧 ) ↔ ( 𝑧 ·ih 𝑥 ) = ( 𝑧 ·ih 𝑦 ) ) )
12	6 11	imbitrid	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → ( 𝑧 ·ih 𝑥 ) = ( 𝑧 ·ih 𝑦 ) ) )
13	12	ralrimdva	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → ∀ 𝑧 ∈ ℋ ( 𝑧 ·ih 𝑥 ) = ( 𝑧 ·ih 𝑦 ) ) )
14		hial2eq2	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ∀ 𝑧 ∈ ℋ ( 𝑧 ·ih 𝑥 ) = ( 𝑧 ·ih 𝑦 ) ↔ 𝑥 = 𝑦 ) )
15	13 14	sylibd	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
16	15	rgen2	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → 𝑥 = 𝑦 )
17		dff1o6	⊢ ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) ↔ ( bra Fn ℋ ∧ ran bra = ( LinFn ∩ ContFn ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( bra ‘ 𝑥 ) = ( bra ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
18	4 5 16 17	mpbir3an	⊢ bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn )