Theorem cyggenod2

Description: In an infinite cyclic group, the generator must have infinite order, but this property no longer characterizes the generators. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	iscyg.1	|- B = ( Base ` G )
	iscyg.2	|- .x. = ( .g ` G )
	iscyg3.e	|- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
	cyggenod.o	|- O = ( od ` G )
Assertion	cyggenod2	|- ( ( G e. Grp /\ X e. E ) -> ( O ` X ) = if ( B e. Fin , ( # ` B ) , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		iscyg.1	|- B = ( Base ` G )
2		iscyg.2	|- .x. = ( .g ` G )
3		iscyg3.e	|- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
4		cyggenod.o	|- O = ( od ` G )
5	1 2 3	iscyggen	|- ( X e. E <-> ( X e. B /\ ran ( n e. ZZ |-> ( n .x. X ) ) = B ) )
6	5	simplbi	|- ( X e. E -> X e. B )
7		eqid	|- ( n e. ZZ |-> ( n .x. X ) ) = ( n e. ZZ |-> ( n .x. X ) )
8	1 4 2 7	dfod2	|- ( ( G e. Grp /\ X e. B ) -> ( O ` X ) = if ( ran ( n e. ZZ |-> ( n .x. X ) ) e. Fin , ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) , 0 ) )
9	6 8	sylan2	|- ( ( G e. Grp /\ X e. E ) -> ( O ` X ) = if ( ran ( n e. ZZ |-> ( n .x. X ) ) e. Fin , ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) , 0 ) )
10	5	simprbi	|- ( X e. E -> ran ( n e. ZZ |-> ( n .x. X ) ) = B )
11	10	adantl	|- ( ( G e. Grp /\ X e. E ) -> ran ( n e. ZZ |-> ( n .x. X ) ) = B )
12	11	eleq1d	|- ( ( G e. Grp /\ X e. E ) -> ( ran ( n e. ZZ |-> ( n .x. X ) ) e. Fin <-> B e. Fin ) )
13	11	fveq2d	|- ( ( G e. Grp /\ X e. E ) -> ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) = ( # ` B ) )
14	12 13	ifbieq1d	|- ( ( G e. Grp /\ X e. E ) -> if ( ran ( n e. ZZ |-> ( n .x. X ) ) e. Fin , ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) , 0 ) = if ( B e. Fin , ( # ` B ) , 0 ) )
15	9 14	eqtrd	|- ( ( G e. Grp /\ X e. E ) -> ( O ` X ) = if ( B e. Fin , ( # ` B ) , 0 ) )