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 = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ 𝒫 ran ( 1^st ‘ 𝑟 ) ∣ ( ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cidl	⊢ Idl
1		vr	⊢ 𝑟
2		crngo	⊢ RingOps
3		vi	⊢ 𝑖
4		c1st	⊢ 1^st
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( 1^st ‘ 𝑟 )
7	6	crn	⊢ ran ( 1^st ‘ 𝑟 )
8	7	cpw	⊢ 𝒫 ran ( 1^st ‘ 𝑟 )
9		cgi	⊢ GId
10	6 9	cfv	⊢ ( GId ‘ ( 1^st ‘ 𝑟 ) )
11	3	cv	⊢ 𝑖
12	10 11	wcel	⊢ ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖
13		vx	⊢ 𝑥
14		vy	⊢ 𝑦
15	13	cv	⊢ 𝑥
16	14	cv	⊢ 𝑦
17	15 16 6	co	⊢ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 )
18	17 11	wcel	⊢ ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
19	18 14 11	wral	⊢ ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
20		vz	⊢ 𝑧
21	20	cv	⊢ 𝑧
22		c2nd	⊢ 2^nd
23	5 22	cfv	⊢ ( 2^nd ‘ 𝑟 )
24	21 15 23	co	⊢ ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 )
25	24 11	wcel	⊢ ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖
26	15 21 23	co	⊢ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 )
27	26 11	wcel	⊢ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖
28	25 27	wa	⊢ ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 )
29	28 20 7	wral	⊢ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 )
30	19 29	wa	⊢ ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) )
31	30 13 11	wral	⊢ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) )
32	12 31	wa	⊢ ( ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) )
33	32 3 8	crab	⊢ { 𝑖 ∈ 𝒫 ran ( 1^st ‘ 𝑟 ) ∣ ( ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) }
34	1 2 33	cmpt	⊢ ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ 𝒫 ran ( 1^st ‘ 𝑟 ) ∣ ( ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) } )
35	0 34	wceq	⊢ Idl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ 𝒫 ran ( 1^st ‘ 𝑟 ) ∣ ( ( GId ‘ ( 1^st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1^st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1^st ‘ 𝑟 ) ( ( 𝑧 ( 2^nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2^nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) } )

Metamath Proof Explorer

Definition df-idl

Detailed syntax breakdown