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

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝐿 ‘ 𝐾 ) = ( 𝐿 ‘ 𝑀 ) ↔ ( 𝐾 · 𝑋 ) = ( 𝑀 · 𝑋 ) ) )