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
|- Y = ( Z/nZ ` N )
znle2.f
|- F = ( ( ZRHom ` Y ) |` W )
znle2.w
|- W = if ( N = 0 , ZZ , ( 0 ..^ N ) )
znle2.l
|- .<_ = ( le ` Y )
znleval.x
|- X = ( Base ` Y )
Assertion znleval
|- ( N e. NN0 -> ( A .<_ B <-> ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 znle2.y
 |-  Y = ( Z/nZ ` N )
2 znle2.f
 |-  F = ( ( ZRHom ` Y ) |` W )
3 znle2.w
 |-  W = if ( N = 0 , ZZ , ( 0 ..^ N ) )
4 znle2.l
 |-  .<_ = ( le ` Y )
5 znleval.x
 |-  X = ( Base ` Y )
6 1 2 3 4 znle2
 |-  ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )
7 relco
 |-  Rel ( ( F o. <_ ) o. `' F )
8 relssdmrn
 |-  ( Rel ( ( F o. <_ ) o. `' F ) -> ( ( F o. <_ ) o. `' F ) C_ ( dom ( ( F o. <_ ) o. `' F ) X. ran ( ( F o. <_ ) o. `' F ) ) )
9 7 8 ax-mp
 |-  ( ( F o. <_ ) o. `' F ) C_ ( dom ( ( F o. <_ ) o. `' F ) X. ran ( ( F o. <_ ) o. `' F ) )
10 dmcoss
 |-  dom ( ( F o. <_ ) o. `' F ) C_ dom `' F
11 df-rn
 |-  ran F = dom `' F
12 1 5 2 3 znf1o
 |-  ( N e. NN0 -> F : W -1-1-onto-> X )
13 f1ofo
 |-  ( F : W -1-1-onto-> X -> F : W -onto-> X )
14 forn
 |-  ( F : W -onto-> X -> ran F = X )
15 12 13 14 3syl
 |-  ( N e. NN0 -> ran F = X )
16 11 15 eqtr3id
 |-  ( N e. NN0 -> dom `' F = X )
17 10 16 sseqtrid
 |-  ( N e. NN0 -> dom ( ( F o. <_ ) o. `' F ) C_ X )
18 rncoss
 |-  ran ( ( F o. <_ ) o. `' F ) C_ ran ( F o. <_ )
19 rncoss
 |-  ran ( F o. <_ ) C_ ran F
20 19 15 sseqtrid
 |-  ( N e. NN0 -> ran ( F o. <_ ) C_ X )
21 18 20 sstrid
 |-  ( N e. NN0 -> ran ( ( F o. <_ ) o. `' F ) C_ X )
22 xpss12
 |-  ( ( dom ( ( F o. <_ ) o. `' F ) C_ X /\ ran ( ( F o. <_ ) o. `' F ) C_ X ) -> ( dom ( ( F o. <_ ) o. `' F ) X. ran ( ( F o. <_ ) o. `' F ) ) C_ ( X X. X ) )
23 17 21 22 syl2anc
 |-  ( N e. NN0 -> ( dom ( ( F o. <_ ) o. `' F ) X. ran ( ( F o. <_ ) o. `' F ) ) C_ ( X X. X ) )
24 9 23 sstrid
 |-  ( N e. NN0 -> ( ( F o. <_ ) o. `' F ) C_ ( X X. X ) )
25 6 24 eqsstrd
 |-  ( N e. NN0 -> .<_ C_ ( X X. X ) )
26 25 ssbrd
 |-  ( N e. NN0 -> ( A .<_ B -> A ( X X. X ) B ) )
27 brxp
 |-  ( A ( X X. X ) B <-> ( A e. X /\ B e. X ) )
28 26 27 syl6ib
 |-  ( N e. NN0 -> ( A .<_ B -> ( A e. X /\ B e. X ) ) )
29 28 pm4.71rd
 |-  ( N e. NN0 -> ( A .<_ B <-> ( ( A e. X /\ B e. X ) /\ A .<_ B ) ) )
30 6 adantr
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> .<_ = ( ( F o. <_ ) o. `' F ) )
31 30 breqd
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( A .<_ B <-> A ( ( F o. <_ ) o. `' F ) B ) )
32 brcog
 |-  ( ( A e. X /\ B e. X ) -> ( A ( ( F o. <_ ) o. `' F ) B <-> E. x ( A `' F x /\ x ( F o. <_ ) B ) ) )
33 32 adantl
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( A ( ( F o. <_ ) o. `' F ) B <-> E. x ( A `' F x /\ x ( F o. <_ ) B ) ) )
34 eqcom
 |-  ( x = ( `' F ` A ) <-> ( `' F ` A ) = x )
35 12 adantr
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> F : W -1-1-onto-> X )
36 f1ocnv
 |-  ( F : W -1-1-onto-> X -> `' F : X -1-1-onto-> W )
37 f1ofn
 |-  ( `' F : X -1-1-onto-> W -> `' F Fn X )
38 35 36 37 3syl
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> `' F Fn X )
39 simprl
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> A e. X )
40 fnbrfvb
 |-  ( ( `' F Fn X /\ A e. X ) -> ( ( `' F ` A ) = x <-> A `' F x ) )
41 38 39 40 syl2anc
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( ( `' F ` A ) = x <-> A `' F x ) )
42 34 41 bitr2id
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( A `' F x <-> x = ( `' F ` A ) ) )
43 42 anbi1d
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( ( A `' F x /\ x ( F o. <_ ) B ) <-> ( x = ( `' F ` A ) /\ x ( F o. <_ ) B ) ) )
44 43 exbidv
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( E. x ( A `' F x /\ x ( F o. <_ ) B ) <-> E. x ( x = ( `' F ` A ) /\ x ( F o. <_ ) B ) ) )
45 33 44 bitrd
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( A ( ( F o. <_ ) o. `' F ) B <-> E. x ( x = ( `' F ` A ) /\ x ( F o. <_ ) B ) ) )
46 fvex
 |-  ( `' F ` A ) e. _V
47 breq1
 |-  ( x = ( `' F ` A ) -> ( x ( F o. <_ ) B <-> ( `' F ` A ) ( F o. <_ ) B ) )
48 46 47 ceqsexv
 |-  ( E. x ( x = ( `' F ` A ) /\ x ( F o. <_ ) B ) <-> ( `' F ` A ) ( F o. <_ ) B )
49 simprr
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> B e. X )
50 brcog
 |-  ( ( ( `' F ` A ) e. _V /\ B e. X ) -> ( ( `' F ` A ) ( F o. <_ ) B <-> E. x ( ( `' F ` A ) <_ x /\ x F B ) ) )
51 46 49 50 sylancr
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( ( `' F ` A ) ( F o. <_ ) B <-> E. x ( ( `' F ` A ) <_ x /\ x F B ) ) )
52 fvex
 |-  ( `' F ` B ) e. _V
53 breq2
 |-  ( x = ( `' F ` B ) -> ( ( `' F ` A ) <_ x <-> ( `' F ` A ) <_ ( `' F ` B ) ) )
54 52 53 ceqsexv
 |-  ( E. x ( x = ( `' F ` B ) /\ ( `' F ` A ) <_ x ) <-> ( `' F ` A ) <_ ( `' F ` B ) )
55 eqcom
 |-  ( x = ( `' F ` B ) <-> ( `' F ` B ) = x )
56 fnbrfvb
 |-  ( ( `' F Fn X /\ B e. X ) -> ( ( `' F ` B ) = x <-> B `' F x ) )
57 38 49 56 syl2anc
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( ( `' F ` B ) = x <-> B `' F x ) )
58 55 57 syl5bb
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( x = ( `' F ` B ) <-> B `' F x ) )
59 vex
 |-  x e. _V
60 brcnvg
 |-  ( ( B e. X /\ x e. _V ) -> ( B `' F x <-> x F B ) )
61 49 59 60 sylancl
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( B `' F x <-> x F B ) )
62 58 61 bitrd
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( x = ( `' F ` B ) <-> x F B ) )
63 62 anbi1d
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( ( x = ( `' F ` B ) /\ ( `' F ` A ) <_ x ) <-> ( x F B /\ ( `' F ` A ) <_ x ) ) )
64 63 biancomd
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( ( x = ( `' F ` B ) /\ ( `' F ` A ) <_ x ) <-> ( ( `' F ` A ) <_ x /\ x F B ) ) )
65 64 exbidv
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( E. x ( x = ( `' F ` B ) /\ ( `' F ` A ) <_ x ) <-> E. x ( ( `' F ` A ) <_ x /\ x F B ) ) )
66 54 65 bitr3id
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( ( `' F ` A ) <_ ( `' F ` B ) <-> E. x ( ( `' F ` A ) <_ x /\ x F B ) ) )
67 51 66 bitr4d
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( ( `' F ` A ) ( F o. <_ ) B <-> ( `' F ` A ) <_ ( `' F ` B ) ) )
68 48 67 syl5bb
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( E. x ( x = ( `' F ` A ) /\ x ( F o. <_ ) B ) <-> ( `' F ` A ) <_ ( `' F ` B ) ) )
69 31 45 68 3bitrd
 |-  ( ( N e. NN0 /\ ( A e. X /\ B e. X ) ) -> ( A .<_ B <-> ( `' F ` A ) <_ ( `' F ` B ) ) )
70 69 pm5.32da
 |-  ( N e. NN0 -> ( ( ( A e. X /\ B e. X ) /\ A .<_ B ) <-> ( ( A e. X /\ B e. X ) /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )
71 df-3an
 |-  ( ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) <-> ( ( A e. X /\ B e. X ) /\ ( `' F ` A ) <_ ( `' F ` B ) ) )
72 70 71 bitr4di
 |-  ( N e. NN0 -> ( ( ( A e. X /\ B e. X ) /\ A .<_ B ) <-> ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )
73 29 72 bitrd
 |-  ( N e. NN0 -> ( A .<_ B <-> ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )