MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rprm Unicode version

Definition df-rprm 20864
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 12803. (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
StepHypRef Expression
1 crpm 20863 . 2  class RPrime
2 vw . . 3  set  w
3 cvv 2801 . . 3  class  _V
4 vb . . . 4  set  b
52cv 1631 . . . . 5  class  w
6 cbs 13164 . . . . 5  class  Base
75, 6cfv 5271 . . . 4  class  ( Base `  w )
8 vp . . . . . . . . . . 11  set  p
98cv 1631 . . . . . . . . . 10  class  p
10 vx . . . . . . . . . . . 12  set  x
1110cv 1631 . . . . . . . . . . 11  class  x
12 vy . . . . . . . . . . . 12  set  y
1312cv 1631 . . . . . . . . . . 11  class  y
14 cmulr 13225 . . . . . . . . . . . 12  class  .r
155, 14cfv 5271 . . . . . . . . . . 11  class  ( .r
`  w )
1611, 13, 15co 5874 . . . . . . . . . 10  class  ( x ( .r `  w
) y )
17 vd . . . . . . . . . . 11  set  d
1817cv 1631 . . . . . . . . . 10  class  d
199, 16, 18wbr 4039 . . . . . . . . 9  wff  p d ( x ( .r
`  w ) y )
209, 11, 18wbr 4039 . . . . . . . . . 10  wff  p d x
219, 13, 18wbr 4039 . . . . . . . . . 10  wff  p d y
2220, 21wo 357 . . . . . . . . 9  wff  ( p d x  \/  p
d y )
2319, 22wi 4 . . . . . . . 8  wff  ( p d ( x ( .r `  w ) y )  ->  (
p d x  \/  p d y ) )
24 cdsr 15436 . . . . . . . . 9  class  ||r
255, 24cfv 5271 . . . . . . . 8  class  ( ||r `  w
)
2623, 17, 25wsbc 3004 . . . . . . 7  wff  [. ( ||r `  w )  /  d ]. ( p d ( x ( .r `  w ) y )  ->  ( p d x  \/  p d y ) )
274cv 1631 . . . . . . 7  class  b
2826, 12, 27wral 2556 . . . . . 6  wff  A. y  e.  b  [. ( ||r `  w
)  /  d ]. ( p d ( x ( .r `  w ) y )  ->  ( p d x  \/  p d y ) )
2928, 10, 27wral 2556 . . . . 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 15437 . . . . . . . 8  class Unit
315, 30cfv 5271 . . . . . . 7  class  (Unit `  w )
32 c0g 13416 . . . . . . . . 9  class  0g
335, 32cfv 5271 . . . . . . . 8  class  ( 0g
`  w )
3433csn 3653 . . . . . . 7  class  { ( 0g `  w ) }
3531, 34cun 3163 . . . . . 6  class  ( (Unit `  w )  u.  {
( 0g `  w
) } )
3627, 35cdif 3162 . . . . 5  class  ( b 
\  ( (Unit `  w )  u.  {
( 0g `  w
) } ) )
3729, 8, 36crab 2560 . . . 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 ) ) }
384, 7, 37csb 3094 . . 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 ) ) }
392, 3, 38cmpt 4093 . 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 ) ) } )
401, 39wceq 1632 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 ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator