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=ifN=0ℤ0..^N
znle2.l ⊢≤˙=≤Y
znleval.x ⊢X=BaseY
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=ifN=0ℤ0..^N
4 znle2.l ⊢≤˙=≤Y
5 znleval.x ⊢X=BaseY
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