Prove that Gl(n, F) is a group I've seen "proofs" of this before but they all just assume we already know that matrix multiplication is associative, matrices with nonzero determinant are invertible, etc. and I do know this insofar that I've been told it since high school, but I don't think I've actually ever seen a proof that matrix multiplication is well defined, associative, etc. Does anyone know of any more rigorous proofs out there? I've googled a lot but haven't found anything. It's not exactly the sort of thing I'd want to spend time on proving rigorously myself since I already know these things to be true, but I would like to see a proof. 
Thanks! 
 A: Matrix multiplication is associative : that's because the multiplicative structure of matrices is a transferred structure from the (algebra) ring of endomorphisms of $K^n$ : since composition is associative, matrix multiplication is as well (note that the formulas of matrix multiplications are, in this set up, theorems rather than definitions)
$I_n$ is an identity element : using the matrix multiplication formulas, this is easily provable. Or else, you can simply note that under the identification $L(K^n)/ M_n(K)$, $I_n$ is the image of the identity mapping $K^n \to K^n$ and therefore it is an identity.
Matrices with nonzero determinant are invertible : 
This comes from the equalities $M Com(M)^T = det(M)I_n = Com(M)^T M$ where $Com(M)$ is the comatrix of $M$. These equalities hold for matrices over arbitrary rings and can be proved through sheer calculations. Since nonzero scalars are invertible (we are over a field), if $det(M)\neq 0$, this implies $M^{-1} := \frac{1}{det(M)}Com(M)^T$ is an inverse of $M$.
In conclusion,  $GL_n(K)$ is a group.
