Metamath Proof Explorer


Definition 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 ( 1st𝑟 ) ∣ ( ( GId ‘ ( 1st𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥𝑖 ( ∀ 𝑦𝑖 ( 𝑥 ( 1st𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1st𝑟 ) ( ( 𝑧 ( 2nd𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2nd𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) } )

Detailed syntax breakdown

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