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 ↔ 𝑁 ∥ 𝐴 ) )