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

Metamath Proof Explorer

Theorem subrgacl

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

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

Step	Hyp	Ref	Expression
1		subrgacl.p	$⊢ \underset{˙}{+} = +_{R}$
2		subrgsubg	$⊢ A \in SubRing (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 SubRing (R) \land X \in A \land Y \in A) \to X \underset{˙}{+} Y \in A$