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

Definition df-domn 16025
Description: A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.)
Assertion
Ref Expression
df-domn  |- Domn  =  {
r  e. NzRing  |  [. ( Base `  r )  / 
b ]. [. ( 0g
`  r )  / 
z ]. A. x  e.  b  A. y  e.  b  ( ( x ( .r `  r
) y )  =  z  ->  ( x  =  z  \/  y  =  z ) ) }
Distinct variable group:    r, b, x, y, z

Detailed syntax breakdown of Definition df-domn
StepHypRef Expression
1 cdomn 16021 . 2  class Domn
2 vx . . . . . . . . . . 11  set  x
32cv 1622 . . . . . . . . . 10  class  x
4 vy . . . . . . . . . . 11  set  y
54cv 1622 . . . . . . . . . 10  class  y
6 vr . . . . . . . . . . . 12  set  r
76cv 1622 . . . . . . . . . . 11  class  r
8 cmulr 13209 . . . . . . . . . . 11  class  .r
97, 8cfv 5255 . . . . . . . . . 10  class  ( .r
`  r )
103, 5, 9co 5858 . . . . . . . . 9  class  ( x ( .r `  r
) y )
11 vz . . . . . . . . . 10  set  z
1211cv 1622 . . . . . . . . 9  class  z
1310, 12wceq 1623 . . . . . . . 8  wff  ( x ( .r `  r
) y )  =  z
142, 11weq 1624 . . . . . . . . 9  wff  x  =  z
154, 11weq 1624 . . . . . . . . 9  wff  y  =  z
1614, 15wo 357 . . . . . . . 8  wff  ( x  =  z  \/  y  =  z )
1713, 16wi 4 . . . . . . 7  wff  ( ( x ( .r `  r ) y )  =  z  ->  (
x  =  z  \/  y  =  z ) )
18 vb . . . . . . . 8  set  b
1918cv 1622 . . . . . . 7  class  b
2017, 4, 19wral 2543 . . . . . 6  wff  A. y  e.  b  ( (
x ( .r `  r ) y )  =  z  ->  (
x  =  z  \/  y  =  z ) )
2120, 2, 19wral 2543 . . . . 5  wff  A. x  e.  b  A. y  e.  b  ( (
x ( .r `  r ) y )  =  z  ->  (
x  =  z  \/  y  =  z ) )
22 c0g 13400 . . . . . 6  class  0g
237, 22cfv 5255 . . . . 5  class  ( 0g
`  r )
2421, 11, 23wsbc 2991 . . . 4  wff  [. ( 0g `  r )  / 
z ]. A. x  e.  b  A. y  e.  b  ( ( x ( .r `  r
) y )  =  z  ->  ( x  =  z  \/  y  =  z ) )
25 cbs 13148 . . . . 5  class  Base
267, 25cfv 5255 . . . 4  class  ( Base `  r )
2724, 18, 26wsbc 2991 . . 3  wff  [. ( Base `  r )  / 
b ]. [. ( 0g
`  r )  / 
z ]. A. x  e.  b  A. y  e.  b  ( ( x ( .r `  r
) y )  =  z  ->  ( x  =  z  \/  y  =  z ) )
28 cnzr 16009 . . 3  class NzRing
2927, 6, 28crab 2547 . 2  class  { r  e. NzRing  |  [. ( Base `  r )  /  b ]. [. ( 0g `  r )  /  z ]. A. x  e.  b 
A. y  e.  b  ( ( x ( .r `  r ) y )  =  z  ->  ( x  =  z  \/  y  =  z ) ) }
301, 29wceq 1623 1  wff Domn  =  {
r  e. NzRing  |  [. ( Base `  r )  / 
b ]. [. ( 0g
`  r )  / 
z ]. A. x  e.  b  A. y  e.  b  ( ( x ( .r `  r
) y )  =  z  ->  ( x  =  z  \/  y  =  z ) ) }
Colors of variables: wff set class
This definition is referenced by:  isdomn  16035
  Copyright terms: Public domain W3C validator