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 e. _V |-> [_ ( Base ` w ) / b ]_ { p e. ( b \ ( ( Unit ` w ) u. { ( 0g ` w ) } ) ) | A. x e. b A. y e. b [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crpm	|- RPrime
1		vw	|- w
2		cvv	|- _V
3		cbs	|- Base
4	1	cv	|- w
5	4 3	cfv	|- ( Base ` w )
6		vb	|- b
7		vp	|- p
8	6	cv	|- b
9		cui	|- Unit
10	4 9	cfv	|- ( Unit ` w )
11		c0g	|- 0g
12	4 11	cfv	|- ( 0g ` w )
13	12	csn	|- { ( 0g ` w ) }
14	10 13	cun	|- ( ( Unit ` w ) u. { ( 0g ` w ) } )
15	8 14	cdif	|- ( b \ ( ( Unit ` w ) u. { ( 0g ` w ) } ) )
16		vx	|- x
17		vy	|- y
18		cdsr	|- ||r
19	4 18	cfv	|- ( ||r ` w )
20		vd	|- d
21	7	cv	|- p
22	20	cv	|- d
23	16	cv	|- x
24		cmulr	|- .r
25	4 24	cfv	|- ( .r ` w )
26	17	cv	|- y
27	23 26 25	co	|- ( x ( .r ` w ) y )
28	21 27 22	wbr	|- p d ( x ( .r ` w ) y )
29	21 23 22	wbr	|- p d x
30	21 26 22	wbr	|- p d y
31	29 30	wo	|- ( p d x \/ p d y )
32	28 31	wi	|- ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) )
33	32 20 19	wsbc	|- [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) )
34	33 17 8	wral	|- A. y e. b [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) )
35	34 16 8	wral	|- A. x e. b A. y e. b [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) )
36	35 7 15	crab	|- { p e. ( b \ ( ( Unit ` w ) u. { ( 0g ` w ) } ) ) | A. x e. b A. y e. b [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) ) }
37	6 5 36	csb	|- [_ ( Base ` w ) / b ]_ { p e. ( b \ ( ( Unit ` w ) u. { ( 0g ` w ) } ) ) | A. x e. b A. y e. b [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) ) }
38	1 2 37	cmpt	|- ( w e. _V |-> [_ ( Base ` w ) / b ]_ { p e. ( b \ ( ( Unit ` w ) u. { ( 0g ` w ) } ) ) | A. x e. b A. y e. b [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) ) } )
39	0 38	wceq	|- RPrime = ( w e. _V |-> [_ ( Base ` w ) / b ]_ { p e. ( b \ ( ( Unit ` w ) u. { ( 0g ` w ) } ) ) | A. x e. b A. y e. b [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) ) } )