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 syl6bbr ⊢ 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