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

Definition df-zn 16474
Description: Define the ring of integers  mod  n. This is literally the quotient ring of  ZZ by the ideal  n ZZ, but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.)
Assertion
Ref Expression
df-zn  |- ℤ/n =  ( n  e. 
NN0  |->  [_ (flds  ZZ )  /  z ]_ [_ ( z  /.s  ( z ~QG  (
(RSpan `  z ) `  { n } ) ) )  /  s ]_ ( s sSet  <. ( le `  ndx ) , 
[_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  /  f ]_ (
( f  o.  <_  )  o.  `' f )
>. ) )
Distinct variable group:    z, n, s, f

Detailed syntax breakdown of Definition df-zn
StepHypRef Expression
1 czn 16470 . 2  class ℤ/n
2 vn . . 3  set  n
3 cn0 9981 . . 3  class  NN0
4 vz . . . 4  set  z
5 ccnfld 16393 . . . . 5  classfld
6 cz 10040 . . . . 5  class  ZZ
7 cress 13165 . . . . 5  classs
85, 6, 7co 5874 . . . 4  class  (flds  ZZ )
9 vs . . . . 5  set  s
104cv 1631 . . . . . 6  class  z
112cv 1631 . . . . . . . . 9  class  n
1211csn 3653 . . . . . . . 8  class  { n }
13 crsp 15940 . . . . . . . . 9  class RSpan
1410, 13cfv 5271 . . . . . . . 8  class  (RSpan `  z )
1512, 14cfv 5271 . . . . . . 7  class  ( (RSpan `  z ) `  {
n } )
16 cqg 14633 . . . . . . 7  class ~QG
1710, 15, 16co 5874 . . . . . 6  class  ( z ~QG  ( (RSpan `  z ) `  { n } ) )
18 cqus 13424 . . . . . 6  class  /.s
1910, 17, 18co 5874 . . . . 5  class  ( z 
/.s  ( z ~QG  ( (RSpan `  z
) `  { n } ) ) )
209cv 1631 . . . . . 6  class  s
21 cnx 13161 . . . . . . . 8  class  ndx
22 cple 13231 . . . . . . . 8  class  le
2321, 22cfv 5271 . . . . . . 7  class  ( le
`  ndx )
24 vf . . . . . . . 8  set  f
25 czrh 16467 . . . . . . . . . 10  class  ZRHom
2620, 25cfv 5271 . . . . . . . . 9  class  ( ZRHom `  s )
27 cc0 8753 . . . . . . . . . . 11  class  0
2811, 27wceq 1632 . . . . . . . . . 10  wff  n  =  0
29 cfzo 10886 . . . . . . . . . . 11  class ..^
3027, 11, 29co 5874 . . . . . . . . . 10  class  ( 0..^ n )
3128, 6, 30cif 3578 . . . . . . . . 9  class  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) )
3226, 31cres 4707 . . . . . . . 8  class  ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ , 
( 0..^ n ) ) )
3324cv 1631 . . . . . . . . . 10  class  f
34 cle 8884 . . . . . . . . . 10  class  <_
3533, 34ccom 4709 . . . . . . . . 9  class  ( f  o.  <_  )
3633ccnv 4704 . . . . . . . . 9  class  `' f
3735, 36ccom 4709 . . . . . . . 8  class  ( ( f  o.  <_  )  o.  `' f )
3824, 32, 37csb 3094 . . . . . . 7  class  [_ (
( ZRHom `  s
)  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  / 
f ]_ ( ( f  o.  <_  )  o.  `' f )
3923, 38cop 3656 . . . . . 6  class  <. ( le `  ndx ) , 
[_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  /  f ]_ (
( f  o.  <_  )  o.  `' f )
>.
40 csts 13162 . . . . . 6  class sSet
4120, 39, 40co 5874 . . . . 5  class  ( s sSet  <. ( le `  ndx ) ,  [_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ , 
( 0..^ n ) ) )  /  f ]_ ( ( f  o. 
<_  )  o.  `' f ) >. )
429, 19, 41csb 3094 . . . 4  class  [_ (
z  /.s  ( z ~QG  ( (RSpan `  z
) `  { n } ) ) )  /  s ]_ (
s sSet  <. ( le `  ndx ) ,  [_ (
( ZRHom `  s
)  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  / 
f ]_ ( ( f  o.  <_  )  o.  `' f ) >.
)
434, 8, 42csb 3094 . . 3  class  [_ (flds  ZZ )  /  z ]_ [_ (
z  /.s  ( z ~QG  ( (RSpan `  z
) `  { n } ) ) )  /  s ]_ (
s sSet  <. ( le `  ndx ) ,  [_ (
( ZRHom `  s
)  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  / 
f ]_ ( ( f  o.  <_  )  o.  `' f ) >.
)
442, 3, 43cmpt 4093 . 2  class  ( n  e.  NN0  |->  [_ (flds  ZZ )  /  z ]_ [_ (
z  /.s  ( z ~QG  ( (RSpan `  z
) `  { n } ) ) )  /  s ]_ (
s sSet  <. ( le `  ndx ) ,  [_ (
( ZRHom `  s
)  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  / 
f ]_ ( ( f  o.  <_  )  o.  `' f ) >.
) )
451, 44wceq 1632 1  wff ℤ/n =  ( n  e. 
NN0  |->  [_ (flds  ZZ )  /  z ]_ [_ ( z  /.s  ( z ~QG  (
(RSpan `  z ) `  { n } ) ) )  /  s ]_ ( s sSet  <. ( le `  ndx ) , 
[_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  /  f ]_ (
( f  o.  <_  )  o.  `' f )
>. ) )
Colors of variables: wff set class
This definition is referenced by:  znval  16505
  Copyright terms: Public domain W3C validator