Theorem Submodule.disjoint_span_singleton''

feat: add an element to a linear indep family, more general version (#31515)