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 ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
proot1hash.o ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion proot1hash ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( ♯ ‘ ( ◡ 𝑂 “ { 𝑁 } ) ) = ( ϕ ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 proot1hash.g ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
2 proot1hash.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 3 2 odf ⊢ 𝑂 : ( Base ‘ 𝐺 ) ⟶ ℕ0
5 ffn ⊢ ( 𝑂 : ( Base ‘ 𝐺 ) ⟶ ℕ0 → 𝑂 Fn ( Base ‘ 𝐺 ) )
6 fniniseg2 ⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( ◡ 𝑂 “ { 𝑁 } ) = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } )
7 4 5 6 mp2b ⊢ ( ◡ 𝑂 “ { 𝑁 } ) = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 }
8 simp3 ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) )
9 fniniseg ⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↔ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑋 ) = 𝑁 ) ) )
10 4 5 9 mp2b ⊢ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↔ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑋 ) = 𝑁 ) )
11 8 10 sylib ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑋 ) = 𝑁 ) )
12 11 simprd ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( 𝑂 ‘ 𝑋 ) = 𝑁 )
13 12 eqeq2d ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ 𝑥 ) = 𝑁 ) )
14 13 rabbidv ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → { 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑋 ) } = { 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } )
15 isidom ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
16 15 simprbi ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Domn )
17 16 3ad2ant1 ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝑅 ∈ Domn )
18 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
19 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
20 19 1 unitgrp ⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Grp )
21 17 18 20 3syl ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝐺 ∈ Grp )
22 3 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
23 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
24 21 22 23 3syl ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
25 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
26 25 mrcssv ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ⊆ ( Base ‘ 𝐺 ) )
27 dfrab3ss ⊢ ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ⊆ ( Base ‘ 𝐺 ) → { 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } = ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∩ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } ) )
28 24 26 27 3syl ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → { 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } = ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∩ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } ) )
29 incom ⊢ ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∩ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } ) = ( { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) )
30 simpl1 ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ∧ 𝑥 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝑅 ∈ IDomn )
31 simpl2 ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ∧ 𝑥 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝑁 ∈ ℕ )
32 simpr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ∧ 𝑥 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝑥 ∈ ( ◡ 𝑂 “ { 𝑁 } ) )
33 simpl3 ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ∧ 𝑥 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) )
34 1 2 25 proot1mul ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑥 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) )
35 30 31 32 33 34 syl22anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ∧ 𝑥 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) )
36 35 ex ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( 𝑥 ∈ ( ◡ 𝑂 “ { 𝑁 } ) → 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ) )
37 36 ssrdv ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( ◡ 𝑂 “ { 𝑁 } ) ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) )
38 7 37 eqsstrrid ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) )
39 df-ss ⊢ ( { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ↔ ( { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ) = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } )
40 38 39 sylib ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ) = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } )
41 29 40 syl5eq ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∩ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } ) = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } )
42 14 28 41 3eqtrrd ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ( 𝑂 ‘ 𝑥 ) = 𝑁 } = { 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑋 ) } )
43 7 42 syl5eq ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( ◡ 𝑂 “ { 𝑁 } ) = { 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑋 ) } )
44 43 fveq2d ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( ♯ ‘ ( ◡ 𝑂 “ { 𝑁 } ) ) = ( ♯ ‘ { 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑋 ) } ) )
45 11 simpld ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
46 simp2 ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → 𝑁 ∈ ℕ )
47 12 46 eqeltrd ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( 𝑂 ‘ 𝑋 ) ∈ ℕ )
48 3 2 25 odngen ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑋 ) ∈ ℕ ) → ( ♯ ‘ { 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑋 ) } ) = ( ϕ ‘ ( 𝑂 ‘ 𝑋 ) ) )
49 21 45 47 48 syl3anc ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( ♯ ‘ { 𝑥 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ { 𝑋 } ) ∣ ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑋 ) } ) = ( ϕ ‘ ( 𝑂 ‘ 𝑋 ) ) )
50 12 fveq2d ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( ϕ ‘ ( 𝑂 ‘ 𝑋 ) ) = ( ϕ ‘ 𝑁 ) )
51 44 49 50 3eqtrd ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) → ( ♯ ‘ ( ◡ 𝑂 “ { 𝑁 } ) ) = ( ϕ ‘ 𝑁 ) )