Definition df-rprm 27340

Description: Define the set of prime elements in a ring. A prime element is a nonzero non-unit that satisfies an equivalent of Euclid's lemma euclemma 15425. (Contributed by Mario Carneiro, 17-Feb-2015.)

Assertion

Ref	Expression
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 ) ) } )

Distinct variable group:   b, d, p, w, x, y

Detailed syntax breakdown of Definition df-rprm

Step	Hyp	Ref	Expression
1		crpm 27339	. 2 class RPrime
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1482	. . . . 5 class w
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` w )
8		vp	. . . . . . . . . . 11 setvar p
9	8	cv 1482	. . . . . . . . . 10 class p
10		vx	. . . . . . . . . . . 12 setvar x
11	10	cv 1482	. . . . . . . . . . 11 class x
12		vy	. . . . . . . . . . . 12 setvar y
13	12	cv 1482	. . . . . . . . . . 11 class y
14		cmulr 15942	. . . . . . . . . . . 12 class .r
15	5, 14	cfv 5888	. . . . . . . . . . 11 class ( .r ` w )
16	11, 13, 15	co 6650	. . . . . . . . . 10 class ( x ( .r ` w ) y )
17		vd	. . . . . . . . . . 11 setvar d
18	17	cv 1482	. . . . . . . . . 10 class d
19	9, 16, 18	wbr 4653	. . . . . . . . 9 wff p d ( x ( .r ` w ) y )
20	9, 11, 18	wbr 4653	. . . . . . . . . 10 wff p d x
21	9, 13, 18	wbr 4653	. . . . . . . . . 10 wff p d y
22	20, 21	wo 383	. . . . . . . . 9 wff ( p d x \/ p d y )
23	19, 22	wi 4	. . . . . . . 8 wff ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) )
24		cdsr 18638	. . . . . . . . 9 class ||r
25	5, 24	cfv 5888	. . . . . . . 8 class ( ||r ` w )
26	23, 17, 25	wsbc 3435	. . . . . . 7 wff [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) )
27	4	cv 1482	. . . . . . 7 class b
28	26, 12, 27	wral 2912	. . . . . 6 wff A. y e. b [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) )
29	28, 10, 27	wral 2912	. . . . 5 wff A. x e. b A. y e. b [. ( ||r ` w ) / d ]. ( p d ( x ( .r ` w ) y ) -> ( p d x \/ p d y ) )
30		cui 18639	. . . . . . . 8 class Unit
31	5, 30	cfv 5888	. . . . . . 7 class (Unit ` w )
32		c0g 16100	. . . . . . . . 9 class 0g
33	5, 32	cfv 5888	. . . . . . . 8 class ( 0g ` w )
34	33	csn 4177	. . . . . . 7 class { ( 0g ` w ) }
35	31, 34	cun 3572	. . . . . 6 class ( (Unit ` w ) u. { ( 0g ` w ) } )
36	27, 35	cdif 3571	. . . . 5 class ( b \ ( (Unit ` w ) u. { ( 0g ` w ) } ) )
37	29, 8, 36	crab 2916	. . . 4 class { 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	4, 7, 37	csb 3533	. . 3 class [_ ( 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	2, 3, 38	cmpt 4729	. 2 class ( 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 ) ) } )
40	1, 39	wceq 1483	1 wff 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 ) ) } )

This definition is referenced by: (None)