Metamath Proof Explorer


Theorem znleval2

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
znleval.x X = Base Y
Assertion znleval2 N 0 A X B X A ˙ B F -1 A F -1 B

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 znleval.x X = Base Y
6 1 2 3 4 5 znleval N 0 A ˙ B A X B X F -1 A F -1 B
7 6 3ad2ant1 N 0 A X B X A ˙ B A X B X F -1 A F -1 B
8 3simpc N 0 A X B X A X B X
9 8 biantrurd N 0 A X B X F -1 A F -1 B A X B X F -1 A F -1 B
10 df-3an A X B X F -1 A F -1 B A X B X F -1 A F -1 B
11 9 10 bitr4di N 0 A X B X F -1 A F -1 B A X B X F -1 A F -1 B
12 7 11 bitr4d N 0 A X B X A ˙ B F -1 A F -1 B