Necessity of Axiom of Choice in Functional Analysis given ZF + Dependent Choice What do we get with the Axiom of Choice (AC) in Functional Analysis that cannot be accomplished with Zermelo-Fraenkel (ZF) plus the Axiom of Dependent Choice (DC)?
So, for instance, just dusted off and opened my old class notes and saw


*

*Hahn-Banach (see note below)

*Baire Category (see note below)

*Open Mapping / Closed Graph thrms

*Uniform Boundedness Principle

*Projection Lemma (Hilbert Space)

*Unit Ball is weak-* compact (Banach-Algaoglu)

*Riesz Representation Theorem (see note below)

*Spectral Theorem

*Separation of Convex sets by Hyperplanes

*Basic theorems about distribution functions/L^P spaces 


... and any other theorems you can think of that fit in this theme of being well known to anyone who took a basic course in functional analysis, and useful to people who use analysis in their work. Please add to list b/c I am sure I forgot some theorems.
(note on Hahn-Banach: In the spirit of the question, the most concrete form that is still abstract enough to use in the proofs of the other theorems is fine here. For instance, in my notes I have $p$ sublinear on a N.V.S. $X$ and $V$ a subspace of $X$, $f\in V^*$ and $|f|\le p$ on $V$ as the assumptions.
note on Baire Category: The version that every complete metric space (or Banach space) is a Baire space would likely be sufficient here since I believe that the second one that locally compact Hausdorff spaces are Baire might not be standard material for a basic course in Functional Analysis. Please correct me if I'm wrong!)
So, which require AC if one already accepts ZF+DC?
Edit This is intended to be more a question about the internal logical dependencies of Functional Analysis than about logic and set theory. A good answer does not need to prove each of the theorems separately. In particular, One might show theorems $n_1$ and $n_2$ can be proven with DC by citing good links. Then say "a standard proof for $n_3$ uses $n_1$ and some epsilon delta stuff. A standard proof $n_4$ uses $n_2$ and $n_3$ plus image of compact sets is compact, so also doesn't need full AC." For the ones that do need AC, maybe a good link for one and then a link showing that others are equivalent under ZF. 
In other words, what I am looking for is for someone to take the few theorems about DC vs. AC that have already been proven, and flesh this out to the rest of (basic) functional analysis by discussing logical dependencies within the field of functional analysis.
Please only assume a background in functional analysis, not in Foundations (sets/logic/etc. beyond everyday use). References to other questions where the details have been worked out in more rigour are quite sufficient.
 A: There is an obvious item missing from your list: the existence of nonmeasurable sets.  The second Solovay model (see here) is a model of ZF+DC and all of its sets are Lebesgue measurable. Without being able to mention the existence of nonmeasurable sets it becomes difficult to motivate the machinery of $\sigma$-algebras.  Furthermore Terry Tao has pointed out some nifty applications of nonmeasurable sets, particularly in the context of Robinson's framework.
In another direction, you can't even start talking about the Stone-Čech compactification, e.g., $\beta\mathbb N$, unless you have something stronger than DC.
My guess would be that the existence of an invariant subspace of a polynomially compact operator on Hilbert space cannot be established without a stronger form of choice. Certainly Lomonosov's proof, while simple, uses powerful fixed-point results that most likely rely on AC.
A: Cédric Villani's undergraduate lecture notes covering the content of Brezis's functional analysis book as well as Lebesgue integral and Fourier integral without the Axiom of Choice using "modern language" is 70% complete (about 400 pages) according to this interview (Google translate).
有不少已经计划要写的书⋯⋯我还没有时间完成，有一天我会回头来做这件事。其中之一是大学部课程的讲义，我写了约莫400页左右，希望涵盖Brezis「泛函分析」的内容，重新用现代的语言阐述，不要用到选择公理(Axiom of Choice)，我在写的过程中决定不再使用选择公理。 
这本书我写了大概百分之七十，包含勒贝格积分(Lebesgue integration)、泛函分析和傅立叶积分，然后就搁下来，八年来碰都没碰，但有段时间我确实曾经为上我的课的学生们用心写这本书。
