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

Definition df-zn 17941
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.) (Revised by AV, 12-Jun-2019.)
Assertion
Ref Expression
df-zn  |- ℤ/n =  ( n  e. 
NN0  |->  [_ring  /  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 17937 . 2  class ℤ/n
2 vn . . 3  setvar  n
3 cn0 10582 . . 3  class  NN0
4 vz . . . 4  setvar  z
5 zring 17886 . . . 4  classring
6 vs . . . . 5  setvar  s
74cv 1368 . . . . . 6  class  z
82cv 1368 . . . . . . . . 9  class  n
98csn 3880 . . . . . . . 8  class  { n }
10 crsp 17255 . . . . . . . . 9  class RSpan
117, 10cfv 5421 . . . . . . . 8  class  (RSpan `  z )
129, 11cfv 5421 . . . . . . 7  class  ( (RSpan `  z ) `  {
n } )
13 cqg 15680 . . . . . . 7  class ~QG
147, 12, 13co 6094 . . . . . 6  class  ( z ~QG  ( (RSpan `  z ) `  { n } ) )
15 cqus 14446 . . . . . 6  class  /.s
167, 14, 15co 6094 . . . . 5  class  ( z 
/.s  ( z ~QG  ( (RSpan `  z
) `  { n } ) ) )
176cv 1368 . . . . . 6  class  s
18 cnx 14174 . . . . . . . 8  class  ndx
19 cple 14248 . . . . . . . 8  class  le
2018, 19cfv 5421 . . . . . . 7  class  ( le
`  ndx )
21 vf . . . . . . . 8  setvar  f
22 czrh 17934 . . . . . . . . . 10  class  ZRHom
2317, 22cfv 5421 . . . . . . . . 9  class  ( ZRHom `  s )
24 cc0 9285 . . . . . . . . . . 11  class  0
258, 24wceq 1369 . . . . . . . . . 10  wff  n  =  0
26 cz 10649 . . . . . . . . . 10  class  ZZ
27 cfzo 11551 . . . . . . . . . . 11  class ..^
2824, 8, 27co 6094 . . . . . . . . . 10  class  ( 0..^ n )
2925, 26, 28cif 3794 . . . . . . . . 9  class  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) )
3023, 29cres 4845 . . . . . . . 8  class  ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ , 
( 0..^ n ) ) )
3121cv 1368 . . . . . . . . . 10  class  f
32 cle 9422 . . . . . . . . . 10  class  <_
3331, 32ccom 4847 . . . . . . . . 9  class  ( f  o.  <_  )
3431ccnv 4842 . . . . . . . . 9  class  `' f
3533, 34ccom 4847 . . . . . . . 8  class  ( ( f  o.  <_  )  o.  `' f )
3621, 30, 35csb 3291 . . . . . . 7  class  [_ (
( ZRHom `  s
)  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  / 
f ]_ ( ( f  o.  <_  )  o.  `' f )
3720, 36cop 3886 . . . . . 6  class  <. ( le `  ndx ) , 
[_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  /  f ]_ (
( f  o.  <_  )  o.  `' f )
>.
38 csts 14175 . . . . . 6  class sSet
3917, 37, 38co 6094 . . . . 5  class  ( s sSet  <. ( le `  ndx ) ,  [_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ , 
( 0..^ n ) ) )  /  f ]_ ( ( f  o. 
<_  )  o.  `' f ) >. )
406, 16, 39csb 3291 . . . 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 ) >.
)
414, 5, 40csb 3291 . . 3  class  [_ring  /  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 ) >.
)
422, 3, 41cmpt 4353 . 2  class  ( n  e.  NN0  |->  [_ring  /  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 ) >.
) )
431, 42wceq 1369 1  wff ℤ/n =  ( n  e. 
NN0  |->  [_ring  /  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 setvar class
This definition is referenced by:  znval  17969
  Copyright terms: Public domain W3C validator