Metamath Proof Explorer

Theorem proot1hash

Description: If an integral domain has a primitive N -th root of unity, it has exactly ( phiN ) of them. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses proot1hash.g 
|- G = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
proot1hash.o 
|- O = ( od ` G )
Assertion proot1hash 
|- ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( # ` ( `' O " { N } ) ) = ( phi ` N ) )

Proof

Step Hyp Ref Expression
1 proot1hash.g 
 |-  G = ( ( mulGrp ` R ) |`s ( Unit ` R ) )
2 proot1hash.o 
 |-  O = ( od ` G )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 3 2 odf 
 |-  O : ( Base ` G ) --> NN0
5 ffn 
 |-  ( O : ( Base ` G ) --> NN0 -> O Fn ( Base ` G ) )
6 fniniseg2 
 |-  ( O Fn ( Base ` G ) -> ( `' O " { N } ) = { x e. ( Base ` G ) | ( O ` x ) = N } )
7 4 5 6 mp2b 
 |-  ( `' O " { N } ) = { x e. ( Base ` G ) | ( O ` x ) = N }
8 simp3 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> X e. ( `' O " { N } ) )
9 fniniseg 
 |-  ( O Fn ( Base ` G ) -> ( X e. ( `' O " { N } ) <-> ( X e. ( Base ` G ) /\ ( O ` X ) = N ) ) )
10 4 5 9 mp2b 
 |-  ( X e. ( `' O " { N } ) <-> ( X e. ( Base ` G ) /\ ( O ` X ) = N ) )
11 8 10 sylib 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( X e. ( Base ` G ) /\ ( O ` X ) = N ) )
12 11 simprd 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( O ` X ) = N )
13 12 eqeq2d 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( ( O ` x ) = ( O ` X ) <-> ( O ` x ) = N ) )
14 13 rabbidv 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> { x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) | ( O ` x ) = ( O ` X ) } = { x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) | ( O ` x ) = N } )
15 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
16 15 simprbi 
 |-  ( R e. IDomn -> R e. Domn )
17 16 3ad2ant1 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> R e. Domn )
18 domnring 
 |-  ( R e. Domn -> R e. Ring )
19 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
20 19 1 unitgrp 
 |-  ( R e. Ring -> G e. Grp )
21 17 18 20 3syl 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> G e. Grp )
22 3 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
23 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
24 21 22 23 3syl 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
25 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
26 25 mrcssv 
 |-  ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) C_ ( Base ` G ) )
27 dfrab3ss 
 |-  ( ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) C_ ( Base ` G ) -> { x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) | ( O ` x ) = N } = ( ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) i^i { x e. ( Base ` G ) | ( O ` x ) = N } ) )
28 24 26 27 3syl 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> { x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) | ( O ` x ) = N } = ( ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) i^i { x e. ( Base ` G ) | ( O ` x ) = N } ) )
29 incom 
 |-  ( ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) i^i { x e. ( Base ` G ) | ( O ` x ) = N } ) = ( { x e. ( Base ` G ) | ( O ` x ) = N } i^i ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) )
30 simpl1 
 |-  ( ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) /\ x e. ( `' O " { N } ) ) -> R e. IDomn )
31 simpl2 
 |-  ( ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) /\ x e. ( `' O " { N } ) ) -> N e. NN )
32 simpr 
 |-  ( ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) /\ x e. ( `' O " { N } ) ) -> x e. ( `' O " { N } ) )
33 simpl3 
 |-  ( ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) /\ x e. ( `' O " { N } ) ) -> X e. ( `' O " { N } ) )
34 1 2 25 proot1mul 
 |-  ( ( ( R e. IDomn /\ N e. NN ) /\ ( x e. ( `' O " { N } ) /\ X e. ( `' O " { N } ) ) ) -> x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) )
35 30 31 32 33 34 syl22anc 
 |-  ( ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) /\ x e. ( `' O " { N } ) ) -> x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) )
36 35 ex 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( x e. ( `' O " { N } ) -> x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) ) )
37 36 ssrdv 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( `' O " { N } ) C_ ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) )
38 7 37 eqsstrrid 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> { x e. ( Base ` G ) | ( O ` x ) = N } C_ ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) )
39 df-ss 
 |-  ( { x e. ( Base ` G ) | ( O ` x ) = N } C_ ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) <-> ( { x e. ( Base ` G ) | ( O ` x ) = N } i^i ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) ) = { x e. ( Base ` G ) | ( O ` x ) = N } )
40 38 39 sylib 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( { x e. ( Base ` G ) | ( O ` x ) = N } i^i ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) ) = { x e. ( Base ` G ) | ( O ` x ) = N } )
41 29 40 syl5eq 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) i^i { x e. ( Base ` G ) | ( O ` x ) = N } ) = { x e. ( Base ` G ) | ( O ` x ) = N } )
42 14 28 41 3eqtrrd 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> { x e. ( Base ` G ) | ( O ` x ) = N } = { x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) | ( O ` x ) = ( O ` X ) } )
43 7 42 syl5eq 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( `' O " { N } ) = { x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) | ( O ` x ) = ( O ` X ) } )
44 43 fveq2d 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( # ` ( `' O " { N } ) ) = ( # ` { x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) | ( O ` x ) = ( O ` X ) } ) )
45 11 simpld 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> X e. ( Base ` G ) )
46 simp2 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> N e. NN )
47 12 46 eqeltrd 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( O ` X ) e. NN )
48 3 2 25 odngen 
 |-  ( ( G e. Grp /\ X e. ( Base ` G ) /\ ( O ` X ) e. NN ) -> ( # ` { x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) | ( O ` x ) = ( O ` X ) } ) = ( phi ` ( O ` X ) ) )
49 21 45 47 48 syl3anc 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( # ` { x e. ( ( mrCls ` ( SubGrp ` G ) ) ` { X } ) | ( O ` x ) = ( O ` X ) } ) = ( phi ` ( O ` X ) ) )
50 12 fveq2d 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( phi ` ( O ` X ) ) = ( phi ` N ) )
51 44 49 50 3eqtrd 
 |-  ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( # ` ( `' O " { N } ) ) = ( phi ` N ) )