isidlc

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

	Ref	Expression
Hypotheses	idlval.1	$⊢ G = 1^{st} (R)$
	idlval.2	$⊢ H = 2^{nd} (R)$
	idlval.3	$⊢ X = ran G$
	idlval.4	$⊢ Z = GId (G)$
Assertion	isidlc	$⊢ R \in CRingOps \to (I \in Idl (R) \leftrightarrow (I \subseteq X \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X z H x \in I)))$

Proof

Step	Hyp	Ref	Expression
1		idlval.1	$⊢ G = 1^{st} (R)$
2		idlval.2	$⊢ H = 2^{nd} (R)$
3		idlval.3	$⊢ X = ran G$
4		idlval.4	$⊢ Z = GId (G)$
5		crngorngo	$⊢ R \in CRingOps \to R \in RingOps$
6	1 2 3 4	isidl	$⊢ R \in RingOps \to (I \in Idl (R) \leftrightarrow (I \subseteq X \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I))))$
7	5 6	syl	$⊢ R \in CRingOps \to (I \in Idl (R) \leftrightarrow (I \subseteq X \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I))))$
8		ssel2	$⊢ (I \subseteq X \land x \in I) \to x \in X$
9	1 2 3	crngocom	$⊢ (R \in CRingOps \land x \in X \land z \in X) \to x H z = z H x$
10	9	eleq1d	$⊢ (R \in CRingOps \land x \in X \land z \in X) \to (x H z \in I \leftrightarrow z H x \in I)$
11	10	biimprd	$⊢ (R \in CRingOps \land x \in X \land z \in X) \to (z H x \in I \to x H z \in I)$
12	11	3expa	$⊢ ((R \in CRingOps \land x \in X) \land z \in X) \to (z H x \in I \to x H z \in I)$
13	12	pm4.71d	$⊢ ((R \in CRingOps \land x \in X) \land z \in X) \to (z H x \in I \leftrightarrow (z H x \in I \land x H z \in I))$
14	13	bicomd	$⊢ ((R \in CRingOps \land x \in X) \land z \in X) \to ((z H x \in I \land x H z \in I) \leftrightarrow z H x \in I)$
15	14	ralbidva	$⊢ (R \in CRingOps \land x \in X) \to (\forall z \in X (z H x \in I \land x H z \in I) \leftrightarrow \forall z \in X z H x \in I)$
16	15	anbi2d	$⊢ (R \in CRingOps \land x \in X) \to ((\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I)) \leftrightarrow (\forall y \in I x G y \in I \land \forall z \in X z H x \in I))$
17	8 16	sylan2	$⊢ (R \in CRingOps \land (I \subseteq X \land x \in I)) \to ((\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I)) \leftrightarrow (\forall y \in I x G y \in I \land \forall z \in X z H x \in I))$
18	17	anassrs	$⊢ ((R \in CRingOps \land I \subseteq X) \land x \in I) \to ((\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I)) \leftrightarrow (\forall y \in I x G y \in I \land \forall z \in X z H x \in I))$
19	18	ralbidva	$⊢ (R \in CRingOps \land I \subseteq X) \to (\forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I)) \leftrightarrow \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X z H x \in I))$
20	19	adantrr	$⊢ (R \in CRingOps \land (I \subseteq X \land Z \in I)) \to (\forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I)) \leftrightarrow \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X z H x \in I))$
21	20	pm5.32da	$⊢ R \in CRingOps \to (((I \subseteq X \land Z \in I) \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I))) \leftrightarrow ((I \subseteq X \land Z \in I) \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X z H x \in I)))$
22		df-3an	$⊢ (I \subseteq X \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I))) \leftrightarrow ((I \subseteq X \land Z \in I) \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I)))$
23		df-3an	$⊢ (I \subseteq X \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X z H x \in I)) \leftrightarrow ((I \subseteq X \land Z \in I) \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X z H x \in I))$
24	21 22 23	3bitr4g	$⊢ R \in CRingOps \to ((I \subseteq X \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X (z H x \in I \land x H z \in I))) \leftrightarrow (I \subseteq X \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X z H x \in I)))$
25	7 24	bitrd	$⊢ R \in CRingOps \to (I \in Idl (R) \leftrightarrow (I \subseteq X \land Z \in I \land \forall x \in I (\forall y \in I x G y \in I \land \forall z \in X z H x \in I)))$

Metamath Proof Explorer

Theorem isidlc

Proof