Metamath Proof Explorer

Theorem znle

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 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
znle.l ⊢ ≤ ˙ = ≤ Y
Assertion znle ⊢ N ∈ ℕ 0 → ≤ ˙ = F ∘ ≤ ∘ F -1

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 znle.l ⊢ ≤ ˙ = ≤ Y
7 eqid ⊢ F ∘ ≤ ∘ F -1 = F ∘ ≤ ∘ F -1
8 1 2 3 4 5 7 znval ⊢ N ∈ ℕ 0 → Y = U sSet ≤ ndx F ∘ ≤ ∘ F -1
9 8 fveq2d ⊢ N ∈ ℕ 0 → ≤ Y = ≤ U sSet ≤ ndx F ∘ ≤ ∘ F -1
10 2 ovexi ⊢ U ∈ V
11 fvex ⊢ ℤRHom ⁡ U ∈ V
12 11 resex ⊢ ℤRHom ⁡ U ↾ W ∈ V
13 4 12 eqeltri ⊢ F ∈ V
14 xrex ⊢ ℝ * ∈ V
15 14 14 xpex ⊢ ℝ * × ℝ * ∈ V
16 lerelxr ⊢ ≤ ⊆ ℝ * × ℝ *
17 15 16 ssexi ⊢ ≤ ∈ V
18 13 17 coex ⊢ F ∘ ≤ ∈ V
19 13 cnvex ⊢ F -1 ∈ V
20 18 19 coex ⊢ F ∘ ≤ ∘ F -1 ∈ V
21 pleid ⊢ le = Slot ≤ ndx
22 21 setsid ⊢ U ∈ V ∧ F ∘ ≤ ∘ F -1 ∈ V → F ∘ ≤ ∘ F -1 = ≤ U sSet ≤ ndx F ∘ ≤ ∘ F -1
23 10 20 22 mp2an ⊢ F ∘ ≤ ∘ F -1 = ≤ U sSet ≤ ndx F ∘ ≤ ∘ F -1
24 9 6 23 3eqtr4g ⊢ N ∈ ℕ 0 → ≤ ˙ = F ∘ ≤ ∘ F -1