Metamath Proof Explorer

Theorem idladdcl

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

		Ref	Expression
	Hypothesis	idladdcl.1	$⊢ G = 1^{st} (R)$
	Assertion	idladdcl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to A G B \in I$

Proof

Step	Hyp	Ref	Expression
1		idladdcl.1	$⊢ G = 1^{st} (R)$
2		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
3		eqid	$⊢ ran G = ran G$
4		eqid	$⊢ GId (G) = GId (G)$
5	1 2 3 4	isidl	$⊢ R \in RingOps \to (I \in Idl (R) \leftrightarrow (I \subseteq ran G \land GId (G) \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in ran G (z 2^{nd} (R) x \in I \land x 2^{nd} (R) z \in I))))$
6	5	biimpa	$⊢ (R \in RingOps \land I \in Idl (R)) \to (I \subseteq ran G \land GId (G) \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in ran G (z 2^{nd} (R) x \in I \land x 2^{nd} (R) z \in I)))$
7	6	simp3d	$⊢ (R \in RingOps \land I \in Idl (R)) \to \forall x \in I (\forall y \in I x G y \in I \land \forall z \in ran G (z 2^{nd} (R) x \in I \land x 2^{nd} (R) z \in I))$
8		simpl	$⊢ (\forall y \in I x G y \in I \land \forall z \in ran G (z 2^{nd} (R) x \in I \land x 2^{nd} (R) z \in I)) \to \forall y \in I x G y \in I$
9	8	ralimi	$⊢ \forall x \in I (\forall y \in I x G y \in I \land \forall z \in ran G (z 2^{nd} (R) x \in I \land x 2^{nd} (R) z \in I)) \to \forall x \in I \forall y \in I x G y \in I$
10	7 9	syl	$⊢ (R \in RingOps \land I \in Idl (R)) \to \forall x \in I \forall y \in I x G y \in I$
11		oveq1	$⊢ x = A \to x G y = A G y$
12	11	eleq1d	$⊢ x = A \to (x G y \in I \leftrightarrow A G y \in I)$
13		oveq2	$⊢ y = B \to A G y = A G B$
14	13	eleq1d	$⊢ y = B \to (A G y \in I \leftrightarrow A G B \in I)$
15	12 14	rspc2v	$⊢ (A \in I \land B \in I) \to (\forall x \in I \forall y \in I x G y \in I \to A G B \in I)$
16	10 15	mpan9	$⊢ ((R \in RingOps \land I \in Idl (R)) \land (A \in I \land B \in I)) \to A G B \in I$