df2idl2crng

Description: The predicate "is an ideal of the commutative ring R ". (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 27-Jun-2026)

	Ref	Expression
Hypotheses	df2idl2crng.u	$⊢ U = 2Ideal (R)$
	df2idl2crng.b	$⊢ B = {Base}_{R}$
	df2idl2crng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	df2idl2crng	$⊢ R \in CRing \to (I \in U \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I))$

Proof

Step	Hyp	Ref	Expression
1		df2idl2crng.u	$⊢ U = 2Ideal (R)$
2		df2idl2crng.b	$⊢ B = {Base}_{R}$
3		df2idl2crng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		crngring	$⊢ R \in CRing \to R \in Ring$
5	1 2 3	df2idl2	$⊢ R \in Ring \to (I \in U \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I)))$
6	4 5	syl	$⊢ R \in CRing \to (I \in U \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I)))$
7		simpll	$⊢ ((R \in CRing \land I \in SubGrp (R)) \land (x \in B \land y \in I)) \to R \in CRing$
8		simpl	$⊢ (x \in B \land y \in I) \to x \in B$
9	8	adantl	$⊢ ((R \in CRing \land I \in SubGrp (R)) \land (x \in B \land y \in I)) \to x \in B$
10	2	subgss	$⊢ I \in SubGrp (R) \to I \subseteq B$
11	10	adantl	$⊢ (R \in CRing \land I \in SubGrp (R)) \to I \subseteq B$
12	11	sseld	$⊢ (R \in CRing \land I \in SubGrp (R)) \to (y \in I \to y \in B)$
13	12	adantld	$⊢ (R \in CRing \land I \in SubGrp (R)) \to ((x \in B \land y \in I) \to y \in B)$
14	13	imp	$⊢ ((R \in CRing \land I \in SubGrp (R)) \land (x \in B \land y \in I)) \to y \in B$
15	2 3 7 9 14	crngcomd	$⊢ ((R \in CRing \land I \in SubGrp (R)) \land (x \in B \land y \in I)) \to x \underset{˙}{\cdot} y = y \underset{˙}{\cdot} x$
16	15	eleq1d	$⊢ ((R \in CRing \land I \in SubGrp (R)) \land (x \in B \land y \in I)) \to (x \underset{˙}{\cdot} y \in I \leftrightarrow y \underset{˙}{\cdot} x \in I)$
17	16	pm4.71da	$⊢ ((R \in CRing \land I \in SubGrp (R)) \land (x \in B \land y \in I)) \to (x \underset{˙}{\cdot} y \in I \leftrightarrow (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I))$
18	17	bicomd	$⊢ ((R \in CRing \land I \in SubGrp (R)) \land (x \in B \land y \in I)) \to ((x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I) \leftrightarrow x \underset{˙}{\cdot} y \in I)$
19	18	2ralbidva	$⊢ (R \in CRing \land I \in SubGrp (R)) \to (\forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I) \leftrightarrow \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I)$
20	19	pm5.32da	$⊢ R \in CRing \to ((I \in SubGrp (R) \land \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I)) \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I))$
21	6 20	bitrd	$⊢ R \in CRing \to (I \in U \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I))$

Metamath Proof Explorer

Theorem df2idl2crng

Proof