This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-pridl

Description: Define the class of prime ideals of a ring R . A proper ideal I of R is prime if whenever A B C_ I for ideals A and B , either A C_ I or B C_ I . The more familiar definition using elements rather than ideals is equivalent provided R is commutative; see ispridl2 and ispridlc . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion df-pridl PrIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpridl ⊢ PrIdl
1 vr ⊢ 𝑟
2 crngo ⊢ RingOps
3 vi ⊢ 𝑖
4 cidl ⊢ Idl
5 1 cv ⊢ 𝑟
6 5 4 cfv ⊢ ( Idl ‘ 𝑟 )
7 3 cv ⊢ 𝑖
8 c1st ⊢ 1st
9 5 8 cfv ⊢ ( 1st ‘ 𝑟 )
10 9 crn ⊢ ran ( 1st ‘ 𝑟 )
11 7 10 wne ⊢ 𝑖 ≠ ran ( 1st ‘ 𝑟 )
12 va ⊢ 𝑎
13 vb ⊢ 𝑏
14 vx ⊢ 𝑥
15 12 cv ⊢ 𝑎
16 vy ⊢ 𝑦
17 13 cv ⊢ 𝑏
18 14 cv ⊢ 𝑥
19 c2nd ⊢ 2nd
20 5 19 cfv ⊢ ( 2nd ‘ 𝑟 )
21 16 cv ⊢ 𝑦
22 18 21 20 co ⊢ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 )
23 22 7 wcel ⊢ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
24 23 16 17 wral ⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
25 24 14 15 wral ⊢ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
26 15 7 wss ⊢ 𝑎 ⊆ 𝑖
27 17 7 wss ⊢ 𝑏 ⊆ 𝑖
28 26 27 wo ⊢ ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 )
29 25 28 wi ⊢ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
30 29 13 6 wral ⊢ ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
31 30 12 6 wral ⊢ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
32 11 31 wa ⊢ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) )
33 32 3 6 crab ⊢ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) }
34 1 2 33 cmpt ⊢ ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )
35 0 34 wceq ⊢ PrIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( Idl ‘ 𝑟 ) ∀ 𝑏 ∈ ( Idl ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )