Metamath Proof Explorer

Theorem znle2

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 )
Assertion znle2 
|- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )

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 eqid 
 |-  ( RSpan ` ZZring ) = ( RSpan ` ZZring )
6 eqid 
 |-  ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) = ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) )
7 eqid 
 |-  ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W ) = ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W )
8 5 6 1 7 3 4 znle 
 |-  ( N e. NN0 -> .<_ = ( ( ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W ) o. <_ ) o. `' ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W ) ) )
9 5 6 1 znzrh 
 |-  ( N e. NN0 -> ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) = ( ZRHom ` Y ) )
10 9 reseq1d 
 |-  ( N e. NN0 -> ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W ) = ( ( ZRHom ` Y ) |` W ) )
11 10 2 eqtr4di 
 |-  ( N e. NN0 -> ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W ) = F )
12 11 coeq1d 
 |-  ( N e. NN0 -> ( ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W ) o. <_ ) = ( F o. <_ ) )
13 11 cnveqd 
 |-  ( N e. NN0 -> `' ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W ) = `' F )
14 12 13 coeq12d 
 |-  ( N e. NN0 -> ( ( ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W ) o. <_ ) o. `' ( ( ZRHom ` ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) ) |` W ) ) = ( ( F o. <_ ) o. `' F ) )
15 8 14 eqtrd 
 |-  ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )