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 ⊢ S = RSpan ⁡ ℤ ring
znval.u ⊢ U = ℤ ring / 𝑠 ℤ ring ~ QG S ⁡ N
znval.y ⊢ Y = ℤ/Nℤ
znval.f ⊢ F = ℤRHom ⁡ U ↾ W
znval.w ⊢ W = if N = 0 ℤ 0 ..^ N
znval.l ⊢ ≤ ˙ = F ∘ ≤ ∘ F -1
Assertion znval ⊢ N ∈ ℕ 0 → Y = U sSet ≤ ndx ≤ ˙

Proof

Step Hyp Ref Expression
1 znval.s ⊢ S = RSpan ⁡ ℤ ring
2 znval.u ⊢ U = ℤ ring / 𝑠 ℤ ring ~ QG S ⁡ N
3 znval.y ⊢ Y = ℤ/Nℤ
4 znval.f ⊢ F = ℤRHom ⁡ U ↾ W
5 znval.w ⊢ W = if N = 0 ℤ 0 ..^ N
6 znval.l ⊢ ≤ ˙ = F ∘ ≤ ∘ F -1
7 zringring ⊢ ℤ ring ∈ Ring
8 7 a1i ⊢ n = N → ℤ ring ∈ Ring
9 ovexd ⊢ n = N ∧ z = ℤ ring → z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n ∈ V
10 id ⊢ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n
11 simpr ⊢ n = N ∧ z = ℤ ring → z = ℤ ring
12 11 fveq2d ⊢ n = N ∧ z = ℤ ring → RSpan ⁡ z = RSpan ⁡ ℤ ring
13 12 1 eqtr4di ⊢ n = N ∧ z = ℤ ring → RSpan ⁡ z = S
14 simpl ⊢ n = N ∧ z = ℤ ring → n = N
15 14 sneqd ⊢ n = N ∧ z = ℤ ring → n = N
16 13 15 fveq12d ⊢ n = N ∧ z = ℤ ring → RSpan ⁡ z ⁡ n = S ⁡ N
17 11 16 oveq12d ⊢ n = N ∧ z = ℤ ring → z ~ QG RSpan ⁡ z ⁡ n = ℤ ring ~ QG S ⁡ N
18 11 17 oveq12d ⊢ n = N ∧ z = ℤ ring → z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n = ℤ ring / 𝑠 ℤ ring ~ QG S ⁡ N
19 18 2 eqtr4di ⊢ n = N ∧ z = ℤ ring → z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n = U
20 10 19 sylan9eqr ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → s = U
21 fvex ⊢ ℤRHom ⁡ s ∈ V
22 21 resex ⊢ ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n ∈ V
23 22 a1i ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n ∈ V
24 id ⊢ f = ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n → f = ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n
25 20 fveq2d ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → ℤRHom ⁡ s = ℤRHom ⁡ U
26 simpll ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → n = N
27 26 eqeq1d ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → n = 0 ↔ N = 0
28 26 oveq2d ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → 0 ..^ n = 0 ..^ N
29 27 28 ifbieq2d ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → if n = 0 ℤ 0 ..^ n = if N = 0 ℤ 0 ..^ N
30 29 5 eqtr4di ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → if n = 0 ℤ 0 ..^ n = W
31 25 30 reseq12d ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n = ℤRHom ⁡ U ↾ W
32 31 4 eqtr4di ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n = F
33 24 32 sylan9eqr ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n ∧ f = ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n → f = F
34 33 coeq1d ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n ∧ f = ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n → f ∘ ≤ = F ∘ ≤
35 33 cnveqd ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n ∧ f = ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n → f -1 = F -1
36 34 35 coeq12d ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n ∧ f = ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n → f ∘ ≤ ∘ f -1 = F ∘ ≤ ∘ F -1
37 36 6 eqtr4di ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n ∧ f = ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n → f ∘ ≤ ∘ f -1 = ≤ ˙
38 23 37 csbied ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → ⦋ ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n / f⦌ f ∘ ≤ ∘ f -1 = ≤ ˙
39 38 opeq2d ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → ≤ ndx ⦋ ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n / f⦌ f ∘ ≤ ∘ f -1 = ≤ ndx ≤ ˙
40 20 39 oveq12d ⊢ n = N ∧ z = ℤ ring ∧ s = z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n → s sSet ≤ ndx ⦋ ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n / f⦌ f ∘ ≤ ∘ f -1 = U sSet ≤ ndx ≤ ˙
41 9 40 csbied ⊢ n = N ∧ z = ℤ ring → ⦋ z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n / s⦌ s sSet ≤ ndx ⦋ ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n / f⦌ f ∘ ≤ ∘ f -1 = U sSet ≤ ndx ≤ ˙
42 8 41 csbied ⊢ n = N → ⦋ ℤ ring / z⦌ ⦋ z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n / s⦌ s sSet ≤ ndx ⦋ ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n / f⦌ f ∘ ≤ ∘ f -1 = U sSet ≤ ndx ≤ ˙
43 df-zn ⊢ ℤ/nℤ = n ∈ ℕ 0 ⟼ ⦋ ℤ ring / z⦌ ⦋ z / 𝑠 z ~ QG RSpan ⁡ z ⁡ n / s⦌ s sSet ≤ ndx ⦋ ℤRHom ⁡ s ↾ if n = 0 ℤ 0 ..^ n / f⦌ f ∘ ≤ ∘ f -1
44 ovex ⊢ U sSet ≤ ndx ≤ ˙ ∈ V
45 42 43 44 fvmpt ⊢ N ∈ ℕ 0 → ℤ/Nℤ = U sSet ≤ ndx ≤ ˙
46 3 45 eqtrid ⊢ N ∈ ℕ 0 → Y = U sSet ≤ ndx ≤ ˙