Metamath Proof Explorer

Theorem znval

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 Mario Carneiro, 2-May-2016) (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 ) )
znval.l 
|- .<_ = ( ( F o. <_ ) o. `' F )
Assertion znval 
|- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )

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 znval.l 
 |-  .<_ = ( ( F o. <_ ) o. `' F )
7 zringring 
 |-  ZZring e. Ring
8 7 a1i 
 |-  ( n = N -> ZZring e. Ring )
9 ovexd 
 |-  ( ( n = N /\ z = ZZring ) -> ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) e. _V )
10 id 
 |-  ( s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) -> s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) )
11 simpr 
 |-  ( ( n = N /\ z = ZZring ) -> z = ZZring )
12 11 fveq2d 
 |-  ( ( n = N /\ z = ZZring ) -> ( RSpan ` z ) = ( RSpan ` ZZring ) )
13 12 1 eqtr4di 
 |-  ( ( n = N /\ z = ZZring ) -> ( RSpan ` z ) = S )
14 simpl 
 |-  ( ( n = N /\ z = ZZring ) -> n = N )
15 14 sneqd 
 |-  ( ( n = N /\ z = ZZring ) -> { n } = { N } )
16 13 15 fveq12d 
 |-  ( ( n = N /\ z = ZZring ) -> ( ( RSpan ` z ) ` { n } ) = ( S ` { N } ) )
17 11 16 oveq12d 
 |-  ( ( n = N /\ z = ZZring ) -> ( z ~QG ( ( RSpan ` z ) ` { n } ) ) = ( ZZring ~QG ( S ` { N } ) ) )
18 11 17 oveq12d 
 |-  ( ( n = N /\ z = ZZring ) -> ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) ) )
19 18 2 eqtr4di 
 |-  ( ( n = N /\ z = ZZring ) -> ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) = U )
20 10 19 sylan9eqr 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> s = U )
21 fvex 
 |-  ( ZRHom ` s ) e. _V
22 21 resex 
 |-  ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) e. _V
23 22 a1i 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) e. _V )
24 id 
 |-  ( f = ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) -> f = ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) )
25 20 fveq2d 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> ( ZRHom ` s ) = ( ZRHom ` U ) )
26 simpll 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> n = N )
27 26 eqeq1d 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> ( n = 0 <-> N = 0 ) )
28 26 oveq2d 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> ( 0 ..^ n ) = ( 0 ..^ N ) )
29 27 28 ifbieq2d 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> if ( n = 0 , ZZ , ( 0 ..^ n ) ) = if ( N = 0 , ZZ , ( 0 ..^ N ) ) )
30 29 5 eqtr4di 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> if ( n = 0 , ZZ , ( 0 ..^ n ) ) = W )
31 25 30 reseq12d 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) = ( ( ZRHom ` U ) |` W ) )
32 31 4 eqtr4di 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) = F )
33 24 32 sylan9eqr 
 |-  ( ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) /\ f = ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) ) -> f = F )
34 33 coeq1d 
 |-  ( ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) /\ f = ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) ) -> ( f o. <_ ) = ( F o. <_ ) )
35 33 cnveqd 
 |-  ( ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) /\ f = ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) ) -> `' f = `' F )
36 34 35 coeq12d 
 |-  ( ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) /\ f = ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) ) -> ( ( f o. <_ ) o. `' f ) = ( ( F o. <_ ) o. `' F ) )
37 36 6 eqtr4di 
 |-  ( ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) /\ f = ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) ) -> ( ( f o. <_ ) o. `' f ) = .<_ )
38 23 37 csbied 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) = .<_ )
39 38 opeq2d 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. = <. ( le ` ndx ) , .<_ >. )
40 20 39 oveq12d 
 |-  ( ( ( n = N /\ z = ZZring ) /\ s = ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) ) -> ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. ) = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
41 9 40 csbied 
 |-  ( ( n = N /\ z = ZZring ) -> [_ ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) / s ]_ ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. ) = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
42 8 41 csbied 
 |-  ( n = N -> [_ ZZring / z ]_ [_ ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) / s ]_ ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. ) = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
43 df-zn 
 |-  Z/nZ = ( n e. NN0 |-> [_ ZZring / z ]_ [_ ( z /s ( z ~QG ( ( RSpan ` z ) ` { n } ) ) ) / s ]_ ( s sSet <. ( le ` ndx ) , [_ ( ( ZRHom ` s ) |` if ( n = 0 , ZZ , ( 0 ..^ n ) ) ) / f ]_ ( ( f o. <_ ) o. `' f ) >. ) )
44 ovex 
 |-  ( U sSet <. ( le ` ndx ) , .<_ >. ) e. _V
45 42 43 44 fvmpt 
 |-  ( N e. NN0 -> ( Z/nZ ` N ) = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
46 3 45 syl5eq 
 |-  ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )