Metamath Proof Explorer


Theorem srgacl

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 )

Proof

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 )