ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-zn Unicode version

Definition df-zn 13931
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 13928 . 2  class ℤ/n
2 vn . . 3  setvar  n
3 cn0 9207 . . 3  class  NN0
4 vz . . . 4  setvar  z
5 czring 13906 . . . 4  classring
6 vs . . . . 5  setvar  s
74cv 1363 . . . . . 6  class  z
82cv 1363 . . . . . . . . 9  class  n
98csn 3607 . . . . . . . 8  class  { n }
10 crsp 13801 . . . . . . . . 9  class RSpan
117, 10cfv 5235 . . . . . . . 8  class  (RSpan `  z )
129, 11cfv 5235 . . . . . . 7  class  ( (RSpan `  z ) `  {
n } )
13 cqg 13125 . . . . . . 7  class ~QG
147, 12, 13co 5897 . . . . . 6  class  ( z ~QG  ( (RSpan `  z ) `  { n } ) )
15 cqus 12780 . . . . . 6  class  /.s
167, 14, 15co 5897 . . . . 5  class  ( z 
/.s  ( z ~QG  ( (RSpan `  z
) `  { n } ) ) )
176cv 1363 . . . . . 6  class  s
18 cnx 12512 . . . . . . . 8  class  ndx
19 cple 12599 . . . . . . . 8  class  le
2018, 19cfv 5235 . . . . . . 7  class  ( le
`  ndx )
21 vf . . . . . . . 8  setvar  f
22 czrh 13926 . . . . . . . . . 10  class  ZRHom
2317, 22cfv 5235 . . . . . . . . 9  class  ( ZRHom `  s )
24 cc0 7842 . . . . . . . . . . 11  class  0
258, 24wceq 1364 . . . . . . . . . 10  wff  n  =  0
26 cz 9284 . . . . . . . . . 10  class  ZZ
27 cfzo 10174 . . . . . . . . . . 11  class ..^
2824, 8, 27co 5897 . . . . . . . . . 10  class  ( 0..^ n )
2925, 26, 28cif 3549 . . . . . . . . 9  class  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) )
3023, 29cres 4646 . . . . . . . 8  class  ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ , 
( 0..^ n ) ) )
3121cv 1363 . . . . . . . . . 10  class  f
32 cle 8024 . . . . . . . . . 10  class  <_
3331, 32ccom 4648 . . . . . . . . 9  class  ( f  o.  <_  )
3431ccnv 4643 . . . . . . . . 9  class  `' f
3533, 34ccom 4648 . . . . . . . 8  class  ( ( f  o.  <_  )  o.  `' f )
3621, 30, 35csb 3072 . . . . . . 7  class  [_ (
( ZRHom `  s
)  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  / 
f ]_ ( ( f  o.  <_  )  o.  `' f )
3720, 36cop 3610 . . . . . 6  class  <. ( le `  ndx ) , 
[_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ ,  ( 0..^ n ) ) )  /  f ]_ (
( f  o.  <_  )  o.  `' f )
>.
38 csts 12513 . . . . . 6  class sSet
3917, 37, 38co 5897 . . . . 5  class  ( s sSet  <. ( le `  ndx ) ,  [_ ( ( ZRHom `  s )  |`  if ( n  =  0 ,  ZZ , 
( 0..^ n ) ) )  /  f ]_ ( ( f  o. 
<_  )  o.  `' f ) >. )
406, 16, 39csb 3072 . . . 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 3072 . . 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 4079 . 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 1364 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 set class
This definition is referenced by:  znval  13949
  Copyright terms: Public domain W3C validator