Halmos wrote Finite Dimensional Vector Spaces in 1942 -- shortly after he got his Ph.D. from J. Doob at University of Illinois -- at the Institute for Advanced Study in Princeton as an assistant to von Neumann.
The book is a mostly finite dimensional introduction to von Neumann's Hilbert space theory. Some physics profs tell their students to read that book to learn the Hilbert space theory they need for quantum mechanics. Generally the book uses Hilbert space, that is infinite dimensional, notation and arguments when they also work for the finite dimensional results -- cute. This approach is easier and cleaner when it works.
There is emphasis on duality, as is important in functional analysis including Hilbert space.
Some of the special emphasis is on spectral theory, important in transformations on Hilbert space.
Halmos includes some multi-linear algebra (can see again in exterior algebra and more modern approaches to general relativity) and near the end has an ergodic theorem!
At one time the book was one of three basic references for Harvard's somewhat famous or notorious Math 55 as in
http://www.american.com/archive/2008/march-april-magazine-co...
The other two references were Rudin's Principles and Spivak's Calculus on Manifolds. So, from Harvard get a good recommendation for excellence for the Halmos book.
I very much enjoyed that Halmos book and later more of his books. He was one of the best writers in math of the 20th century.
His proof of the Hamilton-Cayley theorem is a little less general than the one in, say, E. Nering's book, and I wrote Halmos about that. He wrote back a nice letter.
I learned linear algebra from a course in abstract algebra, Murdoch, Linear Algebra for Undergraduates, (about the easiest linear algebra book anyone could read), one by E. Nering, some work I did in mathematical physics, the first chapters of Nickerson, Spencer, and Steenrod's Advanced Calculus, my ugrad math honors paper on group representation theory, Herstein's Topics in Algebra on abstract algebra, Halmos, FDVS, Forsythe and Molar on numerical linear algebra, applications in multivariate statistics, some work in optimization, carefully wrote out my own notes, enough for a book, and more.
The OP list also includes Horn's book. After all that study, mostly independently and part of my career in applied math and computing, eventually I took Horn's course, intended to be an advanced course. As part of my application to his grad school, I did include a copy of the Halmos letter!
There was next to nothing in the Horn course new to me, and I didn't try very hard. Everything in the course was carefully graded. I did the homework but didn't study for the tests. On an early homework assignment, the grader made a mistake on my paper; I corrected him; and he made no more mistakes. About 3/4ths the way through the course the grader showed me the class scores -- I was first on everything by wide margins. Did that again on the final. Apparently did that again on the corresponding Ph.D. qualifying exam.
In the course, when Horn got to the polar decomposition, I got excited and blurted out in class "That's my favorite theorem" which it was and is. Horn's remark was, "Thank you Dr. Halmos".
The polar decomposition? Go through a lot of stuff in linear transformations and then discover something really simple: All a linear transformation can do is just a rigid motion (rotations, reflections) followed by stretching/shrinking on orthogonal axes. A singular transformation? One or more of the axes go to zero. In the non-singular case, the proof is really simple. In the singular case the difficulty is that there are many choices for the rigid motion part and just have to pick one.
Horn did at times have some especially good proofs.
Horn is very precise with high quality.
It's possible to have a quite fast introduction to linear algebra, but then are missing out on a lot if don't work carefully through a classic text such as Hoffman and Kunze. IIRC it is available as PDF on the internet for free.
E. Nering's book is also fine except for his material in the back on linear programming which is easy (for a lot of it, just slightly tweak Gauss elimination) but he makes difficult. For linear programming, get a good book on linear programming, e.g., Chvatal or Bazaraa and Jarvis. In the back, Nering also does group representations -- very cute.
I'd recommend Halmos, FDVS as ice cream and cake desert after something like Hoffman and Kunze.
For the numerical stuff, should look at the documentation for Linpack. Maybe also look at Forsythe and Molar. Some that has been done since then for numerical methods, e.g., for models of oil reservoirs, is impressive -- might at least glance at that.
Broadly there are two directions in linear algebra: One direction assumes that the field is the real and/or complex numbers and is aimed at analysis and applied math. The other direction assumes finite fields and is aimed at high end abstract algebra and has applications in, say, algebraic coding theory (high end error correcting codes).
The direction with real and complex numbers is, sure, a start on functional analysis (you are in a vector space, but each point is a function -- get to learn how to approximate functions by other functions, e.g., how to approximate random variables by other random variables, e.g., learn Fourier theory), but for that also should have measure theory, e.g., from Royden, Real Analysis and/or the first half of Rudin, Real and Complex Analysis. For that, as in Math 55, a prerequisite is Rudin's, Principles.
Rudin's Functional Analysis is more advanced, still. I got accepted to grad school at Brown's Division of Applied Math (didn't go there), and Rudin's FA was popular there, but I haven't seen a lot of popularity for it elsewhere.
A huge fraction of applied math, somewhere on the way to implementation and code, boils down to linear algebra.