Metamath Proof Explorer

Theorem hhcnf

Description: The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hhcn.1 ⊢D=normℎ∘-ℎ
hhcn.2 ⊢J=MetOpen⁡D
hhcn.4 ⊢K=TopOpen⁡ℂfld
Assertion hhcnf ⊢ContFn=JCnK

Proof

Step Hyp Ref Expression
1 hhcn.1 ⊢D=normℎ∘-ℎ
2 hhcn.2 ⊢J=MetOpen⁡D
3 hhcn.4 ⊢K=TopOpen⁡ℂfld
4 df-rab ⊢t∈ℂℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y=t|t∈ℂℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
5 df-cnfn ⊢ContFn=t∈ℂℋ|∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
6 1 hilmetdval ⊢x∈ℋ∧w∈ℋ→xDw=normℎ⁡x-ℎw
7 normsub ⊢x∈ℋ∧w∈ℋ→normℎ⁡x-ℎw=normℎ⁡w-ℎx
8 6 7 eqtrd ⊢x∈ℋ∧w∈ℋ→xDw=normℎ⁡w-ℎx
9 8 adantll ⊢t:ℋ⟶ℂ∧x∈ℋ∧w∈ℋ→xDw=normℎ⁡w-ℎx
10 9 breq1d ⊢t:ℋ⟶ℂ∧x∈ℋ∧w∈ℋ→xDw<z↔normℎ⁡w-ℎx<z
11 ffvelcdm ⊢t:ℋ⟶ℂ∧x∈ℋ→t⁡x∈ℂ
12 ffvelcdm ⊢t:ℋ⟶ℂ∧w∈ℋ→t⁡w∈ℂ
13 11 12 anim12dan ⊢t:ℋ⟶ℂ∧x∈ℋ∧w∈ℋ→t⁡x∈ℂ∧t⁡w∈ℂ
14 eqid ⊢abs∘−=abs∘−
15 14 cnmetdval ⊢t⁡x∈ℂ∧t⁡w∈ℂ→t⁡xabs∘−t⁡w=t⁡x−t⁡w
16 abssub ⊢t⁡x∈ℂ∧t⁡w∈ℂ→t⁡x−t⁡w=t⁡w−t⁡x
17 15 16 eqtrd ⊢t⁡x∈ℂ∧t⁡w∈ℂ→t⁡xabs∘−t⁡w=t⁡w−t⁡x
18 13 17 syl ⊢t:ℋ⟶ℂ∧x∈ℋ∧w∈ℋ→t⁡xabs∘−t⁡w=t⁡w−t⁡x
19 18 anassrs ⊢t:ℋ⟶ℂ∧x∈ℋ∧w∈ℋ→t⁡xabs∘−t⁡w=t⁡w−t⁡x
20 19 breq1d ⊢t:ℋ⟶ℂ∧x∈ℋ∧w∈ℋ→t⁡xabs∘−t⁡w<y↔t⁡w−t⁡x<y
21 10 20 imbi12d ⊢t:ℋ⟶ℂ∧x∈ℋ∧w∈ℋ→xDw<z→t⁡xabs∘−t⁡w<y↔normℎ⁡w-ℎx<z→t⁡w−t⁡x<y
22 21 ralbidva ⊢t:ℋ⟶ℂ∧x∈ℋ→∀w∈ℋxDw<z→t⁡xabs∘−t⁡w<y↔∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
23 22 rexbidv ⊢t:ℋ⟶ℂ∧x∈ℋ→∃z∈ℝ+∀w∈ℋxDw<z→t⁡xabs∘−t⁡w<y↔∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
24 23 ralbidv ⊢t:ℋ⟶ℂ∧x∈ℋ→∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xabs∘−t⁡w<y↔∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
25 24 ralbidva ⊢t:ℋ⟶ℂ→∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xabs∘−t⁡w<y↔∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
26 25 pm5.32i ⊢t:ℋ⟶ℂ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xabs∘−t⁡w<y↔t:ℋ⟶ℂ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
27 1 hilxmet ⊢D∈∞Met⁡ℋ
28 cnxmet ⊢abs∘−∈∞Met⁡ℂ
29 3 cnfldtopn ⊢K=MetOpen⁡abs∘−
30 2 29 metcn ⊢D∈∞Met⁡ℋ∧abs∘−∈∞Met⁡ℂ→t∈JCnK↔t:ℋ⟶ℂ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xabs∘−t⁡w<y
31 27 28 30 mp2an ⊢t∈JCnK↔t:ℋ⟶ℂ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋxDw<z→t⁡xabs∘−t⁡w<y
32 cnex ⊢ℂ∈V
33 ax-hilex ⊢ℋ∈V
34 32 33 elmap ⊢t∈ℂℋ↔t:ℋ⟶ℂ
35 34 anbi1i ⊢t∈ℂℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y↔t:ℋ⟶ℂ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
36 26 31 35 3bitr4i ⊢t∈JCnK↔t∈ℂℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
37 36 eqabi ⊢JCnK=t|t∈ℂℋ∧∀x∈ℋ∀y∈ℝ+∃z∈ℝ+∀w∈ℋnormℎ⁡w-ℎx<z→t⁡w−t⁡x<y
38 4 5 37 3eqtr4i ⊢ContFn=JCnK