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

Metamath Proof Explorer

Theorem rngacl

Description: Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025)

	Ref	Expression
Hypotheses	rngacl.b	$⊢ B = {Base}_{R}$
	rngacl.p	$⊢ \underset{˙}{+} = +_{R}$
Assertion	rngacl	$⊢ (R \in Rng \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$

Step	Hyp	Ref	Expression
1		rngacl.b	$⊢ B = {Base}_{R}$
2		rngacl.p	$⊢ \underset{˙}{+} = +_{R}$
3		rnggrp	$⊢ R \in Rng \to R \in Grp$
4	1 2	grpcl	$⊢ (R \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$
5	3 4	syl3an1	$⊢ (R \in Rng \land X \in B \land Y \in B) \to X \underset{˙}{+} Y \in B$