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	|- .x. = ( .g ` G )
	cycsubggenodd.3	|- O = ( od ` G )
	cycsubggenodd.4	|- ( ph -> G e. Grp )
	cycsubggenodd.5	|- ( ph -> A e. B )
	cycsubggenodd.6	|- ( ph -> C = ran ( n e. ZZ |-> ( n .x. A ) ) )
Assertion	cycsubggenodd	|- ( ph -> ( O ` A ) = if ( C e. Fin , ( # ` C ) , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		cycsubggenodd.1	|- B = ( Base ` G )
2		cycsubggenodd.2	|- .x. = ( .g ` G )
3		cycsubggenodd.3	|- O = ( od ` G )
4		cycsubggenodd.4	|- ( ph -> G e. Grp )
5		cycsubggenodd.5	|- ( ph -> A e. B )
6		cycsubggenodd.6	|- ( ph -> C = ran ( n e. ZZ |-> ( n .x. A ) ) )
7		eqid	|- ( n e. ZZ |-> ( n .x. A ) ) = ( n e. ZZ |-> ( n .x. A ) )
8	1 3 2 7	dfod2	|- ( ( G e. Grp /\ A e. B ) -> ( O ` A ) = if ( ran ( n e. ZZ |-> ( n .x. A ) ) e. Fin , ( # ` ran ( n e. ZZ |-> ( n .x. A ) ) ) , 0 ) )
9	4 5 8	syl2anc	|- ( ph -> ( O ` A ) = if ( ran ( n e. ZZ |-> ( n .x. A ) ) e. Fin , ( # ` ran ( n e. ZZ |-> ( n .x. A ) ) ) , 0 ) )
10	6	eqcomd	|- ( ph -> ran ( n e. ZZ |-> ( n .x. A ) ) = C )
11	10	eleq1d	|- ( ph -> ( ran ( n e. ZZ |-> ( n .x. A ) ) e. Fin <-> C e. Fin ) )
12	10	fveq2d	|- ( ph -> ( # ` ran ( n e. ZZ |-> ( n .x. A ) ) ) = ( # ` C ) )
13	11 12	ifbieq1d	|- ( ph -> if ( ran ( n e. ZZ |-> ( n .x. A ) ) e. Fin , ( # ` ran ( n e. ZZ |-> ( n .x. A ) ) ) , 0 ) = if ( C e. Fin , ( # ` C ) , 0 ) )
14	9 13	eqtrd	|- ( ph -> ( O ` A ) = if ( C e. Fin , ( # ` C ) , 0 ) )