This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \underset{˙}{+} = +_{R}$
Assertion	srgacl	$⊢ (R \in SRing \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$

Proof

Step	Hyp	Ref	Expression
1		srgacl.b	$⊢ B = {Base}_{R}$
2		srgacl.p	$⊢ \underset{˙}{+} = +_{R}$
3		srgmnd	$⊢ R \in SRing \to R \in Mnd$
4	1 2	mndcl	$⊢ (R \in Mnd \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
5	3 4	syl3an1	$⊢ (R \in SRing \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$