I would like to see a constructive proof (some algorithm?) of the following statement:
Let $A_1, A_2, \dotsc ,A_k \in M_n(\mathbb C)$ be some commuting matrices, let $B$ be the commutative algebra (with identity) over $\mathbb C$ generated by $A_1, A_2, \dotsc, A_k$. Suppose $E \in B$ is not invertible, then $I = (E)$ is a proper ideal of $B$. There exists a maximal ideal $J$ of $B$ such that $I \subset J$.
I know we can prove the existence of maximal ideal of general commutative rings using the axiom of choice, but I think when dealing with concrete examples, a constructive proof can give us more insights.
In fact, I am trying to apply the proof Gelfand's theory of commutative Banach algebras to the special case of matrix algebras. The existence of maximal ideals is a key fact that estabilishes properties of Gelfand transform. In my experience, applying abstract proofs to concrete examples can always help us gain a better understanding. For example, I am very happy to see a finite-dimensional version of Gelfand–Mazur theorem.
Actually I asked a somewhat related question Construct maximal ideal in multivariate polynomial ring in MSE, asking for constructive proofs for maximal ideals in multivariate polynomial algebra (since the matrix algebra is quotient algebra of multivariate polynomial algebra). However, the matrix algebra case is what I really concerned.
I have limited knowledges in algebra, so this may be a very simple question.
