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 ) ) ) )