# 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}={\mathrm{Base}}_{{G}}$
cycsubggenodd.2
cycsubggenodd.3 ${⊢}{O}=\mathrm{od}\left({G}\right)$
cycsubggenodd.4 ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
cycsubggenodd.5 ${⊢}{\phi }\to {A}\in {B}$
cycsubggenodd.6
Assertion cycsubggenodd ${⊢}{\phi }\to {O}\left({A}\right)=if\left({C}\in \mathrm{Fin},\left|{C}\right|,0\right)$

### Proof

Step Hyp Ref Expression
1 cycsubggenodd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 cycsubggenodd.2
3 cycsubggenodd.3 ${⊢}{O}=\mathrm{od}\left({G}\right)$
4 cycsubggenodd.4 ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
5 cycsubggenodd.5 ${⊢}{\phi }\to {A}\in {B}$
6 cycsubggenodd.6
7 eqid
8 1 3 2 7 dfod2
9 4 5 8 syl2anc
10 6 eqcomd
11 10 eleq1d
12 10 fveq2d
13 11 12 ifbieq1d
14 9 13 eqtrd ${⊢}{\phi }\to {O}\left({A}\right)=if\left({C}\in \mathrm{Fin},\left|{C}\right|,0\right)$