Metamath Proof Explorer

Theorem idlsubcl

Description: An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010)

		Ref	Expression
	Hypotheses	idlsubcl.1	$⊢ G = 1^{st} (R)$
		idlsubcl.2	$⊢ D = /_{g} (G)$
	Assertion	idlsubcl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to A D B \in I$

Proof

Step	Hyp	Ref	Expression
1		idlsubcl.1	$⊢ G = 1^{st} (R)$
2		idlsubcl.2	$⊢ D = /_{g} (G)$
3		eqid	$⊢ ran G = ran G$
4	1 3	idlcl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land A \in I) \to A \in ran G$
5	1 3	idlcl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land B \in I) \to B \in ran G$
6	4 5	anim12dan	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to (A \in ran G \land B \in ran G)$
7		eqid	$⊢ inv (G) = inv (G)$
8	1 3 7 2	rngosub	$⊢ (R \in RingOps \land A \in ran G \land B \in ran G) \to A D B = A G inv (G) (B)$
9	8	3expb	$⊢ (R \in RingOps \land (A \in ran G \land B \in ran G)) \to A D B = A G inv (G) (B)$
10	9	adantlr	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in ran G \land B \in ran G)) \to A D B = A G inv (G) (B)$
11	6 10	syldan	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to A D B = A G inv (G) (B)$
12		simprl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to A \in I$
13	1 7	idlnegcl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land B \in I) \to inv (G) (B) \in I$
14	13	adantrl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to inv (G) (B) \in I$
15	12 14	jca	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to (A \in I \land inv (G) (B) \in I)$
16	1	idladdcl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land inv (G) (B) \in I)) \to A G inv (G) (B) \in I$
17	15 16	syldan	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to A G inv (G) (B) \in I$
18	11 17	eqeltrd	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to A D B \in I$