Metamath Proof Explorer

Theorem znleval

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 znleval ( 𝑁 ∈ ℕ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 znle2 ⊢ ( 𝑁 ∈ ℕ0 → ≤ = ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) )
7 relco ⊢ Rel ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 )
8 relssdmrn ⊢ ( Rel ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) → ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ⊆ ( dom ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) × ran ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ) )
9 7 8 ax-mp ⊢ ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ⊆ ( dom ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) × ran ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) )
10 dmcoss ⊢ dom ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ⊆ dom ◡ 𝐹
11 df-rn ⊢ ran 𝐹 = dom ◡ 𝐹
12 1 5 2 3 znf1o ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝑊 –1-1-onto→ 𝑋 )
13 f1ofo ⊢ ( 𝐹 : 𝑊 –1-1-onto→ 𝑋 → 𝐹 : 𝑊 –onto→ 𝑋 )
14 forn ⊢ ( 𝐹 : 𝑊 –onto→ 𝑋 → ran 𝐹 = 𝑋 )
15 12 13 14 3syl ⊢ ( 𝑁 ∈ ℕ0 → ran 𝐹 = 𝑋 )
16 11 15 eqtr3id ⊢ ( 𝑁 ∈ ℕ0 → dom ◡ 𝐹 = 𝑋 )
17 10 16 sseqtrid ⊢ ( 𝑁 ∈ ℕ0 → dom ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ⊆ 𝑋 )
18 rncoss ⊢ ran ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ⊆ ran ( 𝐹 ∘ ≤ )
19 rncoss ⊢ ran ( 𝐹 ∘ ≤ ) ⊆ ran 𝐹
20 19 15 sseqtrid ⊢ ( 𝑁 ∈ ℕ0 → ran ( 𝐹 ∘ ≤ ) ⊆ 𝑋 )
21 18 20 sstrid ⊢ ( 𝑁 ∈ ℕ0 → ran ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ⊆ 𝑋 )
22 xpss12 ⊢ ( ( dom ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ⊆ 𝑋 ∧ ran ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ⊆ 𝑋 ) → ( dom ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) × ran ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ) ⊆ ( 𝑋 × 𝑋 ) )
23 17 21 22 syl2anc ⊢ ( 𝑁 ∈ ℕ0 → ( dom ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) × ran ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ) ⊆ ( 𝑋 × 𝑋 ) )
24 9 23 sstrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) ⊆ ( 𝑋 × 𝑋 ) )
25 6 24 eqsstrd ⊢ ( 𝑁 ∈ ℕ0 → ≤ ⊆ ( 𝑋 × 𝑋 ) )
26 25 ssbrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ≤ 𝐵 → 𝐴 ( 𝑋 × 𝑋 ) 𝐵 ) )
27 brxp ⊢ ( 𝐴 ( 𝑋 × 𝑋 ) 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
28 26 27 syl6ib ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ≤ 𝐵 → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) )
29 28 pm4.71rd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ≤ 𝐵 ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≤ 𝐵 ) ) )
30 6 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ≤ = ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) )
31 30 breqd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ≤ 𝐵 ↔ 𝐴 ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) 𝐵 ) )
32 brcog ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 ◡ 𝐹 𝑥 ∧ 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ) ) )
33 32 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 ◡ 𝐹 𝑥 ∧ 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ) ) )
34 eqcom ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝐴 ) ↔ ( ◡ 𝐹 ‘ 𝐴 ) = 𝑥 )
35 12 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐹 : 𝑊 –1-1-onto→ 𝑋 )
36 f1ocnv ⊢ ( 𝐹 : 𝑊 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑋 –1-1-onto→ 𝑊 )
37 f1ofn ⊢ ( ◡ 𝐹 : 𝑋 –1-1-onto→ 𝑊 → ◡ 𝐹 Fn 𝑋 )
38 35 36 37 3syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ◡ 𝐹 Fn 𝑋 )
39 simprl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
40 fnbrfvb ⊢ ( ( ◡ 𝐹 Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝐴 ) = 𝑥 ↔ 𝐴 ◡ 𝐹 𝑥 ) )
41 38 39 40 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝐴 ) = 𝑥 ↔ 𝐴 ◡ 𝐹 𝑥 ) )
42 34 41 syl5rbb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ◡ 𝐹 𝑥 ↔ 𝑥 = ( ◡ 𝐹 ‘ 𝐴 ) ) )
43 42 anbi1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 ◡ 𝐹 𝑥 ∧ 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ) ↔ ( 𝑥 = ( ◡ 𝐹 ‘ 𝐴 ) ∧ 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ) ) )
44 43 exbidv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∃ 𝑥 ( 𝐴 ◡ 𝐹 𝑥 ∧ 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 = ( ◡ 𝐹 ‘ 𝐴 ) ∧ 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ) ) )
45 33 44 bitrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ( ( 𝐹 ∘ ≤ ) ∘ ◡ 𝐹 ) 𝐵 ↔ ∃ 𝑥 ( 𝑥 = ( ◡ 𝐹 ‘ 𝐴 ) ∧ 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ) ) )
46 fvex ⊢ ( ◡ 𝐹 ‘ 𝐴 ) ∈ V
47 breq1 ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝐴 ) → ( 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ↔ ( ◡ 𝐹 ‘ 𝐴 ) ( 𝐹 ∘ ≤ ) 𝐵 ) )
48 46 47 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ( ◡ 𝐹 ‘ 𝐴 ) ∧ 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ) ↔ ( ◡ 𝐹 ‘ 𝐴 ) ( 𝐹 ∘ ≤ ) 𝐵 )
49 simprr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
50 brcog ⊢ ( ( ( ◡ 𝐹 ‘ 𝐴 ) ∈ V ∧ 𝐵 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝐴 ) ( 𝐹 ∘ ≤ ) 𝐵 ↔ ∃ 𝑥 ( ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ∧ 𝑥 𝐹 𝐵 ) ) )
51 46 49 50 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝐴 ) ( 𝐹 ∘ ≤ ) 𝐵 ↔ ∃ 𝑥 ( ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ∧ 𝑥 𝐹 𝐵 ) ) )
52 fvex ⊢ ( ◡ 𝐹 ‘ 𝐵 ) ∈ V
53 breq2 ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝐵 ) → ( ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ↔ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) )
54 52 53 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ( ◡ 𝐹 ‘ 𝐵 ) ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ) ↔ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) )
55 eqcom ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝐵 ) ↔ ( ◡ 𝐹 ‘ 𝐵 ) = 𝑥 )
56 fnbrfvb ⊢ ( ( ◡ 𝐹 Fn 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝐵 ) = 𝑥 ↔ 𝐵 ◡ 𝐹 𝑥 ) )
57 38 49 56 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝐵 ) = 𝑥 ↔ 𝐵 ◡ 𝐹 𝑥 ) )
58 55 57 syl5bb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑥 = ( ◡ 𝐹 ‘ 𝐵 ) ↔ 𝐵 ◡ 𝐹 𝑥 ) )
59 vex ⊢ 𝑥 ∈ V
60 brcnvg ⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝑥 ∈ V ) → ( 𝐵 ◡ 𝐹 𝑥 ↔ 𝑥 𝐹 𝐵 ) )
61 49 59 60 sylancl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ◡ 𝐹 𝑥 ↔ 𝑥 𝐹 𝐵 ) )
62 58 61 bitrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑥 = ( ◡ 𝐹 ‘ 𝐵 ) ↔ 𝑥 𝐹 𝐵 ) )
63 62 anbi1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝑥 = ( ◡ 𝐹 ‘ 𝐵 ) ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ) ↔ ( 𝑥 𝐹 𝐵 ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ) ) )
64 63 biancomd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝑥 = ( ◡ 𝐹 ‘ 𝐵 ) ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ) ↔ ( ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ∧ 𝑥 𝐹 𝐵 ) ) )
65 64 exbidv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∃ 𝑥 ( 𝑥 = ( ◡ 𝐹 ‘ 𝐵 ) ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ) ↔ ∃ 𝑥 ( ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ∧ 𝑥 𝐹 𝐵 ) ) )
66 54 65 bitr3id ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ↔ ∃ 𝑥 ( ( ◡ 𝐹 ‘ 𝐴 ) ≤ 𝑥 ∧ 𝑥 𝐹 𝐵 ) ) )
67 51 66 bitr4d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝐴 ) ( 𝐹 ∘ ≤ ) 𝐵 ↔ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) )
68 48 67 syl5bb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∃ 𝑥 ( 𝑥 = ( ◡ 𝐹 ‘ 𝐴 ) ∧ 𝑥 ( 𝐹 ∘ ≤ ) 𝐵 ) ↔ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) )
69 31 45 68 3bitrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) )
70 69 pm5.32da ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≤ 𝐵 ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) ) )
71 df-3an ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) ↔ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) )
72 70 71 bitr4di ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≤ 𝐵 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) ) )
73 29 72 bitrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝐴 ) ≤ ( ◡ 𝐹 ‘ 𝐵 ) ) ) )