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