Theorem rnbra

Description: The set of bras equals the set of continuous linear functionals. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	rnbra	⊢ ran bra = ( LinFn ∩ ContFn )

Proof

Step	Hyp	Ref	Expression
1		lnfncnbd	⊢ ( 𝑡 ∈ LinFn → ( 𝑡 ∈ ContFn ↔ ( normfn ‘ 𝑡 ) ∈ ℝ ) )
2	1	pm5.32i	⊢ ( ( 𝑡 ∈ LinFn ∧ 𝑡 ∈ ContFn ) ↔ ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) )
3		elin	⊢ ( 𝑡 ∈ ( LinFn ∩ ContFn ) ↔ ( 𝑡 ∈ LinFn ∧ 𝑡 ∈ ContFn ) )
4		ax-hilex	⊢ ℋ ∈ V
5	4	mptex	⊢ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) ∈ V
6		df-bra	⊢ bra = ( 𝑥 ∈ ℋ ↦ ( 𝑦 ∈ ℋ ↦ ( 𝑦 ·ih 𝑥 ) ) )
7	5 6	fnmpti	⊢ bra Fn ℋ
8		fvelrnb	⊢ ( bra Fn ℋ → ( 𝑡 ∈ ran bra ↔ ∃ 𝑥 ∈ ℋ ( bra ‘ 𝑥 ) = 𝑡 ) )
9	7 8	ax-mp	⊢ ( 𝑡 ∈ ran bra ↔ ∃ 𝑥 ∈ ℋ ( bra ‘ 𝑥 ) = 𝑡 )
10		bralnfn	⊢ ( 𝑥 ∈ ℋ → ( bra ‘ 𝑥 ) ∈ LinFn )
11		brabn	⊢ ( 𝑥 ∈ ℋ → ( normfn ‘ ( bra ‘ 𝑥 ) ) ∈ ℝ )
12	10 11	jca	⊢ ( 𝑥 ∈ ℋ → ( ( bra ‘ 𝑥 ) ∈ LinFn ∧ ( normfn ‘ ( bra ‘ 𝑥 ) ) ∈ ℝ ) )
13		eleq1	⊢ ( ( bra ‘ 𝑥 ) = 𝑡 → ( ( bra ‘ 𝑥 ) ∈ LinFn ↔ 𝑡 ∈ LinFn ) )
14		fveq2	⊢ ( ( bra ‘ 𝑥 ) = 𝑡 → ( normfn ‘ ( bra ‘ 𝑥 ) ) = ( normfn ‘ 𝑡 ) )
15	14	eleq1d	⊢ ( ( bra ‘ 𝑥 ) = 𝑡 → ( ( normfn ‘ ( bra ‘ 𝑥 ) ) ∈ ℝ ↔ ( normfn ‘ 𝑡 ) ∈ ℝ ) )
16	13 15	anbi12d	⊢ ( ( bra ‘ 𝑥 ) = 𝑡 → ( ( ( bra ‘ 𝑥 ) ∈ LinFn ∧ ( normfn ‘ ( bra ‘ 𝑥 ) ) ∈ ℝ ) ↔ ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) ) )
17	12 16	syl5ibcom	⊢ ( 𝑥 ∈ ℋ → ( ( bra ‘ 𝑥 ) = 𝑡 → ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) ) )
18	17	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℋ ( bra ‘ 𝑥 ) = 𝑡 → ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) )
19		riesz1	⊢ ( 𝑡 ∈ LinFn → ( ( normfn ‘ 𝑡 ) ∈ ℝ ↔ ∃ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑡 ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) ) )
20	19	biimpa	⊢ ( ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) → ∃ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑡 ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) )
21		braval	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) )
22		eqtr3	⊢ ( ( ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) ∧ ( 𝑡 ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) ) → ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑡 ‘ 𝑦 ) )
23	22	ex	⊢ ( ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) → ( ( 𝑡 ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) → ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑡 ‘ 𝑦 ) ) )
24	21 23	syl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 𝑡 ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) → ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑡 ‘ 𝑦 ) ) )
25	24	ralimdva	⊢ ( 𝑥 ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( 𝑡 ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) → ∀ 𝑦 ∈ ℋ ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑡 ‘ 𝑦 ) ) )
26	25	adantl	⊢ ( ( ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( 𝑡 ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) → ∀ 𝑦 ∈ ℋ ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑡 ‘ 𝑦 ) ) )
27		brafn	⊢ ( 𝑥 ∈ ℋ → ( bra ‘ 𝑥 ) : ℋ ⟶ ℂ )
28		lnfnf	⊢ ( 𝑡 ∈ LinFn → 𝑡 : ℋ ⟶ ℂ )
29	28	adantr	⊢ ( ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) → 𝑡 : ℋ ⟶ ℂ )
30		ffn	⊢ ( ( bra ‘ 𝑥 ) : ℋ ⟶ ℂ → ( bra ‘ 𝑥 ) Fn ℋ )
31		ffn	⊢ ( 𝑡 : ℋ ⟶ ℂ → 𝑡 Fn ℋ )
32		eqfnfv	⊢ ( ( ( bra ‘ 𝑥 ) Fn ℋ ∧ 𝑡 Fn ℋ ) → ( ( bra ‘ 𝑥 ) = 𝑡 ↔ ∀ 𝑦 ∈ ℋ ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑡 ‘ 𝑦 ) ) )
33	30 31 32	syl2an	⊢ ( ( ( bra ‘ 𝑥 ) : ℋ ⟶ ℂ ∧ 𝑡 : ℋ ⟶ ℂ ) → ( ( bra ‘ 𝑥 ) = 𝑡 ↔ ∀ 𝑦 ∈ ℋ ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑡 ‘ 𝑦 ) ) )
34	27 29 33	syl2anr	⊢ ( ( ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝑥 ) = 𝑡 ↔ ∀ 𝑦 ∈ ℋ ( ( bra ‘ 𝑥 ) ‘ 𝑦 ) = ( 𝑡 ‘ 𝑦 ) ) )
35	26 34	sylibrd	⊢ ( ( ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℋ ( 𝑡 ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) → ( bra ‘ 𝑥 ) = 𝑡 ) )
36	35	reximdva	⊢ ( ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) → ( ∃ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑡 ‘ 𝑦 ) = ( 𝑦 ·ih 𝑥 ) → ∃ 𝑥 ∈ ℋ ( bra ‘ 𝑥 ) = 𝑡 ) )
37	20 36	mpd	⊢ ( ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) → ∃ 𝑥 ∈ ℋ ( bra ‘ 𝑥 ) = 𝑡 )
38	18 37	impbii	⊢ ( ∃ 𝑥 ∈ ℋ ( bra ‘ 𝑥 ) = 𝑡 ↔ ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) )
39	9 38	bitri	⊢ ( 𝑡 ∈ ran bra ↔ ( 𝑡 ∈ LinFn ∧ ( normfn ‘ 𝑡 ) ∈ ℝ ) )
40	2 3 39	3bitr4ri	⊢ ( 𝑡 ∈ ran bra ↔ 𝑡 ∈ ( LinFn ∩ ContFn ) )
41	40	eqriv	⊢ ran bra = ( LinFn ∩ ContFn )