Equivalence of Definitions of Semisimplicity using Zorn's Lemma (is there a simpler way?) This is my attempt to prove that one definition of semisimplicity implies the other. That is, if $M$ is an $R$-module such that $M$ can be written as a direct sum of simple modules, then it is true that for any submodule $N$ of $M$, there exists another submodule $P$ such that $M = N \oplus P$.
I feel like it might be needlessly complicated (and I'm not 100% sure that it's correct), so I'd like some feedback on that. Thanks in advance!!
This is the proof:
Suppose $M = \oplus_{i\in I} M_i$, where each $M_i$ is simple, and that $N$ is a submodule of $M$. Let's define the family of sets:
$$F := \{J \subseteq I : N + (\oplus_{j \in J} M_j) \text{ is direct}\}$$
We will show that any chain of elements of $F$ has an upper bound in $F$.
Let $J_1 \subseteq J_2 \subseteq J_3 \subseteq \text{ }...$ be a chain of elements of $F$. The most natural candidate for an upper bound is  $J' := \bigcup J_i$. For that to be the case, we need to show that $J' \in F$, i. e. that the sum $N + (\oplus_{j \in J'} M_j)$ is direct.
Suppose it wasn't. There would be some nonzero $n \in N \cap \oplus_{j \in J'} M_j$. Since $n \in \oplus_{j \in J'}M_j$, we have that $n = m_{j_1} + ... + m_{j_k}$, where $j_1, ..., j_k \in J'$ and each $m_{j_i} \in M_{j_i}$.
We defined $J'$ as the union of every set $J_i$ in the chain, so each of $j_1, ..., j_k$ has to be in one of these sets. Let's say $J_{f(j_i)}$ is the first set in the chain that contains $j_i$. Since the sets are chained, $J'' := J_{max(f(j_1),...,f(j_k))}$ has to contain all of $j_1$ to $j_k$. From that, we'd have that $n = m_{j_1} + ... + m_{j_k} \in \oplus_{j\in J''} M_j$. That implies that the sum $N + \oplus_{j\in J''} M_j$ is not direct, which is a contradiction, since $J'' \in F$.
With this, we have shown that $J'$ must be in $F$, and, naturally, we can say it is an upper bound for the chain. Therefore, we can invoke Zorn's Lemma and say that there exists a maximal element of $F$.
Let $I'$ be such a maximal element. We have that the sum $M' := N \oplus (\oplus_{i \in I'} M)$ is direct. We will now show that $M' = M$, by showing that $M'$ contains each of the simple submodules $M_i$ that sum up to $M$.
Suppose that isn't the case. There is $k \in I$ such that $M_k \not\subseteq M' \iff M_k \cap M' \neq M_k$. Since $M_k \cap M'$ is a submodule of $M_k$, which is a simple module, we can affirm that $M_k \cap M' = \{0\}$. However, that would imply that the sum $$M' \oplus M_k = N \oplus (\oplus_{i \in I'} M) \oplus M_k = N \oplus (\oplus_{i \in I' \cup \{k\}} M)$$ is direct, which contradicts the maximality of $I'$
With this, we have shown that $M'$ does in fact contain every $M_i$ for $i \in I$, which implies that $M = \oplus_{i\in I} M_i \subseteq M'$. Since $M' \subseteq M$, we conclude that $M = M' = N \oplus (\oplus_{i \in I'} M)$, which means that $N$ is, in fact, a direct summand of $M$.
 A: Your proof is correct, and I strongly suspect there is no way to prove the theorem in question while avoiding some amount of choice. To illustrate this, consider the following claim:

For all sets $I$ and all families $(A_i)_{i \in I}$ of finite sets, there is an element of $\prod\limits_{i \in I} A_i$.

The above claim cannot be proved in ZF. However, it follows from the following claim, which is related to yours (here, we can take any $k$ we like that is a field):

Consider some set $I$. Let $M = \bigoplus\limits_{i \in I} k$, and suppose $N$ is a submodule. Then there is some $J \subseteq I$ such that $M$ is the internal direct sum of $N$ and $\bigoplus\limits_{j \in J} k$, when we abusively consider the latter as a subset of $M$.

Your proof implies this second claim. Clearly, $k$ a field and $M_i = k$ is a special case of $M_i$ simple.
Assume the second claim, and let $(A_i)_{i \in I}$ be a family of finite sets. Without loss of generality, take the $A_i$ to be pairwise disjoint. Then let $P = \bigcup\limits_{i \in I} A_i$, and let $M = \bigoplus\limits_{p \in P} k$ (where $p \in P$ corresponds to generator $m_p \in M$). Let $N$ be the submodule of $M$ generated by $\{\sum\limits_{p \in A_i} m_p \mid i \in I\}$, and take $J \subseteq P$ such that $M$ is the internal direct sum of $N$ and $\bigoplus\limits_{j \in J} k$.
I claim that for all $i \in I$, $A_i \setminus J$ is a singleton set. For we clearly know that $A_i \setminus J \neq \emptyset$, since then we would have $\sum\limits_{p \in A_i} m_p \in J \cap N$, and we can’t have a nonzero element of $J \cap N$. We also can’t have $p, q \in A_i \setminus J$ with $p \neq q$, since then we could not express $m_p$ as a sum of an element from $J$ and an element from $N$. Then we can define $f \in \prod\limits_{i \in I} A_i$ by $f(i) = $ the unique element of $A_i \setminus J$. $\square$
Since the second claim implies the first, and since the first claim can’t be proved in ZF, the second also can’t be proved in ZF.
