This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znle

Description: The value of the Z/nZ structure. It is defined as the quotient ring ZZ / n ZZ , with an "artificial" ordering added to make it a Toset . (In other words, Z/nZ is aring with anorder , but it is not anordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znval.s 
|- S = ( RSpan ` ZZring )
znval.u 
|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
znval.y 
|- Y = ( Z/nZ ` N )
znval.f 
|- F = ( ( ZRHom ` U ) |` W )
znval.w 
|- W = if ( N = 0 , ZZ , ( 0 ..^ N ) )
znle.l 
|- .<_ = ( le ` Y )
Assertion znle 
|- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )

Proof

Step Hyp Ref Expression
1 znval.s 
 |-  S = ( RSpan ` ZZring )
2 znval.u 
 |-  U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
3 znval.y 
 |-  Y = ( Z/nZ ` N )
4 znval.f 
 |-  F = ( ( ZRHom ` U ) |` W )
5 znval.w 
 |-  W = if ( N = 0 , ZZ , ( 0 ..^ N ) )
6 znle.l 
 |-  .<_ = ( le ` Y )
7 eqid 
 |-  ( ( F o. <_ ) o. `' F ) = ( ( F o. <_ ) o. `' F )
8 1 2 3 4 5 7 znval 
 |-  ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , ( ( F o. <_ ) o. `' F ) >. ) )
9 8 fveq2d 
 |-  ( N e. NN0 -> ( le ` Y ) = ( le ` ( U sSet <. ( le ` ndx ) , ( ( F o. <_ ) o. `' F ) >. ) ) )
10 2 ovexi 
 |-  U e. _V
11 fvex 
 |-  ( ZRHom ` U ) e. _V
12 11 resex 
 |-  ( ( ZRHom ` U ) |` W ) e. _V
13 4 12 eqeltri 
 |-  F e. _V
14 xrex 
 |-  RR* e. _V
15 14 14 xpex 
 |-  ( RR* X. RR* ) e. _V
16 lerelxr 
 |-  <_ C_ ( RR* X. RR* )
17 15 16 ssexi 
 |-  <_ e. _V
18 13 17 coex 
 |-  ( F o. <_ ) e. _V
19 13 cnvex 
 |-  `' F e. _V
20 18 19 coex 
 |-  ( ( F o. <_ ) o. `' F ) e. _V
21 pleid 
 |-  le = Slot ( le ` ndx )
22 21 setsid 
 |-  ( ( U e. _V /\ ( ( F o. <_ ) o. `' F ) e. _V ) -> ( ( F o. <_ ) o. `' F ) = ( le ` ( U sSet <. ( le ` ndx ) , ( ( F o. <_ ) o. `' F ) >. ) ) )
23 10 20 22 mp2an 
 |-  ( ( F o. <_ ) o. `' F ) = ( le ` ( U sSet <. ( le ` ndx ) , ( ( F o. <_ ) o. `' F ) >. ) )
24 9 6 23 3eqtr4g 
 |-  ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )