Metamath Proof Explorer

Theorem fincygsubgodd

Description: Calculate the order of a subgroup of a finite cyclic group. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses fincygsubgodd.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
fincygsubgodd.2 ⊢ · = ( .g ‘ 𝐺 )
fincygsubgodd.3 ⊢ 𝐷 = ( ( ♯ ‘ 𝐵 ) / 𝐶 )
fincygsubgodd.4 ⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
fincygsubgodd.5 ⊢ 𝐻 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) )
fincygsubgodd.6 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
fincygsubgodd.7 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
fincygsubgodd.8 ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
fincygsubgodd.9 ⊢ ( 𝜑 → 𝐶 ∥ ( ♯ ‘ 𝐵 ) )
fincygsubgodd.10 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
fincygsubgodd.11 ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
Assertion fincygsubgodd ( 𝜑 → ( ♯ ‘ ran 𝐻 ) = 𝐷 )

Proof

Step Hyp Ref Expression
1 fincygsubgodd.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 fincygsubgodd.2 ⊢ · = ( .g ‘ 𝐺 )
3 fincygsubgodd.3 ⊢ 𝐷 = ( ( ♯ ‘ 𝐵 ) / 𝐶 )
4 fincygsubgodd.4 ⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
5 fincygsubgodd.5 ⊢ 𝐻 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) )
6 fincygsubgodd.6 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
7 fincygsubgodd.7 ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
8 fincygsubgodd.8 ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
9 fincygsubgodd.9 ⊢ ( 𝜑 → 𝐶 ∥ ( ♯ ‘ 𝐵 ) )
10 fincygsubgodd.10 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
11 fincygsubgodd.11 ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
12 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
13 4 rneqi ⊢ ran 𝐹 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
14 8 13 eqtr3di ⊢ ( 𝜑 → 𝐵 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) ) )
15 1 2 12 6 7 14 cycsubggenodd ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) )
16 10 iftrued ⊢ ( 𝜑 → if ( 𝐵 ∈ Fin , ( ♯ ‘ 𝐵 ) , 0 ) = ( ♯ ‘ 𝐵 ) )
17 15 16 eqtrd ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
18 17 oveq1d ⊢ ( 𝜑 → ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) / 𝐶 ) = ( ( ♯ ‘ 𝐵 ) / 𝐶 ) )
19 11 nnzd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
20 1 12 2 odmulg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ ℤ ) → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐶 gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) )
21 6 7 19 20 syl3anc ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐶 gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) )
22 1 12 odcl ⊢ ( 𝐴 ∈ 𝐵 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℕ0 )
23 nn0z ⊢ ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℕ0 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ )
24 7 22 23 3syl ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℤ )
25 9 17 breqtrrd ⊢ ( 𝜑 → 𝐶 ∥ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) )
26 11 24 25 dvdsgcdidd ⊢ ( 𝜑 → ( 𝐶 gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) = 𝐶 )
27 26 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 gcd ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ) · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) = ( 𝐶 · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) )
28 21 27 eqtrd ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( 𝐶 · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) )
29 1 12 7 odcld ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℕ0 )
30 29 nn0cnd ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℂ )
31 1 2 6 19 7 mulgcld ⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ∈ 𝐵 )
32 1 12 31 odcld ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ∈ ℕ0 )
33 32 nn0cnd ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ∈ ℂ )
34 19 zcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
35 11 nnne0d ⊢ ( 𝜑 → 𝐶 ≠ 0 )
36 30 33 34 35 divmul2d ⊢ ( 𝜑 → ( ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) / 𝐶 ) = ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝐴 ) = ( 𝐶 · ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) ) ) )
37 28 36 mpbird ⊢ ( 𝜑 → ( ( ( od ‘ 𝐺 ) ‘ 𝐴 ) / 𝐶 ) = ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) )
38 18 37 eqtr3d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) / 𝐶 ) = ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) )
39 3 38 eqtrid ⊢ ( 𝜑 → 𝐷 = ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) )
40 5 rneqi ⊢ ran 𝐻 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) )
41 40 a1i ⊢ ( 𝜑 → ran 𝐻 = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝐶 · 𝐴 ) ) ) )
42 1 2 12 6 31 41 cycsubggenodd ⊢ ( 𝜑 → ( ( od ‘ 𝐺 ) ‘ ( 𝐶 · 𝐴 ) ) = if ( ran 𝐻 ∈ Fin , ( ♯ ‘ ran 𝐻 ) , 0 ) )
43 39 42 eqtrd ⊢ ( 𝜑 → 𝐷 = if ( ran 𝐻 ∈ Fin , ( ♯ ‘ ran 𝐻 ) , 0 ) )
44 iffalse ⊢ ( ¬ ran 𝐻 ∈ Fin → if ( ran 𝐻 ∈ Fin , ( ♯ ‘ ran 𝐻 ) , 0 ) = 0 )
45 43 44 sylan9eq ⊢ ( ( 𝜑 ∧ ¬ ran 𝐻 ∈ Fin ) → 𝐷 = 0 )
46 3 a1i ⊢ ( 𝜑 → 𝐷 = ( ( ♯ ‘ 𝐵 ) / 𝐶 ) )
47 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
48 nn0cn ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
49 10 47 48 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
50 7 10 hashelne0d ⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝐵 ) = 0 )
51 50 neqned ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ≠ 0 )
52 49 34 51 35 divne0d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) / 𝐶 ) ≠ 0 )
53 46 52 eqnetrd ⊢ ( 𝜑 → 𝐷 ≠ 0 )
54 53 neneqd ⊢ ( 𝜑 → ¬ 𝐷 = 0 )
55 54 adantr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐻 ∈ Fin ) → ¬ 𝐷 = 0 )
56 45 55 condan ⊢ ( 𝜑 → ran 𝐻 ∈ Fin )
57 56 iftrued ⊢ ( 𝜑 → if ( ran 𝐻 ∈ Fin , ( ♯ ‘ ran 𝐻 ) , 0 ) = ( ♯ ‘ ran 𝐻 ) )
58 39 42 57 3eqtrrd ⊢ ( 𝜑 → ( ♯ ‘ ran 𝐻 ) = 𝐷 )