Theorem subrgacl

Description: A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		subrgacl.p	|- .+ = ( +g ` R )
2		subrgsubg	|- ( A e. ( SubRing ` 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. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .+ Y ) e. A )