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	⊢ ℤ/nℤ = ( 𝑛 ∈ ℕ0 ↦ ⦋ ℤring / 𝑧 ⦌ ⦋ ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) / 𝑠 ⦌ ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czn	⊢ ℤ/nℤ
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		czring	⊢ ℤring
4		vz	⊢ 𝑧
5	4	cv	⊢ 𝑧
6		cqus	⊢ /s
7		cqg	⊢ ~QG
8		crsp	⊢ RSpan
9	5 8	cfv	⊢ ( RSpan ‘ 𝑧 )
10	1	cv	⊢ 𝑛
11	10	csn	⊢ { 𝑛 }
12	11 9	cfv	⊢ ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } )
13	5 12 7	co	⊢ ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) )
14	5 13 6	co	⊢ ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) )
15		vs	⊢ 𝑠
16	15	cv	⊢ 𝑠
17		csts	⊢ sSet
18		cple	⊢ le
19		cnx	⊢ ndx
20	19 18	cfv	⊢ ( le ‘ ndx )
21		czrh	⊢ ℤRHom
22	16 21	cfv	⊢ ( ℤRHom ‘ 𝑠 )
23		cc0	⊢ 0
24	10 23	wceq	⊢ 𝑛 = 0
25		cz	⊢ ℤ
26		cfzo	⊢ ..^
27	23 10 26	co	⊢ ( 0 ..^ 𝑛 )
28	24 25 27	cif	⊢ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) )
29	22 28	cres	⊢ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) )
30		vf	⊢ 𝑓
31	30	cv	⊢ 𝑓
32		cle	⊢ ≤
33	31 32	ccom	⊢ ( 𝑓 ∘ ≤ )
34	31	ccnv	⊢ ◡ 𝑓
35	33 34	ccom	⊢ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 )
36	30 29 35	csb	⊢ ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 )
37	20 36	cop	⊢ ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩
38	16 37 17	co	⊢ ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ )
39	15 14 38	csb	⊢ ⦋ ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) / 𝑠 ⦌ ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ )
40	4 3 39	csb	⊢ ⦋ ℤring / 𝑧 ⦌ ⦋ ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) / 𝑠 ⦌ ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ )
41	1 2 40	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ ⦋ ℤring / 𝑧 ⦌ ⦋ ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) / 𝑠 ⦌ ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ ) )
42	0 41	wceq	⊢ ℤ/nℤ = ( 𝑛 ∈ ℕ0 ↦ ⦋ ℤring / 𝑧 ⦌ ⦋ ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) / 𝑠 ⦌ ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ ) )