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

Metamath Proof Explorer

Theorem zndvds0

Description: Special case of zndvds when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 zncyg.y 
 |-  Y = ( Z/nZ ` N )
2 zndvds.2 
 |-  L = ( ZRHom ` Y )
3 zndvds0.3 
 |-  .0. = ( 0g ` Y )
4 0z 
 |-  0 e. ZZ
5 1 2 zndvds 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ 0 e. ZZ ) -> ( ( L ` A ) = ( L ` 0 ) <-> N || ( A - 0 ) ) )
6 4 5 mp3an3 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) = ( L ` 0 ) <-> N || ( A - 0 ) ) )
7 1 zncrng 
 |-  ( N e. NN0 -> Y e. CRing )
8 7 adantr 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> Y e. CRing )
9 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
10 2 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
11 8 9 10 3syl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> L e. ( ZZring RingHom Y ) )
12 rhmghm 
 |-  ( L e. ( ZZring RingHom Y ) -> L e. ( ZZring GrpHom Y ) )
13 zring0 
 |-  0 = ( 0g ` ZZring )
14 13 3 ghmid 
 |-  ( L e. ( ZZring GrpHom Y ) -> ( L ` 0 ) = .0. )
15 11 12 14 3syl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` 0 ) = .0. )
16 15 eqeq2d 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) = ( L ` 0 ) <-> ( L ` A ) = .0. ) )
17 simpr 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> A e. ZZ )
18 17 zcnd 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> A e. CC )
19 18 subid1d 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( A - 0 ) = A )
20 19 breq2d 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( N || ( A - 0 ) <-> N || A ) )
21 6 16 20 3bitr3d 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) = .0. <-> N || A ) )