Metamath Proof Explorer

Theorem cygznlem1

Description: Lemma for cygzn . (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygzn.b ⊢ B = Base G
cygzn.n ⊢ N = if B ∈ Fin B 0
cygzn.y ⊢ Y = ℤ/Nℤ
cygzn.m ⊢ · ˙ = ⋅ G
cygzn.l ⊢ L = ℤRHom ⁡ Y
cygzn.e ⊢ E = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
cygzn.g ⊢ φ → G ∈ CycGrp
cygzn.x ⊢ φ → X ∈ E
Assertion cygznlem1 ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → L ⁡ K = L ⁡ M ↔ K · ˙ X = M · ˙ X

Proof

Step Hyp Ref Expression
1 cygzn.b ⊢ B = Base G
2 cygzn.n ⊢ N = if B ∈ Fin B 0
3 cygzn.y ⊢ Y = ℤ/Nℤ
4 cygzn.m ⊢ · ˙ = ⋅ G
5 cygzn.l ⊢ L = ℤRHom ⁡ Y
6 cygzn.e ⊢ E = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
7 cygzn.g ⊢ φ → G ∈ CycGrp
8 cygzn.x ⊢ φ → X ∈ E
9 hashcl ⊢ B ∈ Fin → B ∈ ℕ 0
10 9 adantl ⊢ φ ∧ B ∈ Fin → B ∈ ℕ 0
11 0nn0 ⊢ 0 ∈ ℕ 0
12 11 a1i ⊢ φ ∧ ¬ B ∈ Fin → 0 ∈ ℕ 0
13 10 12 ifclda ⊢ φ → if B ∈ Fin B 0 ∈ ℕ 0
14 2 13 eqeltrid ⊢ φ → N ∈ ℕ 0
15 14 adantr ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → N ∈ ℕ 0
16 simprl ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → K ∈ ℤ
17 simprr ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → M ∈ ℤ
18 3 5 zndvds ⊢ N ∈ ℕ 0 ∧ K ∈ ℤ ∧ M ∈ ℤ → L ⁡ K = L ⁡ M ↔ N ∥ K − M
19 15 16 17 18 syl3anc ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → L ⁡ K = L ⁡ M ↔ N ∥ K − M
20 cyggrp ⊢ G ∈ CycGrp → G ∈ Grp
21 7 20 syl ⊢ φ → G ∈ Grp
22 eqid ⊢ od ⁡ G = od ⁡ G
23 1 4 6 22 cyggenod2 ⊢ G ∈ Grp ∧ X ∈ E → od ⁡ G ⁡ X = if B ∈ Fin B 0
24 21 8 23 syl2anc ⊢ φ → od ⁡ G ⁡ X = if B ∈ Fin B 0
25 24 2 eqtr4di ⊢ φ → od ⁡ G ⁡ X = N
26 25 adantr ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → od ⁡ G ⁡ X = N
27 26 breq1d ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → od ⁡ G ⁡ X ∥ K − M ↔ N ∥ K − M
28 21 adantr ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → G ∈ Grp
29 1 4 6 iscyggen ⊢ X ∈ E ↔ X ∈ B ∧ ran ⁡ n ∈ ℤ ⟼ n · ˙ X = B
30 29 simplbi ⊢ X ∈ E → X ∈ B
31 8 30 syl ⊢ φ → X ∈ B
32 31 adantr ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → X ∈ B
33 eqid ⊢ 0 G = 0 G
34 1 22 4 33 odcong ⊢ G ∈ Grp ∧ X ∈ B ∧ K ∈ ℤ ∧ M ∈ ℤ → od ⁡ G ⁡ X ∥ K − M ↔ K · ˙ X = M · ˙ X
35 28 32 16 17 34 syl112anc ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → od ⁡ G ⁡ X ∥ K − M ↔ K · ˙ X = M · ˙ X
36 19 27 35 3bitr2d ⊢ φ ∧ K ∈ ℤ ∧ M ∈ ℤ → L ⁡ K = L ⁡ M ↔ K · ˙ X = M · ˙ X