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

1. Hahn-Banach (see note below)



2. Baire Category (see note below)




3. Open Mapping / Closed Graph thrms



4. Uniform Boundedness Principle


5. Projection Lemma (Hilbert Space)


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


7. Riesz Representation Theorem (see note below)


8. Spectral Theorem



9. Separation of Convex sets by Hyperplanes


10. 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.