Metamath Proof Explorer


Theorem znle2

Description: The ordering of the Z/nZ structure. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znle2.y Y = /N
znle2.f F = ℤRHom Y W
znle2.w W = if N = 0 0 ..^ N
znle2.l ˙ = Y
Assertion znle2 N 0 ˙ = F F -1

Proof

Step Hyp Ref Expression
1 znle2.y Y = /N
2 znle2.f F = ℤRHom Y W
3 znle2.w W = if N = 0 0 ..^ N
4 znle2.l ˙ = Y
5 eqid RSpan ring = RSpan ring
6 eqid ring / 𝑠 ring ~ QG RSpan ring N = ring / 𝑠 ring ~ QG RSpan ring N
7 eqid ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W = ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W
8 5 6 1 7 3 4 znle N 0 ˙ = ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W -1
9 5 6 1 znzrh N 0 ℤRHom ring / 𝑠 ring ~ QG RSpan ring N = ℤRHom Y
10 9 reseq1d N 0 ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W = ℤRHom Y W
11 10 2 eqtr4di N 0 ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W = F
12 11 coeq1d N 0 ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W = F
13 11 cnveqd N 0 ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W -1 = F -1
14 12 13 coeq12d N 0 ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W ℤRHom ring / 𝑠 ring ~ QG RSpan ring N W -1 = F F -1
15 8 14 eqtrd N 0 ˙ = F F -1