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 ⊢ B = Base G
fincygsubgodd.2 ⊢ · ˙ = ⋅ G
fincygsubgodd.3 ⊢ D = B C
fincygsubgodd.4 ⊢ F = n ∈ ℤ ⟼ n · ˙ A
fincygsubgodd.5 ⊢ H = n ∈ ℤ ⟼ n · ˙ C · ˙ A
fincygsubgodd.6 ⊢ φ → G ∈ Grp
fincygsubgodd.7 ⊢ φ → A ∈ B
fincygsubgodd.8 ⊢ φ → ran ⁡ F = B
fincygsubgodd.9 ⊢ φ → C ∥ B
fincygsubgodd.10 ⊢ φ → B ∈ Fin
fincygsubgodd.11 ⊢ φ → C ∈ ℕ
Assertion fincygsubgodd ⊢ φ → ran ⁡ H = D

Proof

Step Hyp Ref Expression
1 fincygsubgodd.1 ⊢ B = Base G
2 fincygsubgodd.2 ⊢ · ˙ = ⋅ G
3 fincygsubgodd.3 ⊢ D = B C
4 fincygsubgodd.4 ⊢ F = n ∈ ℤ ⟼ n · ˙ A
5 fincygsubgodd.5 ⊢ H = n ∈ ℤ ⟼ n · ˙ C · ˙ A
6 fincygsubgodd.6 ⊢ φ → G ∈ Grp
7 fincygsubgodd.7 ⊢ φ → A ∈ B
8 fincygsubgodd.8 ⊢ φ → ran ⁡ F = B
9 fincygsubgodd.9 ⊢ φ → C ∥ B
10 fincygsubgodd.10 ⊢ φ → B ∈ Fin
11 fincygsubgodd.11 ⊢ φ → C ∈ ℕ
12 eqid ⊢ od ⁡ G = od ⁡ G
13 4 rneqi ⊢ ran ⁡ F = ran ⁡ n ∈ ℤ ⟼ n · ˙ A
14 13 8 syl5reqr ⊢ φ → B = ran ⁡ n ∈ ℤ ⟼ n · ˙ A
15 1 2 12 6 7 14 cycsubggenodd ⊢ φ → od ⁡ G ⁡ A = if B ∈ Fin B 0
16 10 iftrued ⊢ φ → if B ∈ Fin B 0 = B
17 15 16 eqtrd ⊢ φ → od ⁡ G ⁡ A = B
18 17 oveq1d ⊢ φ → od ⁡ G ⁡ A C = B C
19 11 nnzd ⊢ φ → C ∈ ℤ
20 1 12 2 odmulg ⊢ G ∈ Grp ∧ A ∈ B ∧ C ∈ ℤ → od ⁡ G ⁡ A = C gcd od ⁡ G ⁡ A ⁢ od ⁡ G ⁡ C · ˙ A
21 6 7 19 20 syl3anc ⊢ φ → od ⁡ G ⁡ A = C gcd od ⁡ G ⁡ A ⁢ od ⁡ G ⁡ C · ˙ A
22 1 12 odcl ⊢ A ∈ B → od ⁡ G ⁡ A ∈ ℕ 0
23 nn0z ⊢ od ⁡ G ⁡ A ∈ ℕ 0 → od ⁡ G ⁡ A ∈ ℤ
24 7 22 23 3syl ⊢ φ → od ⁡ G ⁡ A ∈ ℤ
25 9 17 breqtrrd ⊢ φ → C ∥ od ⁡ G ⁡ A
26 11 24 25 dvdsgcdidd ⊢ φ → C gcd od ⁡ G ⁡ A = C
27 26 oveq1d ⊢ φ → C gcd od ⁡ G ⁡ A ⁢ od ⁡ G ⁡ C · ˙ A = C ⁢ od ⁡ G ⁡ C · ˙ A
28 21 27 eqtrd ⊢ φ → od ⁡ G ⁡ A = C ⁢ od ⁡ G ⁡ C · ˙ A
29 1 12 7 odcld ⊢ φ → od ⁡ G ⁡ A ∈ ℕ 0
30 29 nn0cnd ⊢ φ → od ⁡ G ⁡ A ∈ ℂ
31 1 2 6 19 7 mulgcld ⊢ φ → C · ˙ A ∈ B
32 1 12 31 odcld ⊢ φ → od ⁡ G ⁡ C · ˙ A ∈ ℕ 0
33 32 nn0cnd ⊢ φ → od ⁡ G ⁡ C · ˙ A ∈ ℂ
34 19 zcnd ⊢ φ → C ∈ ℂ
35 11 nnne0d ⊢ φ → C ≠ 0
36 30 33 34 35 divmul2d ⊢ φ → od ⁡ G ⁡ A C = od ⁡ G ⁡ C · ˙ A ↔ od ⁡ G ⁡ A = C ⁢ od ⁡ G ⁡ C · ˙ A
37 28 36 mpbird ⊢ φ → od ⁡ G ⁡ A C = od ⁡ G ⁡ C · ˙ A
38 18 37 eqtr3d ⊢ φ → B C = od ⁡ G ⁡ C · ˙ A
39 3 38 syl5eq ⊢ φ → D = od ⁡ G ⁡ C · ˙ A
40 5 rneqi ⊢ ran ⁡ H = ran ⁡ n ∈ ℤ ⟼ n · ˙ C · ˙ A
41 40 a1i ⊢ φ → ran ⁡ H = ran ⁡ n ∈ ℤ ⟼ n · ˙ C · ˙ A
42 1 2 12 6 31 41 cycsubggenodd ⊢ φ → od ⁡ G ⁡ C · ˙ A = if ran ⁡ H ∈ Fin ran ⁡ H 0
43 39 42 eqtrd ⊢ φ → D = if ran ⁡ H ∈ Fin ran ⁡ H 0
44 iffalse ⊢ ¬ ran ⁡ H ∈ Fin → if ran ⁡ H ∈ Fin ran ⁡ H 0 = 0
45 43 44 sylan9eq ⊢ φ ∧ ¬ ran ⁡ H ∈ Fin → D = 0
46 3 a1i ⊢ φ → D = B C
47 hashcl ⊢ B ∈ Fin → B ∈ ℕ 0
48 nn0cn ⊢ B ∈ ℕ 0 → B ∈ ℂ
49 10 47 48 3syl ⊢ φ → B ∈ ℂ
50 7 10 hashelne0d ⊢ φ → ¬ B = 0
51 50 neqned ⊢ φ → B ≠ 0
52 49 34 51 35 divne0d ⊢ φ → B C ≠ 0
53 46 52 eqnetrd ⊢ φ → D ≠ 0
54 53 neneqd ⊢ φ → ¬ D = 0
55 54 adantr ⊢ φ ∧ ¬ ran ⁡ H ∈ Fin → ¬ D = 0
56 45 55 condan ⊢ φ → ran ⁡ H ∈ Fin
57 56 iftrued ⊢ φ → if ran ⁡ H ∈ Fin ran ⁡ H 0 = ran ⁡ H
58 39 42 57 3eqtrrd ⊢ φ → ran ⁡ H = D