Metamath Proof Explorer

Definition df-rprm

Description: Define the function associating with a ring its set of prime elements. A prime element is a nonzero non-unit that satisfies an equivalent of Euclid's lemma euclemma . Prime elements are closely related to irreducible elements (see df-irred ). (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Assertion df-rprm ⊢ RPrime = w ∈ V ⟼ ⦋ Base w / b⦌ p ∈ b ∖ Unit ⁡ w ∪ 0 w | ∀ x ∈ b ∀ y ∈ b [˙ ∥ r ⁡ w / d]˙ p d x ⋅ w y → p d x ∨ p d y

Detailed syntax breakdown

Step Hyp Ref Expression
0 crpm class RPrime
1 vw setvar w
2 cvv class V
3 cbs class Base
4 1 cv setvar w
5 4 3 cfv class Base w
6 vb setvar b
7 vp setvar p
8 6 cv setvar b
9 cui class Unit
10 4 9 cfv class Unit ⁡ w
11 c0g class 0 𝑔
12 4 11 cfv class 0 w
13 12 csn class 0 w
14 10 13 cun class Unit ⁡ w ∪ 0 w
15 8 14 cdif class b ∖ Unit ⁡ w ∪ 0 w
16 vx setvar x
17 vy setvar y
18 cdsr class ∥ r
19 4 18 cfv class ∥ r ⁡ w
20 vd setvar d
21 7 cv setvar p
22 20 cv setvar d
23 16 cv setvar x
24 cmulr class ⋅ 𝑟
25 4 24 cfv class ⋅ w
26 17 cv setvar y
27 23 26 25 co class x ⋅ w y
28 21 27 22 wbr wff p d x ⋅ w y
29 21 23 22 wbr wff p d x
30 21 26 22 wbr wff p d y
31 29 30 wo wff p d x ∨ p d y
32 28 31 wi wff p d x ⋅ w y → p d x ∨ p d y
33 32 20 19 wsbc wff [˙ ∥ r ⁡ w / d]˙ p d x ⋅ w y → p d x ∨ p d y
34 33 17 8 wral wff ∀ y ∈ b [˙ ∥ r ⁡ w / d]˙ p d x ⋅ w y → p d x ∨ p d y
35 34 16 8 wral wff ∀ x ∈ b ∀ y ∈ b [˙ ∥ r ⁡ w / d]˙ p d x ⋅ w y → p d x ∨ p d y
36 35 7 15 crab class p ∈ b ∖ Unit ⁡ w ∪ 0 w | ∀ x ∈ b ∀ y ∈ b [˙ ∥ r ⁡ w / d]˙ p d x ⋅ w y → p d x ∨ p d y
37 6 5 36 csb class ⦋ Base w / b⦌ p ∈ b ∖ Unit ⁡ w ∪ 0 w | ∀ x ∈ b ∀ y ∈ b [˙ ∥ r ⁡ w / d]˙ p d x ⋅ w y → p d x ∨ p d y
38 1 2 37 cmpt class w ∈ V ⟼ ⦋ Base w / b⦌ p ∈ b ∖ Unit ⁡ w ∪ 0 w | ∀ x ∈ b ∀ y ∈ b [˙ ∥ r ⁡ w / d]˙ p d x ⋅ w y → p d x ∨ p d y
39 0 38 wceq wff RPrime = w ∈ V ⟼ ⦋ Base w / b⦌ p ∈ b ∖ Unit ⁡ w ∪ 0 w | ∀ x ∈ b ∀ y ∈ b [˙ ∥ r ⁡ w / d]˙ p d x ⋅ w y → p d x ∨ p d y