Description: Closure of the addition operation of a semiring. (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Thierry Arnoux, 1-Apr-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | srgacl.b | |- B = ( Base ` R ) |
|
srgacl.p | |- .+ = ( +g ` R ) |
||
Assertion | srgacl | |- ( ( R e. SRing /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | srgacl.b | |- B = ( Base ` R ) |
|
2 | srgacl.p | |- .+ = ( +g ` R ) |
|
3 | srgmnd | |- ( R e. SRing -> R e. Mnd ) |
|
4 | 1 2 | mndcl | |- ( ( R e. Mnd /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B ) |
5 | 3 4 | syl3an1 | |- ( ( R e. SRing /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B ) |