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

Metamath Proof Explorer

Theorem subrngacl

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

		Ref	Expression
	Hypothesis	subrngacl.p	$⊢ \underset{˙}{+} = +_{R}$
	Assertion	subrngacl	$⊢ (A \in SubRng (R) \land X \in A \land Y \in A) \to X \underset{˙}{+} Y \in A$

Step	Hyp	Ref	Expression
1		subrngacl.p	$⊢ \underset{˙}{+} = +_{R}$
2		subrngsubg	$⊢ A \in SubRng (R) \to A \in SubGrp (R)$
3	1	subgcl	$⊢ (A \in SubGrp (R) \land X \in A \land Y \in A) \to X \underset{˙}{+} Y \in A$
4	2 3	syl3an1	$⊢ (A \in SubRng (R) \land X \in A \land Y \in A) \to X \underset{˙}{+} Y \in A$