Metamath Proof Explorer

Theorem cycsubggenodd

Description: Relationship between the order of a subgroup and the order of a generator of the subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses cycsubggenodd.1 ⊢ B = Base G
cycsubggenodd.2 ⊢ · ˙ = ⋅ G
cycsubggenodd.3 ⊢ O = od ⁡ G
cycsubggenodd.4 ⊢ φ → G ∈ Grp
cycsubggenodd.5 ⊢ φ → A ∈ B
cycsubggenodd.6 ⊢ φ → C = ran ⁡ n ∈ ℤ ⟼ n · ˙ A
Assertion cycsubggenodd ⊢ φ → O ⁡ A = if C ∈ Fin C 0

Proof

Step Hyp Ref Expression
1 cycsubggenodd.1 ⊢ B = Base G
2 cycsubggenodd.2 ⊢ · ˙ = ⋅ G
3 cycsubggenodd.3 ⊢ O = od ⁡ G
4 cycsubggenodd.4 ⊢ φ → G ∈ Grp
5 cycsubggenodd.5 ⊢ φ → A ∈ B
6 cycsubggenodd.6 ⊢ φ → C = ran ⁡ n ∈ ℤ ⟼ n · ˙ A
7 eqid ⊢ n ∈ ℤ ⟼ n · ˙ A = n ∈ ℤ ⟼ n · ˙ A
8 1 3 2 7 dfod2 ⊢ G ∈ Grp ∧ A ∈ B → O ⁡ A = if ran ⁡ n ∈ ℤ ⟼ n · ˙ A ∈ Fin ran ⁡ n ∈ ℤ ⟼ n · ˙ A 0
9 4 5 8 syl2anc ⊢ φ → O ⁡ A = if ran ⁡ n ∈ ℤ ⟼ n · ˙ A ∈ Fin ran ⁡ n ∈ ℤ ⟼ n · ˙ A 0
10 6 eqcomd ⊢ φ → ran ⁡ n ∈ ℤ ⟼ n · ˙ A = C
11 10 eleq1d ⊢ φ → ran ⁡ n ∈ ℤ ⟼ n · ˙ A ∈ Fin ↔ C ∈ Fin
12 10 fveq2d ⊢ φ → ran ⁡ n ∈ ℤ ⟼ n · ˙ A = C
13 11 12 ifbieq1d ⊢ φ → if ran ⁡ n ∈ ℤ ⟼ n · ˙ A ∈ Fin ran ⁡ n ∈ ℤ ⟼ n · ˙ A 0 = if C ∈ Fin C 0
14 9 13 eqtrd ⊢ φ → O ⁡ A = if C ∈ Fin C 0