lidlsubcl

Description: An ideal is closed under subtraction. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by OpenAI, 25-Mar-2020)

	Ref	Expression
Hypotheses	lidlcl.u	$⊢ U = LIdeal (R)$
	lidlsubcl.m	$⊢ \underset{˙}{-} = -_{R}$
Assertion	lidlsubcl	$⊢ ((R \in Ring \land I \in U) \land (X \in I \land Y \in I)) \to X \underset{˙}{-} Y \in I$

Step	Hyp	Ref	Expression
1		lidlcl.u	$⊢ U = LIdeal (R)$
2		lidlsubcl.m	$⊢ \underset{˙}{-} = -_{R}$
3	1	lidlsubg	$⊢ (R \in Ring \land I \in U) \to I \in SubGrp (R)$
4	3	3adant3	$⊢ (R \in Ring \land I \in U \land (X \in I \land Y \in I)) \to I \in SubGrp (R)$
5		simp3l	$⊢ (R \in Ring \land I \in U \land (X \in I \land Y \in I)) \to X \in I$
6		simp3r	$⊢ (R \in Ring \land I \in U \land (X \in I \land Y \in I)) \to Y \in I$
7	2	subgsubcl	$⊢ (I \in SubGrp (R) \land X \in I \land Y \in I) \to X \underset{˙}{-} Y \in I$
8	4 5 6 7	syl3anc	$⊢ (R \in Ring \land I \in U \land (X \in I \land Y \in I)) \to X \underset{˙}{-} Y \in I$
9	8	3expa	$⊢ ((R \in Ring \land I \in U) \land (X \in I \land Y \in I)) \to X \underset{˙}{-} Y \in I$

Metamath Proof Explorer