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 ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
zndvds.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
zndvds0.3 ⊢ 0 = ( 0g ‘ 𝑌 )
Assertion zndvds0 ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = 0 ↔ 𝑁 ∥ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 zncyg.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 zndvds.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
3 zndvds0.3 ⊢ 0 = ( 0g ‘ 𝑌 )
4 0z ⊢ 0 ∈ ℤ
5 1 2 zndvds ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 0 ) ↔ 𝑁 ∥ ( 𝐴 − 0 ) ) )
6 4 5 mp3an3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 0 ) ↔ 𝑁 ∥ ( 𝐴 − 0 ) ) )
7 1 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CRing )
8 7 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝑌 ∈ CRing )
9 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
10 2 zrhrhm ⊢ ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
11 8 9 10 3syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
12 rhmghm ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) → 𝐿 ∈ ( ℤring GrpHom 𝑌 ) )
13 zring0 ⊢ 0 = ( 0g ‘ ℤring )
14 13 3 ghmid ⊢ ( 𝐿 ∈ ( ℤring GrpHom 𝑌 ) → ( 𝐿 ‘ 0 ) = 0 )
15 11 12 14 3syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 0 ) = 0 )
16 15 eqeq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 0 ) ↔ ( 𝐿 ‘ 𝐴 ) = 0 ) )
17 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℤ )
18 17 zcnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℂ )
19 18 subid1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝐴 − 0 ) = 𝐴 )
20 19 breq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝑁 ∥ ( 𝐴 − 0 ) ↔ 𝑁 ∥ 𝐴 ) )
21 6 16 20 3bitr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = 0 ↔ 𝑁 ∥ 𝐴 ) )