Metamath Proof Explorer

Definition df-zn

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)

Ref Expression
Assertion df-zn 
|- Z/nZ = ( n e. NN0 |-> [_ ZZring / 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 ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 czn 
 |-  Z/nZ
1 vn 
 |-  n
2 cn0 
 |-  NN0
3 czring 
 |-  ZZring
4 vz 
 |-  z
5 4 cv 
 |-  z
6 cqus 
 |-  /s
7 cqg 
 |-  ~QG
8 crsp 
 |-  RSpan
9 5 8 cfv 
 |-  ( RSpan ` z )
10 1 cv 
 |-  n
11 10 csn 
 |-  { n }
12 11 9 cfv 
 |-  ( ( RSpan ` z ) ` { n } )
13 5 12 7 co 
 |-  ( z ~QG ( ( RSpan ` z ) ` { n } ) )
14 5 13 6 co 
 |-  ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) )
15 vs 
 |-  s
16 15 cv 
 |-  s
17 csts 
 |-  sSet
18 cple 
 |-  le
19 cnx 
 |-  ndx
20 19 18 cfv 
 |-  ( le ` ndx )
21 czrh 
 |-  ZRHom
22 16 21 cfv 
 |-  ( ZRHom ` s )
23 cc0 
 |-  0
24 10 23 wceq 
 |-  n = 0
25 cz 
 |-  ZZ
26 cfzo 
 |-  ..^
27 23 10 26 co 
 |-  ( 0 ..^ n )
28 24 25 27 cif 
 |-  if ( n = 0 , ZZ , ( 0 ..^ n ) )
29 22 28 cres 
 |-  ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) )
30 vf 
 |-  f
31 30 cv 
 |-  f
32 cle 
 |-  <_
33 31 32 ccom 
 |-  ( f o. <_ )
34 31 ccnv 
 |-  `' f
35 33 34 ccom 
 |-  ( ( f o. <_ ) o. `' f )
36 30 29 35 csb 
 |-  [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f )
37 20 36 cop 
 |-  <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >.
38 16 37 17 co 
 |-  ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. )
39 15 14 38 csb 
 |-  [_ ( 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 ) >. )
40 4 3 39 csb 
 |-  [_ ZZring / 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 ) >. )
41 1 2 40 cmpt 
 |-  ( n e. NN0 |-> [_ ZZring / 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 ) >. ) )
42 0 41 wceq 
 |-  Z/nZ = ( n e. NN0 |-> [_ ZZring / 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 ) >. ) )