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𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐵 ↔ ( 𝐹𝐴 ) ≤ ( 𝐹𝐵 ) ) )