Metamath Proof Explorer

Theorem znval

Description: The value of the Z/nZ structure. It is defined as the quotient ring ZZ / n ZZ , with an "artificial" ordering added to make it a Toset . (In other words, Z/nZ is aring with anorder , but it is not anordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 2-May-2016) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znval.s ⊢ 𝑆 = ( RSpan ‘ ℤring )
znval.u ⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
znval.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znval.f ⊢ 𝐹 = ( ( ℤRHom ‘ 𝑈 ) ↾ 𝑊 )
znval.w ⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
znval.l ⊢ ≤ = ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 )
Assertion znval ( 𝑁 ∈ ℕ0 → 𝑌 = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )

Proof

Step Hyp Ref Expression
1 znval.s ⊢ 𝑆 = ( RSpan ‘ ℤring )
2 znval.u ⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
3 znval.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4 znval.f ⊢ 𝐹 = ( ( ℤRHom ‘ 𝑈 ) ↾ 𝑊 )
5 znval.w ⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
6 znval.l ⊢ ≤ = ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 )
7 zringring ⊢ ℤring ∈ Ring
8 7 a1i ⊢ ( 𝑛 = 𝑁 → ℤring ∈ Ring )
9 ovexd ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ∈ V )
10 id ⊢ ( 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) → 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) )
11 simpr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → 𝑧 = ℤring )
12 11 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → ( RSpan ‘ 𝑧 ) = ( RSpan ‘ ℤring ) )
13 12 1 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → ( RSpan ‘ 𝑧 ) = 𝑆 )
14 simpl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → 𝑛 = 𝑁 )
15 14 sneqd ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → { 𝑛 } = { 𝑁 } )
16 13 15 fveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) = ( 𝑆 ‘ { 𝑁 } ) )
17 11 16 oveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) = ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
18 11 17 oveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) ) )
19 18 2 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) = 𝑈 )
20 10 19 sylan9eqr ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → 𝑠 = 𝑈 )
21 fvex ⊢ ( ℤRHom ‘ 𝑠 ) ∈ V
22 21 resex ⊢ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) ∈ V
23 22 a1i ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) ∈ V )
24 id ⊢ ( 𝑓 = ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) → 𝑓 = ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) )
25 20 fveq2d ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → ( ℤRHom ‘ 𝑠 ) = ( ℤRHom ‘ 𝑈 ) )
26 simpll ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → 𝑛 = 𝑁 )
27 26 eqeq1d ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → ( 𝑛 = 0 ↔ 𝑁 = 0 ) )
28 26 oveq2d ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → ( 0 ..^ 𝑛 ) = ( 0 ..^ 𝑁 ) )
29 27 28 ifbieq2d ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) )
30 29 5 eqtr4di ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) = 𝑊 )
31 25 30 reseq12d ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) = ( ( ℤRHom ‘ 𝑈 ) ↾ 𝑊 ) )
32 31 4 eqtr4di ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) = 𝐹 )
33 24 32 sylan9eqr ⊢ ( ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) ∧ 𝑓 = ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) ) → 𝑓 = 𝐹 )
34 33 coeq1d ⊢ ( ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) ∧ 𝑓 = ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) ) → ( 𝑓 ∘ ≤ ) = ( 𝐹 ∘ ≤ ) )
35 33 cnveqd ⊢ ( ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) ∧ 𝑓 = ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) ) → ◡ 𝑓 = ◡ 𝐹 )
36 34 35 coeq12d ⊢ ( ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) ∧ 𝑓 = ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) ) → ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) = ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) )
37 36 6 eqtr4di ⊢ ( ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) ∧ 𝑓 = ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) ) → ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) = ≤ )
38 23 37 csbied ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) = ≤ )
39 38 opeq2d ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ = ⟨ ( le ‘ ndx ) , ≤ ⟩ )
40 20 39 oveq12d ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) ∧ 𝑠 = ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) ) → ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ ) = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )
41 9 40 csbied ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑧 = ℤring ) → ⦋ ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) / 𝑠 ⦌ ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ ) = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )
42 8 41 csbied ⊢ ( 𝑛 = 𝑁 → ⦋ ℤring / 𝑧 ⦌ ⦋ ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) / 𝑠 ⦌ ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ ) = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )
43 df-zn ⊢ ℤ/nℤ = ( 𝑛 ∈ ℕ0 ↦ ⦋ ℤring / 𝑧 ⦌ ⦋ ( 𝑧 /s ( 𝑧 ~QG ( ( RSpan ‘ 𝑧 ) ‘ { 𝑛 } ) ) ) / 𝑠 ⦌ ( 𝑠 sSet ⟨ ( le ‘ ndx ) , ⦋ ( ( ℤRHom ‘ 𝑠 ) ↾ if ( 𝑛 = 0 , ℤ , ( 0 ..^ 𝑛 ) ) ) / 𝑓 ⦌ ( ( 𝑓 ∘ ≤ ) ∘ ◡ 𝑓 ) ⟩ ) )
44 ovex ⊢ ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) ∈ V
45 42 43 44 fvmpt ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑁 ) = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )
46 3 45 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 = ( 𝑈 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )