Frobenius theorem (real division algebras)

In mathematics, more specifically in abstract algebra, the Frobenius theorem, proved by Ferdinand Georg Frobenius in 1877, characterizes the finite-dimensional associative division algebras over the real numbers. According to the theorem, every such algebra is isomorphic to one of the following:
These algebras have real dimension , and , respectively. Of these three algebras, and are commutative, but is not.
Proof.
The main ingredients for the following proof are the Cayley–Hamilton theorem and the fundamental theorem of algebra.
The claim.
The key to the argument is the following
Proof of Claim: Let be the dimension of as an -vector space, and pick in with characteristic polynomial . By the fundamental theorem of algebra, we can write
We can rewrite in terms of the polynomials :
Since , the polynomials are all irreducible over . By the Cayley–Hamilton theorem, and because is a division algebra, it follows that either for some or that for some . The first case implies that is real. In the second case, it follows that is the minimal polynomial of . Because has the same complex roots as the minimal polynomial and because it is real it follows that
Since is the characteristic polynomial of the coefficient of in is up to a sign. Therefore, we read from the above equation we have: if and only if , in other words if and only if .
So is the subset of all with . In particular, it is a vector subspace. Moreover, has codimension since it is the kernel of a non-zero linear form, and note that is the direct sum of and as vector spaces.
The finish.
For in define . Because of the identity , it follows that is real. Furthermore, since , we have: for . Thus is a positive definite symmetric bilinear form, in other words, an inner product on .
Let be a subspace of that generates as an algebra and which is minimal with respect to this property. Let be an orthonormal basis of with respect to . Then orthonormality implies that:
If , then is isomorphic to .
If , then is generated by and subject to the relation . Hence it is isomorphic to .
If , it has been shown above that is generated by subject to the relations 
These are precisely the relations for .
If , then cannot be a division algebra. Assume that . Let . It is easy to see that (this only works if ). If were a division algebra, implies , which in turn means: and so generate . This contradicts the minimality of .