I'd like to thank all the commenters for their insights. In the end, I have decided to go with Lax's Linear Algebra and its Applications, primarily due to its insistence on abstract vector spaces (i.e., the field is not assumed to be complex or real numbers) and the focus on linear transformations as opposed to matrices, which will set up the students nicely for functional analysis.
Also, my concerns about his "applied" examples have been allayed, as I think the students will find them interesting and not the typical "plug and chug" applications they get elsewhere. The focus on analysis-related topics will also help tie in some aspects of what they learned in calculus (e.g., $e^A$ as a Taylor series...cool connection between linear algebra and calculus!).
I doubt I'll go through the whole book for a semester -- despite it's brevity, it's very, very dense on knowledge (so in terms of $/bit, it's quite well priced ;-). I think that covering Chapters 1-7 is a must as core abstract material.
- Fundamentals (basic definitions of abstract linear spaces and quotient spaces)
- Duality -- I'm including this because I want to hit on spaces of functions at the end wrt machine learning, where the idea of a dual space is important.
- Linear Mappings
- Matrices
- Determinants and Trace
- Spectral Theory
- Euclidean Structure (lots of important and very widely applied concepts here)
Also, given the interest in machine learning among students this group, I also think that Chapters 8,9,10, and 16 should be delved into, since symmetric and/or positive matrices play a role in many machine learning algorithms.
Spectral Theory of Self-Adjoint Mappings: Covers the common case of symmetric matrices (e.g., in PCA and aspects of SVD), especially the ubiquitous quadratic forms that underlie KKT conditions and many optimization methods.
Calculus of Vector and Matrix-Valued Functions: Views these objects as vector-objects, not sets of scalar equations. Very useful for understanding convergence of optimization algorithms and getting a new view on multivariate calculus (e.g., be able to calculate $\frac{d}{dt}A(t)B(t)$). Does not really cover Matrix Calculus, such as $\frac{d\mathbf{F}}{\mathbf{X}}$, but that is not a huge concern for me as it's mainly conventions for bookkeeping of variables.
Matrix Inequalities: Pop up all the time when dealing with constraints. Also covers the extremely useful Singular Value Decomposition.
- (Chap 16) Positive Matrices: Perron-Frobenius Theorem -- enough said!
After that, I thought that Chapter 11 on Dynamics (to pull it together) and my own intro to Reproducing Kernel Hilbert Spaces (the conceptual world of kernel-based learning methods) would be good ways to end the course.
Again, thanks all for your input! Very much appreciated the community here.