Theorem cygznlem1

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

	Ref	Expression
Hypotheses	cygzn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cygzn.n	⊢ 𝑁 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 )
	cygzn.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	cygzn.m	⊢ · = ( .g ‘ 𝐺 )
	cygzn.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
	cygzn.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
	cygzn.g	⊢ ( 𝜑 → 𝐺 ∈ CycGrp )
	cygzn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
Assertion	cygznlem1	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝐿 ‘ 𝐾 ) = ( 𝐿 ‘ 𝑀 ) ↔ ( 𝐾 · 𝑋 ) = ( 𝑀 · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cygzn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cygzn.n	⊢ 𝑁 = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 )
3		cygzn.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
4		cygzn.m	⊢ · = ( .g ‘ 𝐺 )
5		cygzn.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
6		cygzn.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
7		cygzn.g	⊢ ( 𝜑 → 𝐺 ∈ CycGrp )
8		cygzn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
9		hashcl	⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
11		0nn0	⊢ 0 ∈ ℕ0
12	11	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ Fin ) → 0 ∈ ℕ0 )
13	10 12	ifclda	⊢ ( 𝜑 → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) ∈ ℕ0 )
14	2 13	eqeltrid	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑁 ∈ ℕ0 )
16		simprl	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝐾 ∈ ℤ )
17		simprr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
18	3 5	zndvds	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐾 ) = ( 𝐿 ‘ 𝑀 ) ↔ 𝑁 ∥ ( 𝐾 − 𝑀 ) ) )
19	15 16 17 18	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝐿 ‘ 𝐾 ) = ( 𝐿 ‘ 𝑀 ) ↔ 𝑁 ∥ ( 𝐾 − 𝑀 ) ) )
20		cyggrp	⊢ ( 𝐺 ∈ CycGrp → 𝐺 ∈ Grp )
21	7 20	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
22		eqid	⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
23	1 4 6 22	cyggenod2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) → ( ( od ‘ 𝐺 ) ‘ 𝑋 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
24	21 8 23	syl2anc	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝑋 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
25	24 2	eqtr4di	⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝑋 ) = 𝑁 )
26	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( od ‘ 𝐺 ) ‘ 𝑋 ) = 𝑁 )
27	26	breq1d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑋 ) ∥ ( 𝐾 − 𝑀 ) ↔ 𝑁 ∥ ( 𝐾 − 𝑀 ) ) )
28	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝐺 ∈ Grp )
29	1 4 6	iscyggen	⊢ ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )
30	29	simplbi	⊢ ( 𝑋 ∈ 𝐸 → 𝑋 ∈ 𝐵 )
31	8 30	syl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
32	31	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑋 ∈ 𝐵 )
33		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
34	1 22 4 33	odcong	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑋 ) ∥ ( 𝐾 − 𝑀 ) ↔ ( 𝐾 · 𝑋 ) = ( 𝑀 · 𝑋 ) ) )
35	28 32 16 17 34	syl112anc	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑋 ) ∥ ( 𝐾 − 𝑀 ) ↔ ( 𝐾 · 𝑋 ) = ( 𝑀 · 𝑋 ) ) )
36	19 27 35	3bitr2d	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝐿 ‘ 𝐾 ) = ( 𝐿 ‘ 𝑀 ) ↔ ( 𝐾 · 𝑋 ) = ( 𝑀 · 𝑋 ) ) )