df-idl

Description: Define the class of (two-sided) ideals of a ring R . A subset of R is an ideal if it contains 0 , is closed under addition, and is closed under multiplication on either side by any element of R . (Contributed by Jeff Madsen, 10-Jun-2010)

		Ref	Expression
	Assertion	df-idl	$⊢ Idl = (r \in RingOps ⟼ \{i \in 𝒫 ran 1^{st} (r) \| (GId (1^{st} (r)) \in i \land \forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cidl	$class Idl$
1		vr	$setvar r$
2		crngo	$class RingOps$
3		vi	$setvar i$
4		c1st	$class 1^{st}$
5	1	cv	$setvar r$
6	5 4	cfv	$class 1^{st} (r)$
7	6	crn	$class ran 1^{st} (r)$
8	7	cpw	$class 𝒫 ran 1^{st} (r)$
9		cgi	$class GId$
10	6 9	cfv	$class GId (1^{st} (r))$
11	3	cv	$setvar i$
12	10 11	wcel	$wff GId (1^{st} (r)) \in i$
13		vx	$setvar x$
14		vy	$setvar y$
15	13	cv	$setvar x$
16	14	cv	$setvar y$
17	15 16 6	co	$class (x 1^{st} (r) y)$
18	17 11	wcel	$wff x 1^{st} (r) y \in i$
19	18 14 11	wral	$wff \forall y \in i x 1^{st} (r) y \in i$
20		vz	$setvar z$
21	20	cv	$setvar z$
22		c2nd	$class 2^{nd}$
23	5 22	cfv	$class 2^{nd} (r)$
24	21 15 23	co	$class (z 2^{nd} (r) x)$
25	24 11	wcel	$wff z 2^{nd} (r) x \in i$
26	15 21 23	co	$class (x 2^{nd} (r) z)$
27	26 11	wcel	$wff x 2^{nd} (r) z \in i$
28	25 27	wa	$wff (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)$
29	28 20 7	wral	$wff \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)$
30	19 29	wa	$wff (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i))$
31	30 13 11	wral	$wff \forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i))$
32	12 31	wa	$wff (GId (1^{st} (r)) \in i \land \forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)))$
33	32 3 8	crab	$class \{i \in 𝒫 ran 1^{st} (r) \| (GId (1^{st} (r)) \in i \land \forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)))\}$
34	1 2 33	cmpt	$class (r \in RingOps ⟼ \{i \in 𝒫 ran 1^{st} (r) \| (GId (1^{st} (r)) \in i \land \forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)))\})$
35	0 34	wceq	$wff Idl = (r \in RingOps ⟼ \{i \in 𝒫 ran 1^{st} (r) \| (GId (1^{st} (r)) \in i \land \forall x \in i (\forall y \in i x 1^{st} (r) y \in i \land \forall z \in ran 1^{st} (r) (z 2^{nd} (r) x \in i \land x 2^{nd} (r) z \in i)))\})$

Metamath Proof Explorer

Definition df-idl

Detailed syntax breakdown