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

Metamath Proof Explorer

Definition df-prmidl

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 prmidl2 and isprmidlc . (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Thierry Arnoux, 14-Jan-2024)

Ref Expression
Assertion df-prmidl PrmIdeal = ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprmidl ⊢ PrmIdeal
1 vr ⊢ 𝑟
2 crg ⊢ Ring
3 vi ⊢ 𝑖
4 clidl ⊢ LIdeal
5 1 cv ⊢ 𝑟
6 5 4 cfv ⊢ ( LIdeal ‘ 𝑟 )
7 3 cv ⊢ 𝑖
8 cbs ⊢ Base
9 5 8 cfv ⊢ ( Base ‘ 𝑟 )
10 7 9 wne ⊢ 𝑖 ≠ ( Base ‘ 𝑟 )
11 va ⊢ 𝑎
12 vb ⊢ 𝑏
13 vx ⊢ 𝑥
14 11 cv ⊢ 𝑎
15 vy ⊢ 𝑦
16 12 cv ⊢ 𝑏
17 13 cv ⊢ 𝑥
18 cmulr ⊢ .r
19 5 18 cfv ⊢ ( .r ‘ 𝑟 )
20 15 cv ⊢ 𝑦
21 17 20 19 co ⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 )
22 21 7 wcel ⊢ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
23 22 15 16 wral ⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
24 23 13 14 wral ⊢ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖
25 14 7 wss ⊢ 𝑎 ⊆ 𝑖
26 16 7 wss ⊢ 𝑏 ⊆ 𝑖
27 25 26 wo ⊢ ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 )
28 24 27 wi ⊢ ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
29 28 12 6 wral ⊢ ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
30 29 11 6 wral ⊢ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) )
31 10 30 wa ⊢ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) )
32 31 3 6 crab ⊢ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) }
33 1 2 32 cmpt ⊢ ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )
34 0 33 wceq ⊢ PrmIdeal = ( 𝑟 ∈ Ring ↦ { 𝑖 ∈ ( LIdeal ‘ 𝑟 ) ∣ ( 𝑖 ≠ ( Base ‘ 𝑟 ) ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑟 ) ∀ 𝑏 ∈ ( LIdeal ‘ 𝑟 ) ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 → ( 𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖 ) ) ) } )