Definition df-zn 19855

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

Step	Hyp	Ref	Expression
1		czn 19851	. 2 class ℤ/nℤ
2		vn	. . 3 setvar n
3		cn0 11292	. . 3 class NN0
4		vz	. . . 4 setvar z
5		zring 19818	. . . 4 class ℤring
6		vs	. . . . 5 setvar s
7	4	cv 1482	. . . . . 6 class z
8	2	cv 1482	. . . . . . . . 9 class n
9	8	csn 4177	. . . . . . . 8 class { n }
10		crsp 19171	. . . . . . . . 9 class RSpan
11	7, 10	cfv 5888	. . . . . . . 8 class (RSpan ` z )
12	9, 11	cfv 5888	. . . . . . 7 class ( (RSpan ` z ) ` { n } )
13		cqg 17590	. . . . . . 7 class ~QG
14	7, 12, 13	co 6650	. . . . . 6 class ( z ~QG ( (RSpan ` z ) ` { n } ) )
15		cqus 16165	. . . . . 6 class /.s
16	7, 14, 15	co 6650	. . . . 5 class ( z /.s ( z ~QG ( (RSpan ` z ) ` { n } ) ) )
17	6	cv 1482	. . . . . 6 class s
18		cnx 15854	. . . . . . . 8 class ndx
19		cple 15948	. . . . . . . 8 class le
20	18, 19	cfv 5888	. . . . . . 7 class ( le ` ndx )
21		vf	. . . . . . . 8 setvar f
22		czrh 19848	. . . . . . . . . 10 class ZRHom
23	17, 22	cfv 5888	. . . . . . . . 9 class ( ZRHom ` s )
24		cc0 9936	. . . . . . . . . . 11 class 0
25	8, 24	wceq 1483	. . . . . . . . . 10 wff n = 0
26		cz 11377	. . . . . . . . . 10 class ZZ
27		cfzo 12465	. . . . . . . . . . 11 class ..^
28	24, 8, 27	co 6650	. . . . . . . . . 10 class ( 0..^ n )
29	25, 26, 28	cif 4086	. . . . . . . . 9 class if ( n = 0 , ZZ , ( 0..^ n ) )
30	23, 29	cres 5116	. . . . . . . 8 class ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) )
31	21	cv 1482	. . . . . . . . . 10 class f
32		cle 10075	. . . . . . . . . 10 class <_
33	31, 32	ccom 5118	. . . . . . . . 9 class ( f o. <_ )
34	31	ccnv 5113	. . . . . . . . 9 class `' f
35	33, 34	ccom 5118	. . . . . . . 8 class ( ( f o. <_ ) o. `' f )
36	21, 30, 35	csb 3533	. . . . . . 7 class [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f )
37	20, 36	cop 4183	. . . . . 6 class <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >.
38		csts 15855	. . . . . 6 class sSet
39	17, 37, 38	co 6650	. . . . 5 class ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. )
40	6, 16, 39	csb 3533	. . . 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 ) >. )
41	4, 5, 40	csb 3533	. . 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 ) >. )
42	2, 3, 41	cmpt 4729	. 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 ) >. ) )
43	1, 42	wceq 1483	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 ) >. ) )

This definition is referenced by:  znval  19883