Metamath Proof Explorer

Theorem znzrhfo

Description: The ZZ ring homomorphism is a surjection onto ZZ / n ZZ . (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses znzrhfo.y 
|- Y = ( Z/nZ ` N )
znzrhfo.b 
|- B = ( Base ` Y )
znzrhfo.2 
|- L = ( ZRHom ` Y )
Assertion znzrhfo 
|- ( N e. NN0 -> L : ZZ -onto-> B )

Proof

Step Hyp Ref Expression
1 znzrhfo.y 
 |-  Y = ( Z/nZ ` N )
2 znzrhfo.b 
 |-  B = ( Base ` Y )
3 znzrhfo.2 
 |-  L = ( ZRHom ` Y )
4 eqidd 
 |-  ( N e. NN0 -> ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) = ( ZZring /s ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) )
5 zringbas 
 |-  ZZ = ( Base ` ZZring )
6 5 a1i 
 |-  ( N e. NN0 -> ZZ = ( Base ` ZZring ) )
7 eqid 
 |-  ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) = ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) )
8 ovexd 
 |-  ( N e. NN0 -> ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) e. _V )
9 zringring 
 |-  ZZring e. Ring
10 9 a1i 
 |-  ( N e. NN0 -> ZZring e. Ring )
11 4 6 7 8 10 quslem 
 |-  ( N e. NN0 -> ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) : ZZ -onto-> ( ZZ /. ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) )
12 eqid 
 |-  ( RSpan ` ZZring ) = ( RSpan ` ZZring )
13 eqid 
 |-  ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) = ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) )
14 12 1 13 znbas 
 |-  ( N e. NN0 -> ( ZZ /. ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) = ( Base ` Y ) )
15 14 2 eqtr4di 
 |-  ( N e. NN0 -> ( ZZ /. ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) = B )
16 foeq3 
 |-  ( ( ZZ /. ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) = B -> ( ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) : ZZ -onto-> ( ZZ /. ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) <-> ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) : ZZ -onto-> B ) )
17 15 16 syl 
 |-  ( N e. NN0 -> ( ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) : ZZ -onto-> ( ZZ /. ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) <-> ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) : ZZ -onto-> B ) )
18 11 17 mpbid 
 |-  ( N e. NN0 -> ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) : ZZ -onto-> B )
19 12 13 1 3 znzrh2 
 |-  ( N e. NN0 -> L = ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) )
20 foeq1 
 |-  ( L = ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) -> ( L : ZZ -onto-> B <-> ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) : ZZ -onto-> B ) )
21 19 20 syl 
 |-  ( N e. NN0 -> ( L : ZZ -onto-> B <-> ( x e. ZZ |-> [ x ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) : ZZ -onto-> B ) )
22 18 21 mpbird 
 |-  ( N e. NN0 -> L : ZZ -onto-> B )