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

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

Proof

Step Hyp Ref Expression
1 zncyg.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 zndvds.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
3 eqcom ⊢ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝐵 ) ↔ ( 𝐿 ‘ 𝐵 ) = ( 𝐿 ‘ 𝐴 ) )
4 eqid ⊢ ( RSpan ‘ ℤring ) = ( RSpan ‘ ℤring )
5 eqid ⊢ ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) = ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) )
6 4 5 1 2 znzrhval ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ) → ( 𝐿 ‘ 𝐵 ) = [ 𝐵 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
7 6 3adant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐿 ‘ 𝐵 ) = [ 𝐵 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
8 4 5 1 2 znzrhval ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) = [ 𝐴 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
9 8 3adant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) = [ 𝐴 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
10 7 9 eqeq12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐵 ) = ( 𝐿 ‘ 𝐴 ) ↔ [ 𝐵 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) = [ 𝐴 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
11 zringring ⊢ ℤring ∈ Ring
12 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
13 12 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝑁 ∈ ℤ )
14 13 snssd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { 𝑁 } ⊆ ℤ )
15 zringbas ⊢ ℤ = ( Base ‘ ℤring )
16 eqid ⊢ ( LIdeal ‘ ℤring ) = ( LIdeal ‘ ℤring )
17 4 15 16 rspcl ⊢ ( ( ℤring ∈ Ring ∧ { 𝑁 } ⊆ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
18 11 14 17 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
19 16 lidlsubg ⊢ ( ( ℤring ∈ Ring ∧ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( SubGrp ‘ ℤring ) )
20 11 18 19 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( SubGrp ‘ ℤring ) )
21 15 5 eqger ⊢ ( ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( SubGrp ‘ ℤring ) → ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) Er ℤ )
22 20 21 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) Er ℤ )
23 simp3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℤ )
24 22 23 erth ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) 𝐴 ↔ [ 𝐵 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) = [ 𝐴 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
25 zringabl ⊢ ℤring ∈ Abel
26 15 16 lidlss ⊢ ( ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ⊆ ℤ )
27 18 26 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ⊆ ℤ )
28 eqid ⊢ ( -g ‘ ℤring ) = ( -g ‘ ℤring )
29 15 28 5 eqgabl ⊢ ( ( ℤring ∈ Abel ∧ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ⊆ ℤ ) → ( 𝐵 ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) 𝐴 ↔ ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
30 25 27 29 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) 𝐴 ↔ ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
31 simp2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
32 23 31 jca ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
33 32 biantrurd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ↔ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
34 df-3an ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ↔ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
35 33 34 bitr4di ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ↔ ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
36 zsubrg ⊢ ℤ ∈ ( SubRing ‘ ℂfld )
37 subrgsubg ⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubGrp ‘ ℂfld ) )
38 36 37 mp1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ℤ ∈ ( SubGrp ‘ ℂfld ) )
39 cnfldsub ⊢ − = ( -g ‘ ℂfld )
40 df-zring ⊢ ℤring = ( ℂfld ↾s ℤ )
41 39 40 28 subgsub ⊢ ( ( ℤ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) )
42 38 41 syld3an1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) )
43 42 eqcomd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) = ( 𝐴 − 𝐵 ) )
44 dvdsrzring ⊢ ∥ = ( ∥r ‘ ℤring )
45 15 4 44 rspsn ⊢ ( ( ℤring ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) = { 𝑥 ∣ 𝑁 ∥ 𝑥 } )
46 11 13 45 sylancr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) = { 𝑥 ∣ 𝑁 ∥ 𝑥 } )
47 43 46 eleq12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ↔ ( 𝐴 − 𝐵 ) ∈ { 𝑥 ∣ 𝑁 ∥ 𝑥 } ) )
48 ovex ⊢ ( 𝐴 − 𝐵 ) ∈ V
49 breq2 ⊢ ( 𝑥 = ( 𝐴 − 𝐵 ) → ( 𝑁 ∥ 𝑥 ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )
50 48 49 elab ⊢ ( ( 𝐴 − 𝐵 ) ∈ { 𝑥 ∣ 𝑁 ∥ 𝑥 } ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) )
51 47 50 bitrdi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )
52 30 35 51 3bitr2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) 𝐴 ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )
53 10 24 52 3bitr2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐵 ) = ( 𝐿 ‘ 𝐴 ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )
54 3 53 bitrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝐵 ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )