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 
|- 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 znleval2 
|- ( ( N e. NN0 /\ A e. X /\ B e. X ) -> ( A .<_ B <-> ( `' 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 5 znleval 
 |-  ( N e. NN0 -> ( A .<_ B <-> ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )
7 6 3ad2ant1 
 |-  ( ( N e. NN0 /\ A e. X /\ B e. X ) -> ( A .<_ B <-> ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )
8 3simpc 
 |-  ( ( N e. NN0 /\ A e. X /\ B e. X ) -> ( A e. X /\ B e. X ) )
9 8 biantrurd 
 |-  ( ( N e. NN0 /\ A e. X /\ B e. X ) -> ( ( `' F ` A ) <_ ( `' F ` B ) <-> ( ( A e. X /\ B e. X ) /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )
10 df-3an 
 |-  ( ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) <-> ( ( A e. X /\ B e. X ) /\ ( `' F ` A ) <_ ( `' F ` B ) ) )
11 9 10 bitr4di 
 |-  ( ( N e. NN0 /\ A e. X /\ B e. X ) -> ( ( `' F ` A ) <_ ( `' F ` B ) <-> ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )
12 7 11 bitr4d 
 |-  ( ( N e. NN0 /\ A e. X /\ B e. X ) -> ( A .<_ B <-> ( `' F ` A ) <_ ( `' F ` B ) ) )