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