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 = ( 𝑤 ∈ V ↦ ⦋ ( Base ‘ 𝑤 ) / 𝑏 ⦌ { 𝑝 ∈ ( 𝑏 ∖ ( ( Unit ‘ 𝑤 ) ∪ { ( 0g ‘ 𝑤 ) } ) ) ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑤 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crpm	⊢ RPrime
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		cbs	⊢ Base
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( Base ‘ 𝑤 )
6		vb	⊢ 𝑏
7		vp	⊢ 𝑝
8	6	cv	⊢ 𝑏
9		cui	⊢ Unit
10	4 9	cfv	⊢ ( Unit ‘ 𝑤 )
11		c0g	⊢ 0g
12	4 11	cfv	⊢ ( 0g ‘ 𝑤 )
13	12	csn	⊢ { ( 0g ‘ 𝑤 ) }
14	10 13	cun	⊢ ( ( Unit ‘ 𝑤 ) ∪ { ( 0g ‘ 𝑤 ) } )
15	8 14	cdif	⊢ ( 𝑏 ∖ ( ( Unit ‘ 𝑤 ) ∪ { ( 0g ‘ 𝑤 ) } ) )
16		vx	⊢ 𝑥
17		vy	⊢ 𝑦
18		cdsr	⊢ ∥r
19	4 18	cfv	⊢ ( ∥r ‘ 𝑤 )
20		vd	⊢ 𝑑
21	7	cv	⊢ 𝑝
22	20	cv	⊢ 𝑑
23	16	cv	⊢ 𝑥
24		cmulr	⊢ .r
25	4 24	cfv	⊢ ( .r ‘ 𝑤 )
26	17	cv	⊢ 𝑦
27	23 26 25	co	⊢ ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 )
28	21 27 22	wbr	⊢ 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 )
29	21 23 22	wbr	⊢ 𝑝 𝑑 𝑥
30	21 26 22	wbr	⊢ 𝑝 𝑑 𝑦
31	29 30	wo	⊢ ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 )
32	28 31	wi	⊢ ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) )
33	32 20 19	wsbc	⊢ [ ( ∥r ‘ 𝑤 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) )
34	33 17 8	wral	⊢ ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑤 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) )
35	34 16 8	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑤 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) )
36	35 7 15	crab	⊢ { 𝑝 ∈ ( 𝑏 ∖ ( ( Unit ‘ 𝑤 ) ∪ { ( 0g ‘ 𝑤 ) } ) ) ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑤 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) }
37	6 5 36	csb	⊢ ⦋ ( Base ‘ 𝑤 ) / 𝑏 ⦌ { 𝑝 ∈ ( 𝑏 ∖ ( ( Unit ‘ 𝑤 ) ∪ { ( 0g ‘ 𝑤 ) } ) ) ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑤 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) }
38	1 2 37	cmpt	⊢ ( 𝑤 ∈ V ↦ ⦋ ( Base ‘ 𝑤 ) / 𝑏 ⦌ { 𝑝 ∈ ( 𝑏 ∖ ( ( Unit ‘ 𝑤 ) ∪ { ( 0g ‘ 𝑤 ) } ) ) ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑤 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) } )
39	0 38	wceq	⊢ RPrime = ( 𝑤 ∈ V ↦ ⦋ ( Base ‘ 𝑤 ) / 𝑏 ⦌ { 𝑝 ∈ ( 𝑏 ∖ ( ( Unit ‘ 𝑤 ) ∪ { ( 0g ‘ 𝑤 ) } ) ) ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑤 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑤 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) } )