Theorem: Submodule Test

Let $\struct {R, +_R, \times_R}$ be a ring with unity $1_R$.
Let $\struct {G, +, \circ}_R$ be a unitary $R$-module.
Let $H$ be a non-empty subset of $G$.
Then $\struct {H, +, \circ}_R$ is a submodule of $G$ {{iff}}:
{{begin-eqn}}
{{eqn | n = SM1
      | q = \forall x, y \in H
      | l = x + y
      | o = \in
      | r = H
}}
{{eqn | n = SM2
      | q = \forall x \in H: \forall \lambda \in R
      | l = \lambda \circ x
      | o = \in
      | r = H
}}
{{end-eqn}}

Proof:
=== Necessary Condition ===
Let $\struct {H, +, \circ}_R$ fulfil the conditions $\text {SM} 1$ and $\text {SM} 2$.
We have {{hypothesis}} that $H \subseteq G$ such that $H \ne \O$.
We have from $\text {SM} 1$:
:$\forall x, y \in H: x + y \in H$
We have {{hypothesis}} that $\struct {R, +_R, \times_R}$ is a ring with unity whose unity is $1_R$.
Hence:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = H
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {-1_R} \circ x
      | o = \in
      | r = H
      | c = from $\text {SM} 2$
}}
{{eqn | ll= \leadsto
      | l = -x
      | o = \in
      | r = H
      | c = {{Defof|Unity of Ring}}
}}
{{end-eqn}}
It follows from the Two-Step Subgroup Test that $H$ is a subgroup of $\struct {G, +}$.
It remains to be shown that $\struct {H, +, \circ}_R$ fulfils the module axioms as follows:
{{begin-axiom}}
{{axiom | n = \text M 1
        | lc= Scalar Multiplication (Left) Distributes over Module Addition
        | q = \forall \lambda \in R: \forall x, y \in H
        | ml= \lambda \circ \paren {x + y}
        | mo= =
        | mr= \paren {\lambda \circ x} + \paren {\lambda \circ y}
}}
{{axiom | n = \text M 2
        | lc= Scalar Multiplication (Right) Distributes over Scalar Addition
        | q = \forall \lambda, \mu \in R: \forall x \in H
        | ml= \paren {\lambda +_R \mu} \circ x
        | mo= =
        | mr= \paren {\lambda \circ x} + \paren {\mu \circ x}
}}
{{axiom | n = \text M 3
        | lc= Associativity of Scalar Multiplication
        | q = \forall \lambda, \mu \in R: \forall x \in H
        | ml= \paren {\lambda \times_R \mu} \circ x
        | mo= =
        | mr= \lambda \circ \paren {\mu \circ x}
}}
{{end-axiom}}
;{{Module-axiom|1}}
{{begin-eqn}}
{{eqn | q = \forall x, y \in H
      | l = x + y
      | o = \in
      | r = H
      | c = from $\text {SM} 1$
}}
{{eqn | l = \lambda \circ x
      | o = \in
      | r = H
      | c = from $\text {SM} 2$
}}
{{eqn | l = \lambda \circ y
      | o = \in
      | r = H
      | c = from $\text {SM} 2$
}}
{{eqn | ll= \leadsto
      | l = \paren {\lambda \circ x} + \paren {\lambda \circ y}
      | o = \in
      | r = H
      | c = from $\text {SM} 1$
}}
{{eqn | ll= \leadsto
      | l = \paren {\lambda \circ x} + \paren {\lambda \circ y}
      | o = \in
      | r = G
      | c = as $H \subseteq G$
}}
{{eqn | ll= \leadsto
      | l = \paren {\lambda \circ x} + \paren {\lambda \circ y}
      | r = \lambda \circ \paren {x + y}
      | c = {{Module-axiom|1}} as applied to $\struct {G, +, \circ}_R$
}}
{{end-eqn}}
Hence $\struct {H, +, \circ}_R$ fulfils {{Module-axiom|1}}.
;{{Module-axiom|2}}
{{begin-eqn}}
{{eqn | q = \forall x \in H: \forall \lambda \in R
      | l = \lambda \circ x
      | o = \in
      | r = H
      | c = from $\text {SM} 2$
}}
{{eqn | ll= \leadsto
      | q = \forall \mu \in R
      | l = \paren {\lambda +_R \mu} \circ x
      | o = \in
      | r = H
      | c = from $\text {SM} 2$: as $\lambda +_R \mu \in R$
}}
{{eqn | ll= \leadsto
      | l = \paren {\lambda +_R \mu} \circ x
      | o = \in
      | r = G
      | c = as $H \subseteq G$
}}
{{eqn | ll= \leadsto
      | l = \paren {\lambda +_R \mu} \circ x
      | r = \paren {\lambda \circ x} + \paren {\mu \circ x}
      | c = {{Module-axiom|2}} as applied to $\struct {G, +, \circ}_R$
}}
{{end-eqn}}
Hence $\struct {H, +, \circ}_R$ fulfils {{Module-axiom|2}}.
;{{Module-axiom|3}}
{{begin-eqn}}
{{eqn | q = \forall x \in H: \forall \lambda \in R
      | l = \lambda \circ x
      | o = \in
      | r = H
      | c = from $\text {SM} 2$
}}
{{eqn | ll= \leadsto
      | q = \forall \mu \in R
      | l = \paren {\lambda \times_R \mu} \circ x
      | o = \in
      | r = H
      | c = from $\text {SM} 2$: as $\lambda \times_R \mu \in R$
}}
{{eqn | ll= \leadsto
      | l = \paren {\lambda \times_R \mu} \circ x
      | o = \in
      | r = G
      | c = as $H \subseteq G$
}}
{{eqn | ll= \leadsto
      | l = \paren {\lambda \times_R \mu} \circ x
      | r = \lambda \circ \paren {\mu \circ x}
      | c = {{Module-axiom|3}} as applied to $\struct {G, +, \circ}_R$
}}
{{end-eqn}}
Hence $\struct {H, +, \circ}_R$ fulfils {{Module-axiom|3}}.