Metamath Proof Explorer

Definition df-domn

Description: Adomain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdomn 
 |-  Domn
1 vr 
 |-  r
2 cnzr 
 |-  NzRing
3 cbs 
 |-  Base
4 1 cv 
 |-  r
5 4 3 cfv 
 |-  ( Base ` r )
6 vb 
 |-  b
7 c0g 
 |-  0g
8 4 7 cfv 
 |-  ( 0g ` r )
9 vz 
 |-  z
10 vx 
 |-  x
11 6 cv 
 |-  b
12 vy 
 |-  y
13 10 cv 
 |-  x
14 cmulr 
 |-  .r
15 4 14 cfv 
 |-  ( .r ` r )
16 12 cv 
 |-  y
17 13 16 15 co 
 |-  ( x ( .r ` r ) y )
18 9 cv 
 |-  z
19 17 18 wceq 
 |-  ( x ( .r ` r ) y ) = z
20 13 18 wceq 
 |-  x = z
21 16 18 wceq 
 |-  y = z
22 20 21 wo 
 |-  ( x = z \/ y = z )
23 19 22 wi 
 |-  ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
24 23 12 11 wral 
 |-  A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
25 24 10 11 wral 
 |-  A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
26 25 9 8 wsbc 
 |-  [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
27 26 6 5 wsbc 
 |-  [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) )
28 27 1 2 crab 
 |-  { 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 ) ) }
29 0 28 wceq 
 |-  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 ) ) }