This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ℤ/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 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ ) )