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

Metamath Proof Explorer

Theorem znval2

Description: Self-referential expression for the Z/nZ structure. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypotheses znval2.s 
|- S = ( RSpan ` ZZring )
znval2.u 
|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
znval2.y 
|- Y = ( Z/nZ ` N )
znval2.l 
|- .<_ = ( le ` Y )
Assertion znval2 
|- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )

Proof

Step Hyp Ref Expression
1 znval2.s 
 |-  S = ( RSpan ` ZZring )
2 znval2.u 
 |-  U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
3 znval2.y 
 |-  Y = ( Z/nZ ` N )
4 znval2.l 
 |-  .<_ = ( le ` Y )
5 eqid 
 |-  ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) = ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) )
6 eqid 
 |-  if ( N = 0 , ZZ , ( 0 ..^ N ) ) = if ( N = 0 , ZZ , ( 0 ..^ N ) )
7 eqid 
 |-  ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) = ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) )
8 1 2 3 5 6 7 znval 
 |-  ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) >. ) )
9 1 2 3 5 6 4 znle 
 |-  ( N e. NN0 -> .<_ = ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) )
10 9 opeq2d 
 |-  ( N e. NN0 -> <. ( le ` ndx ) , .<_ >. = <. ( le ` ndx ) , ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) >. )
11 10 oveq2d 
 |-  ( N e. NN0 -> ( U sSet <. ( le ` ndx ) , .<_ >. ) = ( U sSet <. ( le ` ndx ) , ( ( ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) o. <_ ) o. `' ( ( ZRHom ` U ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) ) >. ) )
12 8 11 eqtr4d 
 |-  ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )