This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znle2.f ⊢ 𝐹 = ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 )
znle2.w ⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
znle2.l ⊢ ≤ = ( le ‘ 𝑌 )
znleval.x ⊢ 𝑋 = ( Base ‘ 𝑌 )
Assertion znleval2 ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ≤ 𝐵 ↔ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 znle2.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 znle2.f ⊢ 𝐹 = ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 )
3 znle2.w ⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
4 znle2.l ⊢ ≤ = ( le ‘ 𝑌 )
5 znleval.x ⊢ 𝑋 = ( Base ‘ 𝑌 )
6 1 2 3 4 5 znleval ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) ) )
7 6 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) ) )
8 3simpc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
9 8 biantrurd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) ) )
10 df-3an ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) )
11 9 10 bitr4di ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) ) )
12 7 11 bitr4d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ≤ 𝐵 ↔ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) )