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 𝐵 = ( Base ‘ 𝑅 )
srgacl.p + = ( +g𝑅 )
Assertion srgacl ( ( 𝑅 ∈ SRing ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 srgacl.b 𝐵 = ( Base ‘ 𝑅 )
2 srgacl.p + = ( +g𝑅 )
3 srgmnd ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
4 1 2 mndcl ( ( 𝑅 ∈ Mnd ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
5 3 4 syl3an1 ( ( 𝑅 ∈ SRing ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )