Metamath Proof Explorer

Theorem fincygsubgodexd

Description: A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses fincygsubgodexd.1 
|- B = ( Base ` G )
fincygsubgodexd.2 
|- ( ph -> G e. CycGrp )
fincygsubgodexd.3 
|- ( ph -> C || ( # ` B ) )
fincygsubgodexd.4 
|- ( ph -> B e. Fin )
fincygsubgodexd.5 
|- ( ph -> C e. NN )
Assertion fincygsubgodexd 
|- ( ph -> E. x e. ( SubGrp ` G ) ( # ` x ) = C )

Proof

Step Hyp Ref Expression
1 fincygsubgodexd.1 
 |-  B = ( Base ` G )
2 fincygsubgodexd.2 
 |-  ( ph -> G e. CycGrp )
3 fincygsubgodexd.3 
 |-  ( ph -> C || ( # ` B ) )
4 fincygsubgodexd.4 
 |-  ( ph -> B e. Fin )
5 fincygsubgodexd.5 
 |-  ( ph -> C e. NN )
6 eqid 
 |-  ( .g ` G ) = ( .g ` G )
7 1 6 iscyg 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ E. y e. B ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) )
8 7 simprbi 
 |-  ( G e. CycGrp -> E. y e. B ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B )
9 2 8 syl 
 |-  ( ph -> E. y e. B ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B )
10 eqid 
 |-  ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) = ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) )
11 cyggrp 
 |-  ( G e. CycGrp -> G e. Grp )
12 2 11 syl 
 |-  ( ph -> G e. Grp )
13 12 adantr 
 |-  ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) -> G e. Grp )
14 simprl 
 |-  ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) -> y e. B )
15 1 12 4 hashfingrpnn 
 |-  ( ph -> ( # ` B ) e. NN )
16 nndivdvds 
 |-  ( ( ( # ` B ) e. NN /\ C e. NN ) -> ( C || ( # ` B ) <-> ( ( # ` B ) / C ) e. NN ) )
17 15 5 16 syl2anc 
 |-  ( ph -> ( C || ( # ` B ) <-> ( ( # ` B ) / C ) e. NN ) )
18 3 17 mpbid 
 |-  ( ph -> ( ( # ` B ) / C ) e. NN )
19 18 adantr 
 |-  ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) -> ( ( # ` B ) / C ) e. NN )
20 1 6 10 13 14 19 fincygsubgd 
 |-  ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) -> ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) e. ( SubGrp ` G ) )
21 simpr 
 |-  ( ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) /\ x = ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) ) -> x = ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) )
22 21 fveq2d 
 |-  ( ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) /\ x = ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) ) -> ( # ` x ) = ( # ` ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) ) )
23 eqid 
 |-  ( ( # ` B ) / ( ( # ` B ) / C ) ) = ( ( # ` B ) / ( ( # ` B ) / C ) )
24 eqid 
 |-  ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = ( n e. ZZ |-> ( n ( .g ` G ) y ) )
25 simprr 
 |-  ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) -> ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B )
26 5 nnne0d 
 |-  ( ph -> C =/= 0 )
27 divconjdvds 
 |-  ( ( C || ( # ` B ) /\ C =/= 0 ) -> ( ( # ` B ) / C ) || ( # ` B ) )
28 3 26 27 syl2anc 
 |-  ( ph -> ( ( # ` B ) / C ) || ( # ` B ) )
29 28 adantr 
 |-  ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) -> ( ( # ` B ) / C ) || ( # ` B ) )
30 4 adantr 
 |-  ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) -> B e. Fin )
31 1 6 23 24 10 13 14 25 29 30 19 fincygsubgodd 
 |-  ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) -> ( # ` ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) ) = ( ( # ` B ) / ( ( # ` B ) / C ) ) )
32 31 adantr 
 |-  ( ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) /\ x = ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) ) -> ( # ` ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) ) = ( ( # ` B ) / ( ( # ` B ) / C ) ) )
33 15 nncnd 
 |-  ( ph -> ( # ` B ) e. CC )
34 5 nncnd 
 |-  ( ph -> C e. CC )
35 15 nnne0d 
 |-  ( ph -> ( # ` B ) =/= 0 )
36 33 34 35 26 ddcand 
 |-  ( ph -> ( ( # ` B ) / ( ( # ` B ) / C ) ) = C )
37 36 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) /\ x = ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) ) -> ( ( # ` B ) / ( ( # ` B ) / C ) ) = C )
38 22 32 37 3eqtrd 
 |-  ( ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) /\ x = ran ( n e. ZZ |-> ( n ( .g ` G ) ( ( ( # ` B ) / C ) ( .g ` G ) y ) ) ) ) -> ( # ` x ) = C )
39 20 38 rspcedeq1vd 
 |-  ( ( ph /\ ( y e. B /\ ran ( n e. ZZ |-> ( n ( .g ` G ) y ) ) = B ) ) -> E. x e. ( SubGrp ` G ) ( # ` x ) = C )
40 9 39 rexlimddv 
 |-  ( ph -> E. x e. ( SubGrp ` G ) ( # ` x ) = C )