Metamath Proof Explorer

Theorem odngen

Description: A cyclic subgroup of size ( OA ) has ( phi( OA ) ) generators. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses odhash.x 
|- X = ( Base ` G )
odhash.o 
|- O = ( od ` G )
odhash.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion odngen 
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) = ( phi ` ( O ` A ) ) )

Proof

Step Hyp Ref Expression
1 odhash.x 
 |-  X = ( Base ` G )
2 odhash.o 
 |-  O = ( od ` G )
3 odhash.k 
 |-  K = ( mrCls ` ( SubGrp ` G ) )
4 eqid 
 |-  ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) = ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) )
5 4 mptpreima 
 |-  ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) " { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) = { y e. ( 0 ..^ ( O ` A ) ) | ( y ( .g ` G ) A ) e. { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } }
6 5 fveq2i 
 |-  ( # ` ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) " { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) ) = ( # ` { y e. ( 0 ..^ ( O ` A ) ) | ( y ( .g ` G ) A ) e. { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } } )
7 eqid 
 |-  ( .g ` G ) = ( .g ` G )
8 1 7 2 3 odf1o2 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) : ( 0 ..^ ( O ` A ) ) -1-1-onto-> ( K ` { A } ) )
9 f1ocnv 
 |-  ( ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) : ( 0 ..^ ( O ` A ) ) -1-1-onto-> ( K ` { A } ) -> `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) : ( K ` { A } ) -1-1-onto-> ( 0 ..^ ( O ` A ) ) )
10 f1of1 
 |-  ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) : ( K ` { A } ) -1-1-onto-> ( 0 ..^ ( O ` A ) ) -> `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) : ( K ` { A } ) -1-1-> ( 0 ..^ ( O ` A ) ) )
11 8 9 10 3syl 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) : ( K ` { A } ) -1-1-> ( 0 ..^ ( O ` A ) ) )
12 ssrab2 
 |-  { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } C_ ( K ` { A } )
13 fvex 
 |-  ( K ` { A } ) e. _V
14 13 rabex 
 |-  { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } e. _V
15 14 f1imaen 
 |-  ( ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) : ( K ` { A } ) -1-1-> ( 0 ..^ ( O ` A ) ) /\ { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } C_ ( K ` { A } ) ) -> ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) " { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) ~~ { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } )
16 hasheni 
 |-  ( ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) " { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) ~~ { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } -> ( # ` ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) " { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) ) = ( # ` { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) )
17 15 16 syl 
 |-  ( ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) : ( K ` { A } ) -1-1-> ( 0 ..^ ( O ` A ) ) /\ { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } C_ ( K ` { A } ) ) -> ( # ` ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) " { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) ) = ( # ` { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) )
18 11 12 17 sylancl 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` ( `' ( y e. ( 0 ..^ ( O ` A ) ) |-> ( y ( .g ` G ) A ) ) " { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) ) = ( # ` { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) )
19 simpl1 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) /\ y e. ( 0 ..^ ( O ` A ) ) ) -> G e. Grp )
20 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) /\ y e. ( 0 ..^ ( O ` A ) ) ) -> A e. X )
21 elfzoelz 
 |-  ( y e. ( 0 ..^ ( O ` A ) ) -> y e. ZZ )
22 21 adantl 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) /\ y e. ( 0 ..^ ( O ` A ) ) ) -> y e. ZZ )
23 1 7 3 cycsubg2cl 
 |-  ( ( G e. Grp /\ A e. X /\ y e. ZZ ) -> ( y ( .g ` G ) A ) e. ( K ` { A } ) )
24 19 20 22 23 syl3anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) /\ y e. ( 0 ..^ ( O ` A ) ) ) -> ( y ( .g ` G ) A ) e. ( K ` { A } ) )
25 fveqeq2 
 |-  ( x = ( y ( .g ` G ) A ) -> ( ( O ` x ) = ( O ` A ) <-> ( O ` ( y ( .g ` G ) A ) ) = ( O ` A ) ) )
26 25 elrab3 
 |-  ( ( y ( .g ` G ) A ) e. ( K ` { A } ) -> ( ( y ( .g ` G ) A ) e. { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } <-> ( O ` ( y ( .g ` G ) A ) ) = ( O ` A ) ) )
27 24 26 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) /\ y e. ( 0 ..^ ( O ` A ) ) ) -> ( ( y ( .g ` G ) A ) e. { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } <-> ( O ` ( y ( .g ` G ) A ) ) = ( O ` A ) ) )
28 simpl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) /\ y e. ( 0 ..^ ( O ` A ) ) ) -> ( O ` A ) e. NN )
29 1 2 7 odmulgeq 
 |-  ( ( ( G e. Grp /\ A e. X /\ y e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` ( y ( .g ` G ) A ) ) = ( O ` A ) <-> ( y gcd ( O ` A ) ) = 1 ) )
30 19 20 22 28 29 syl31anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) /\ y e. ( 0 ..^ ( O ` A ) ) ) -> ( ( O ` ( y ( .g ` G ) A ) ) = ( O ` A ) <-> ( y gcd ( O ` A ) ) = 1 ) )
31 27 30 bitrd 
 |-  ( ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) /\ y e. ( 0 ..^ ( O ` A ) ) ) -> ( ( y ( .g ` G ) A ) e. { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } <-> ( y gcd ( O ` A ) ) = 1 ) )
32 31 rabbidva 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> { y e. ( 0 ..^ ( O ` A ) ) | ( y ( .g ` G ) A ) e. { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } } = { y e. ( 0 ..^ ( O ` A ) ) | ( y gcd ( O ` A ) ) = 1 } )
33 32 fveq2d 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` { y e. ( 0 ..^ ( O ` A ) ) | ( y ( .g ` G ) A ) e. { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } } ) = ( # ` { y e. ( 0 ..^ ( O ` A ) ) | ( y gcd ( O ` A ) ) = 1 } ) )
34 dfphi2 
 |-  ( ( O ` A ) e. NN -> ( phi ` ( O ` A ) ) = ( # ` { y e. ( 0 ..^ ( O ` A ) ) | ( y gcd ( O ` A ) ) = 1 } ) )
35 34 3ad2ant3 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( phi ` ( O ` A ) ) = ( # ` { y e. ( 0 ..^ ( O ` A ) ) | ( y gcd ( O ` A ) ) = 1 } ) )
36 33 35 eqtr4d 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` { y e. ( 0 ..^ ( O ` A ) ) | ( y ( .g ` G ) A ) e. { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } } ) = ( phi ` ( O ` A ) ) )
37 6 18 36 3eqtr3a 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( # ` { x e. ( K ` { A } ) | ( O ` x ) = ( O ` A ) } ) = ( phi ` ( O ` A ) ) )