Metamath Proof Explorer

Theorem fincygsubgodd

Description: Calculate the order of a subgroup of a finite cyclic group. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses fincygsubgodd.1 
|- B = ( Base ` G )
fincygsubgodd.2 
|- .x. = ( .g ` G )
fincygsubgodd.3 
|- D = ( ( # ` B ) / C )
fincygsubgodd.4 
|- F = ( n e. ZZ |-> ( n .x. A ) )
fincygsubgodd.5 
|- H = ( n e. ZZ |-> ( n .x. ( C .x. A ) ) )
fincygsubgodd.6 
|- ( ph -> G e. Grp )
fincygsubgodd.7 
|- ( ph -> A e. B )
fincygsubgodd.8 
|- ( ph -> ran F = B )
fincygsubgodd.9 
|- ( ph -> C || ( # ` B ) )
fincygsubgodd.10 
|- ( ph -> B e. Fin )
fincygsubgodd.11 
|- ( ph -> C e. NN )
Assertion fincygsubgodd 
|- ( ph -> ( # ` ran H ) = D )

Proof

Step Hyp Ref Expression
1 fincygsubgodd.1 
 |-  B = ( Base ` G )
2 fincygsubgodd.2 
 |-  .x. = ( .g ` G )
3 fincygsubgodd.3 
 |-  D = ( ( # ` B ) / C )
4 fincygsubgodd.4 
 |-  F = ( n e. ZZ |-> ( n .x. A ) )
5 fincygsubgodd.5 
 |-  H = ( n e. ZZ |-> ( n .x. ( C .x. A ) ) )
6 fincygsubgodd.6 
 |-  ( ph -> G e. Grp )
7 fincygsubgodd.7 
 |-  ( ph -> A e. B )
8 fincygsubgodd.8 
 |-  ( ph -> ran F = B )
9 fincygsubgodd.9 
 |-  ( ph -> C || ( # ` B ) )
10 fincygsubgodd.10 
 |-  ( ph -> B e. Fin )
11 fincygsubgodd.11 
 |-  ( ph -> C e. NN )
12 eqid 
 |-  ( od ` G ) = ( od ` G )
13 4 rneqi 
 |-  ran F = ran ( n e. ZZ |-> ( n .x. A ) )
14 8 13 eqtr3di 
 |-  ( ph -> B = ran ( n e. ZZ |-> ( n .x. A ) ) )
15 1 2 12 6 7 14 cycsubggenodd 
 |-  ( ph -> ( ( od ` G ) ` A ) = if ( B e. Fin , ( # ` B ) , 0 ) )
16 10 iftrued 
 |-  ( ph -> if ( B e. Fin , ( # ` B ) , 0 ) = ( # ` B ) )
17 15 16 eqtrd 
 |-  ( ph -> ( ( od ` G ) ` A ) = ( # ` B ) )
18 17 oveq1d 
 |-  ( ph -> ( ( ( od ` G ) ` A ) / C ) = ( ( # ` B ) / C ) )
19 11 nnzd 
 |-  ( ph -> C e. ZZ )
20 1 12 2 odmulg 
 |-  ( ( G e. Grp /\ A e. B /\ C e. ZZ ) -> ( ( od ` G ) ` A ) = ( ( C gcd ( ( od ` G ) ` A ) ) x. ( ( od ` G ) ` ( C .x. A ) ) ) )
21 6 7 19 20 syl3anc 
 |-  ( ph -> ( ( od ` G ) ` A ) = ( ( C gcd ( ( od ` G ) ` A ) ) x. ( ( od ` G ) ` ( C .x. A ) ) ) )
22 1 12 odcl 
 |-  ( A e. B -> ( ( od ` G ) ` A ) e. NN0 )
23 nn0z 
 |-  ( ( ( od ` G ) ` A ) e. NN0 -> ( ( od ` G ) ` A ) e. ZZ )
24 7 22 23 3syl 
 |-  ( ph -> ( ( od ` G ) ` A ) e. ZZ )
25 9 17 breqtrrd 
 |-  ( ph -> C || ( ( od ` G ) ` A ) )
26 11 24 25 dvdsgcdidd 
 |-  ( ph -> ( C gcd ( ( od ` G ) ` A ) ) = C )
27 26 oveq1d 
 |-  ( ph -> ( ( C gcd ( ( od ` G ) ` A ) ) x. ( ( od ` G ) ` ( C .x. A ) ) ) = ( C x. ( ( od ` G ) ` ( C .x. A ) ) ) )
28 21 27 eqtrd 
 |-  ( ph -> ( ( od ` G ) ` A ) = ( C x. ( ( od ` G ) ` ( C .x. A ) ) ) )
29 1 12 7 odcld 
 |-  ( ph -> ( ( od ` G ) ` A ) e. NN0 )
30 29 nn0cnd 
 |-  ( ph -> ( ( od ` G ) ` A ) e. CC )
31 1 2 6 19 7 mulgcld 
 |-  ( ph -> ( C .x. A ) e. B )
32 1 12 31 odcld 
 |-  ( ph -> ( ( od ` G ) ` ( C .x. A ) ) e. NN0 )
33 32 nn0cnd 
 |-  ( ph -> ( ( od ` G ) ` ( C .x. A ) ) e. CC )
34 19 zcnd 
 |-  ( ph -> C e. CC )
35 11 nnne0d 
 |-  ( ph -> C =/= 0 )
36 30 33 34 35 divmul2d 
 |-  ( ph -> ( ( ( ( od ` G ) ` A ) / C ) = ( ( od ` G ) ` ( C .x. A ) ) <-> ( ( od ` G ) ` A ) = ( C x. ( ( od ` G ) ` ( C .x. A ) ) ) ) )
37 28 36 mpbird 
 |-  ( ph -> ( ( ( od ` G ) ` A ) / C ) = ( ( od ` G ) ` ( C .x. A ) ) )
38 18 37 eqtr3d 
 |-  ( ph -> ( ( # ` B ) / C ) = ( ( od ` G ) ` ( C .x. A ) ) )
39 3 38 eqtrid 
 |-  ( ph -> D = ( ( od ` G ) ` ( C .x. A ) ) )
40 5 rneqi 
 |-  ran H = ran ( n e. ZZ |-> ( n .x. ( C .x. A ) ) )
41 40 a1i 
 |-  ( ph -> ran H = ran ( n e. ZZ |-> ( n .x. ( C .x. A ) ) ) )
42 1 2 12 6 31 41 cycsubggenodd 
 |-  ( ph -> ( ( od ` G ) ` ( C .x. A ) ) = if ( ran H e. Fin , ( # ` ran H ) , 0 ) )
43 39 42 eqtrd 
 |-  ( ph -> D = if ( ran H e. Fin , ( # ` ran H ) , 0 ) )
44 iffalse 
 |-  ( -. ran H e. Fin -> if ( ran H e. Fin , ( # ` ran H ) , 0 ) = 0 )
45 43 44 sylan9eq 
 |-  ( ( ph /\ -. ran H e. Fin ) -> D = 0 )
46 3 a1i 
 |-  ( ph -> D = ( ( # ` B ) / C ) )
47 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
48 nn0cn 
 |-  ( ( # ` B ) e. NN0 -> ( # ` B ) e. CC )
49 10 47 48 3syl 
 |-  ( ph -> ( # ` B ) e. CC )
50 7 10 hashelne0d 
 |-  ( ph -> -. ( # ` B ) = 0 )
51 50 neqned 
 |-  ( ph -> ( # ` B ) =/= 0 )
52 49 34 51 35 divne0d 
 |-  ( ph -> ( ( # ` B ) / C ) =/= 0 )
53 46 52 eqnetrd 
 |-  ( ph -> D =/= 0 )
54 53 neneqd 
 |-  ( ph -> -. D = 0 )
55 54 adantr 
 |-  ( ( ph /\ -. ran H e. Fin ) -> -. D = 0 )
56 45 55 condan 
 |-  ( ph -> ran H e. Fin )
57 56 iftrued 
 |-  ( ph -> if ( ran H e. Fin , ( # ` ran H ) , 0 ) = ( # ` ran H ) )
58 39 42 57 3eqtrrd 
 |-  ( ph -> ( # ` ran H ) = D )