Theorem subrngacl

Description: A subring is closed under addition. (Contributed by AV, 14-Feb-2025)

	Ref	Expression
Hypothesis	subrngacl.p	|- .+ = ( +g ` R )
Assertion	subrngacl	|- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .+ Y ) e. A )

Proof

Step	Hyp	Ref	Expression
1		subrngacl.p	|- .+ = ( +g ` R )
2		subrngsubg	|- ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) )
3	1	subgcl	|- ( ( A e. ( SubGrp ` R ) /\ X e. A /\ Y e. A ) -> ( X .+ Y ) e. A )
4	2 3	syl3an1	|- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .+ Y ) e. A )