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={\mathrm{Base}}_R$$
	rngacl.p	$$⊢\underset{\dot{}}{+}={+}_R$$
Assertion	rngacl	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		rngacl.b	$$⊢B={\mathrm{Base}}_R$$
2		rngacl.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
4	1 2	grpcl	$$⊢\left(R\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
5	3 4	syl3an1	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$