Definition df-zn 14629

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 14626	. 2 class ℤ/nℤ
2		vn	. . 3 setvar n
3		cn0 9401	. . 3 class NN0
4		vz	. . . 4 setvar z
5		czring 14603	. . . 4 class ℤring
6		vs	. . . . 5 setvar s
7	4	cv 1396	. . . . . 6 class z
8	2	cv 1396	. . . . . . . . 9 class n
9	8	csn 3669	. . . . . . . 8 class { n }
10		crsp 14481	. . . . . . . . 9 class RSpan
11	7, 10	cfv 5326	. . . . . . . 8 class (RSpan ` z )
12	9, 11	cfv 5326	. . . . . . 7 class ( (RSpan ` z ) ` { n } )
13		cqg 13755	. . . . . . 7 class ~QG
14	7, 12, 13	co 6017	. . . . . 6 class ( z ~QG ( (RSpan ` z ) ` { n } ) )
15		cqus 13382	. . . . . 6 class /.s
16	7, 14, 15	co 6017	. . . . 5 class ( z /.s ( z ~QG ( (RSpan ` z ) ` { n } ) ) )
17	6	cv 1396	. . . . . 6 class s
18		cnx 13078	. . . . . . . 8 class ndx
19		cple 13166	. . . . . . . 8 class le
20	18, 19	cfv 5326	. . . . . . 7 class ( le ` ndx )
21		vf	. . . . . . . 8 setvar f
22		czrh 14624	. . . . . . . . . 10 class ZRHom
23	17, 22	cfv 5326	. . . . . . . . 9 class ( ZRHom ` s )
24		cc0 8031	. . . . . . . . . . 11 class 0
25	8, 24	wceq 1397	. . . . . . . . . 10 wff n = 0
26		cz 9478	. . . . . . . . . 10 class ZZ
27		cfzo 10376	. . . . . . . . . . 11 class ..^
28	24, 8, 27	co 6017	. . . . . . . . . 10 class ( 0..^ n )
29	25, 26, 28	cif 3605	. . . . . . . . 9 class if ( n = 0 , ZZ , ( 0..^ n ) )
30	23, 29	cres 4727	. . . . . . . 8 class ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) )
31	21	cv 1396	. . . . . . . . . 10 class f
32		cle 8214	. . . . . . . . . 10 class <_
33	31, 32	ccom 4729	. . . . . . . . 9 class ( f o. <_ )
34	31	ccnv 4724	. . . . . . . . 9 class `' f
35	33, 34	ccom 4729	. . . . . . . 8 class ( ( f o. <_ ) o. `' f )
36	21, 30, 35	csb 3127	. . . . . . 7 class [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f )
37	20, 36	cop 3672	. . . . . 6 class <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >.
38		csts 13079	. . . . . 6 class sSet
39	17, 37, 38	co 6017	. . . . 5 class ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. )
40	6, 16, 39	csb 3127	. . . 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 3127	. . 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 4150	. 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 1397	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  14649