Maximal-submodule splitting criterion for semisimplicity (source code)

= Maximal-submodule splitting criterion for semisimplicity
{title2=$\forall M\text{ maximal in }V,\quad V=M\oplus C\implies V\text{ semisimple}$}

For a finite-dimensional <module>, it suffices that every maximal proper <submodule> have a <submodule> complement in order that every <submodule> have one. Let $W$ be the sum of all <simple modules> contained in the given <module>. If $W$ is proper, choose a maximal <submodule> $M$ containing it. A complement $C$ is isomorphic to the simple quotient $V/M$ and hence is itself simple. This forces $C\subseteq W\subseteq M$, contradicting the complement. Thus $W=V$. Greedily adding simple summands not already in the sum gives a <direct sum> in finitely many steps. Finally, given any $U$, choose a maximal sum of these simple summands disjoint from $U$. A missing simple summand has zero intersection with their sum plus $U$, contradicting maximality unless their sum complements $U$. This proves the <semisimple module> criterion, including the zero <module>.