This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )