Metamath Proof Explorer

Theorem zndvds

Description: Express equality of equivalence classes in ZZ / n ZZ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses zncyg.y 
|- Y = ( Z/nZ ` N )
zndvds.2 
|- L = ( ZRHom ` Y )
Assertion zndvds 
|- ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( L ` A ) = ( L ` B ) <-> N || ( A - B ) ) )

Proof

Step Hyp Ref Expression
1 zncyg.y 
 |-  Y = ( Z/nZ ` N )
2 zndvds.2 
 |-  L = ( ZRHom ` Y )
3 eqcom 
 |-  ( ( L ` A ) = ( L ` B ) <-> ( L ` B ) = ( L ` A ) )
4 eqid 
 |-  ( RSpan ` ZZring ) = ( RSpan ` ZZring )
5 eqid 
 |-  ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) = ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) )
6 4 5 1 2 znzrhval 
 |-  ( ( N e. NN0 /\ B e. ZZ ) -> ( L ` B ) = [ B ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) )
7 6 3adant2 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( L ` B ) = [ B ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) )
8 4 5 1 2 znzrhval 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` A ) = [ A ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) )
9 8 3adant3 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( L ` A ) = [ A ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) )
10 7 9 eqeq12d 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( L ` B ) = ( L ` A ) <-> [ B ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) = [ A ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) )
11 zringring 
 |-  ZZring e. Ring
12 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
13 12 3ad2ant1 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> N e. ZZ )
14 13 snssd 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> { N } C_ ZZ )
15 zringbas 
 |-  ZZ = ( Base ` ZZring )
16 eqid 
 |-  ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
17 4 15 16 rspcl 
 |-  ( ( ZZring e. Ring /\ { N } C_ ZZ ) -> ( ( RSpan ` ZZring ) ` { N } ) e. ( LIdeal ` ZZring ) )
18 11 14 17 sylancr 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( RSpan ` ZZring ) ` { N } ) e. ( LIdeal ` ZZring ) )
19 16 lidlsubg 
 |-  ( ( ZZring e. Ring /\ ( ( RSpan ` ZZring ) ` { N } ) e. ( LIdeal ` ZZring ) ) -> ( ( RSpan ` ZZring ) ` { N } ) e. ( SubGrp ` ZZring ) )
20 11 18 19 sylancr 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( RSpan ` ZZring ) ` { N } ) e. ( SubGrp ` ZZring ) )
21 15 5 eqger 
 |-  ( ( ( RSpan ` ZZring ) ` { N } ) e. ( SubGrp ` ZZring ) -> ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) Er ZZ )
22 20 21 syl 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) Er ZZ )
23 simp3 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> B e. ZZ )
24 22 23 erth 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( B ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) A <-> [ B ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) = [ A ] ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) ) )
25 zringabl 
 |-  ZZring e. Abel
26 15 16 lidlss 
 |-  ( ( ( RSpan ` ZZring ) ` { N } ) e. ( LIdeal ` ZZring ) -> ( ( RSpan ` ZZring ) ` { N } ) C_ ZZ )
27 18 26 syl 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( RSpan ` ZZring ) ` { N } ) C_ ZZ )
28 eqid 
 |-  ( -g ` ZZring ) = ( -g ` ZZring )
29 15 28 5 eqgabl 
 |-  ( ( ZZring e. Abel /\ ( ( RSpan ` ZZring ) ` { N } ) C_ ZZ ) -> ( B ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) A <-> ( B e. ZZ /\ A e. ZZ /\ ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) ) ) )
30 25 27 29 sylancr 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( B ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) A <-> ( B e. ZZ /\ A e. ZZ /\ ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) ) ) )
31 simp2 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> A e. ZZ )
32 23 31 jca 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( B e. ZZ /\ A e. ZZ ) )
33 32 biantrurd 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) <-> ( ( B e. ZZ /\ A e. ZZ ) /\ ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) ) ) )
34 df-3an 
 |-  ( ( B e. ZZ /\ A e. ZZ /\ ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) ) <-> ( ( B e. ZZ /\ A e. ZZ ) /\ ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) ) )
35 33 34 bitr4di 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) <-> ( B e. ZZ /\ A e. ZZ /\ ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) ) ) )
36 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
37 subrgsubg 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubGrp ` CCfld ) )
38 36 37 mp1i 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ZZ e. ( SubGrp ` CCfld ) )
39 cnfldsub 
 |-  - = ( -g ` CCfld )
40 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
41 39 40 28 subgsub 
 |-  ( ( ZZ e. ( SubGrp ` CCfld ) /\ A e. ZZ /\ B e. ZZ ) -> ( A - B ) = ( A ( -g ` ZZring ) B ) )
42 38 41 syld3an1 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( A - B ) = ( A ( -g ` ZZring ) B ) )
43 42 eqcomd 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( A ( -g ` ZZring ) B ) = ( A - B ) )
44 dvdsrzring 
 |-  || = ( ||r ` ZZring )
45 15 4 44 rspsn 
 |-  ( ( ZZring e. Ring /\ N e. ZZ ) -> ( ( RSpan ` ZZring ) ` { N } ) = { x | N || x } )
46 11 13 45 sylancr 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( RSpan ` ZZring ) ` { N } ) = { x | N || x } )
47 43 46 eleq12d 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) <-> ( A - B ) e. { x | N || x } ) )
48 ovex 
 |-  ( A - B ) e. _V
49 breq2 
 |-  ( x = ( A - B ) -> ( N || x <-> N || ( A - B ) ) )
50 48 49 elab 
 |-  ( ( A - B ) e. { x | N || x } <-> N || ( A - B ) )
51 47 50 bitrdi 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( A ( -g ` ZZring ) B ) e. ( ( RSpan ` ZZring ) ` { N } ) <-> N || ( A - B ) ) )
52 30 35 51 3bitr2d 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( B ( ZZring ~QG ( ( RSpan ` ZZring ) ` { N } ) ) A <-> N || ( A - B ) ) )
53 10 24 52 3bitr2d 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( L ` B ) = ( L ` A ) <-> N || ( A - B ) ) )
54 3 53 bitrid 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( L ` A ) = ( L ` B ) <-> N || ( A - B ) ) )