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

Definition df-zn 16458
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 16454 . 2  class ℤ/n
2 vn . . 3  set  n
3 cn0 9965 . . 3  class  NN0
4 vz . . . 4  set  z
5 ccnfld 16377 . . . . 5  classfld
6 cz 10024 . . . . 5  class  ZZ
7 cress 13149 . . . . 5  classs
85, 6, 7co 5858 . . . 4  class  (flds  ZZ )
9 vs . . . . 5  set  s
104cv 1622 . . . . . 6  class  z
112cv 1622 . . . . . . . . 9  class  n
1211csn 3640 . . . . . . . 8  class  { n }
13 crsp 15924 . . . . . . . . 9  class RSpan
1410, 13cfv 5255 . . . . . . . 8  class  (RSpan `  z )
1512, 14cfv 5255 . . . . . . 7  class  ( (RSpan `  z ) `  {
n } )
16 cqg 14617 . . . . . . 7  class ~QG
1710, 15, 16co 5858 . . . . . 6  class  ( z ~QG  ( (RSpan `  z ) `  { n } ) )
18 cqus 13408 . . . . . 6  class  /.s
1910, 17, 18co 5858 . . . . 5  class  ( z 
/.s  ( z ~QG  ( (RSpan `  z
) `  { n } ) ) )
209cv 1622 . . . . . 6  class  s
21 cnx 13145 . . . . . . . 8  class  ndx
22 cple 13215 . . . . . . . 8  class  le
2321, 22cfv 5255 . . . . . . 7  class  ( le
`  ndx )
24 vf . . . . . . . 8  set  f
25 czrh 16451 . . . . . . . . . 10  class  ZRHom
2620, 25cfv 5255 . . . . . . . . 9  class  ( ZRHom `  s )
27 cc0 8737 . . . . . . . . . . 11  class  0
2811, 27wceq 1623 . . . . . . . . . 10  wff  n  =  0
29 cfzo 10870 . . . . . . . . . . 11  class ..^
3027, 11, 29co 5858 . . . . . . . . . 10  class  ( 0..^ n )
3128, 6, 30cif 3565 . . . . . . . . 9  class  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) )
3226, 31cres 4691 . . . . . . . 8  class  ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ , 
( 0..^ n ) ) )
3324cv 1622 . . . . . . . . . 10  class  f
34 cle 8868 . . . . . . . . . 10  class  <_
3533, 34ccom 4693 . . . . . . . . 9  class  ( f  o.  <_  )
3633ccnv 4688 . . . . . . . . 9  class  `' f
3735, 36ccom 4693 . . . . . . . 8  class  ( ( f  o.  <_  )  o.  `' f )
3824, 32, 37csb 3081 . . . . . . 7  class  [_ (
( ZRHom `  s
)  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  / 
f ]_ ( ( f  o.  <_  )  o.  `' f )
3923, 38cop 3643 . . . . . 6  class  <. ( le `  ndx ) , 
[_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  /  f ]_ (
( f  o.  <_  )  o.  `' f )
>.
40 csts 13146 . . . . . 6  class sSet
4120, 39, 40co 5858 . . . . 5  class  ( s sSet  <. ( le `  ndx ) ,  [_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ , 
( 0..^ n ) ) )  /  f ]_ ( ( f  o. 
<_  )  o.  `' f ) >. )
429, 19, 41csb 3081 . . . 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 3081 . . 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 4077 . 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 1623 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  16489
  Copyright terms: Public domain W3C validator