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
|- .+ = ( +g ` R )
Assertion rngacl
|- ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )

Proof

Step Hyp Ref Expression
1 rngacl.b
 |-  B = ( Base ` R )
2 rngacl.p
 |-  .+ = ( +g ` R )
3 rnggrp
 |-  ( R e. Rng -> R e. Grp )
4 1 2 grpcl
 |-  ( ( R e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
5 3 4 syl3an1
 |-  ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )