Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The one-step submodule criterion; intersections and sums of submodules are submodules

Statement

Let MM be a left RR-module. A nonempty subset S⊆MS\subseteq M is a submodule if and only if

ru+v∈S(r∈R,u,v∈S).ru+v\in S\qquad(r\in R, u,v\in S).

Consequently, the intersection of every nonempty family of submodules is a submodule, and, for submodules A,B≤MA,B\le M,

A+B:={a+b:a∈A,b∈B}A+B:=\{a+b:a\in A, b\in B\}

is a submodule of MM.

Facts & Assumptions

Given: A left RR-module MM.

[L1]

The module axioms include 1Rm=m1_Rm=m and distributivity of scalar multiplication over both additions (Unital left and right modules over a ring; unqualified module means left module).

[L2]

In a module, (−r)m=−(rm)(-r)m=-(rm); taking r=1Rr=1_R and using [L1] gives (−1R)m=−m(-1_R)m=-m (In a module, 0Rm=0M0_Rm=0_M, r0M=0Mr0_M=0_M, (−r)m=−(rm)(-r)m=-(rm) and r(−m)=−(rm)r(-m)=-(rm)).

[L3]

A nonempty subset of a group is a subgroup exactly when it is closed under xy−1xy^{-1} (One-step subgroup test: a nonempty H⊆GH \subseteq G is a subgroup iff gh−1∈Hgh^{-1} \in H for all g,h∈Hg, h \in H; the identity and the inverses of HH are then those of GG).

[L4]

A submodule is an additive subgroup closed under scalar multiplication (Submodule of a module).

Proof

technique · direct
1.1

If SS is a submodule, then u∈Su\in S implies ru∈Sru\in S, and then ru+v∈Sru+v\in S for r∈Rr\in R and u,v∈Su,v\in S.

L4given
1.2

Conversely, suppose the displayed closure condition holds and choose s∈Ss\in S. With r=−1Rr=-1_R and both elements equal to ss, it gives (−1R)s+s=0M∈S(-1_R)s+s=0_M\in S.

L1L2given
1.3

If u,v∈Su,v\in S, the same condition with scalar −1R-1_R, first element vv, and second element uu gives (−1R)v+u=u−v∈S(-1_R)v+u=u-v\in S.

L1L2given
2.1

The additive subgroup test applies by steps 1.2--1.3; scalar closure follows from the displayed condition with v=0Mv=0_M. Thus SS is a submodule.

step 1.2step 1.3L3L4given
3.1

For a nonempty family (Ni)(N_i) of submodules, 0M0_M lies in every NiN_i; and if u,vu,v lie in their intersection, then ru+vru+v lies in every NiN_i. The criterion proves ⋂iNi\bigcap_iN_i is a submodule.

step 2.1L4given
4.1

For x=a+bx=a+b and y=a′+b′y=a'+b' in A+BA+B, distributivity gives rx+y=(ra+a′)+(rb+b′)∈A+Brx+y=(ra+a')+(rb+b')\in A+B; moreover 0M=0M+0M∈A+B0_M=0_M+0_M\in A+B. The criterion proves A+BA+B is a submodule.

step 2.1L1L4given∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 16 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources