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 = ℤ/Nℤ
zndvds.2 ⊢ L = ℤRHom ⁡ Y
Assertion zndvds ⊢ N ∈ ℕ 0 ∧ A ∈ ℤ ∧ B ∈ ℤ → L ⁡ A = L ⁡ B ↔ N ∥ A − B

Proof

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