# 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}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\mathrm{Unit}\left({R}\right)$
proot1hash.o ${⊢}{O}=\mathrm{od}\left({G}\right)$
Assertion proot1hash ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left|{{O}}^{-1}\left[\left\{{N}\right\}\right]\right|=\mathrm{\varphi }\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 proot1hash.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\mathrm{Unit}\left({R}\right)$
2 proot1hash.o ${⊢}{O}=\mathrm{od}\left({G}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
4 3 2 odf ${⊢}{O}:{\mathrm{Base}}_{{G}}⟶{ℕ}_{0}$
5 ffn ${⊢}{O}:{\mathrm{Base}}_{{G}}⟶{ℕ}_{0}\to {O}Fn{\mathrm{Base}}_{{G}}$
6 fniniseg2 ${⊢}{O}Fn{\mathrm{Base}}_{{G}}\to {{O}}^{-1}\left[\left\{{N}\right\}\right]=\left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}$
7 4 5 6 mp2b ${⊢}{{O}}^{-1}\left[\left\{{N}\right\}\right]=\left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}$
8 simp3 ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]$
9 fniniseg ${⊢}{O}Fn{\mathrm{Base}}_{{G}}\to \left({X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]↔\left({X}\in {\mathrm{Base}}_{{G}}\wedge {O}\left({X}\right)={N}\right)\right)$
10 4 5 9 mp2b ${⊢}{X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]↔\left({X}\in {\mathrm{Base}}_{{G}}\wedge {O}\left({X}\right)={N}\right)$
11 8 10 sylib ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left({X}\in {\mathrm{Base}}_{{G}}\wedge {O}\left({X}\right)={N}\right)$
12 11 simprd ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {O}\left({X}\right)={N}$
13 12 eqeq2d ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left({O}\left({x}\right)={O}\left({X}\right)↔{O}\left({x}\right)={N}\right)$
14 13 rabbidv ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left\{{x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)|{O}\left({x}\right)={O}\left({X}\right)\right\}=\left\{{x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)|{O}\left({x}\right)={N}\right\}$
15 isidom ${⊢}{R}\in \mathrm{IDomn}↔\left({R}\in \mathrm{CRing}\wedge {R}\in \mathrm{Domn}\right)$
16 15 simprbi ${⊢}{R}\in \mathrm{IDomn}\to {R}\in \mathrm{Domn}$
17 16 3ad2ant1 ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {R}\in \mathrm{Domn}$
18 domnring ${⊢}{R}\in \mathrm{Domn}\to {R}\in \mathrm{Ring}$
19 eqid ${⊢}\mathrm{Unit}\left({R}\right)=\mathrm{Unit}\left({R}\right)$
20 19 1 unitgrp ${⊢}{R}\in \mathrm{Ring}\to {G}\in \mathrm{Grp}$
21 17 18 20 3syl ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {G}\in \mathrm{Grp}$
22 3 subgacs ${⊢}{G}\in \mathrm{Grp}\to \mathrm{SubGrp}\left({G}\right)\in \mathrm{ACS}\left({\mathrm{Base}}_{{G}}\right)$
23 acsmre ${⊢}\mathrm{SubGrp}\left({G}\right)\in \mathrm{ACS}\left({\mathrm{Base}}_{{G}}\right)\to \mathrm{SubGrp}\left({G}\right)\in \mathrm{Moore}\left({\mathrm{Base}}_{{G}}\right)$
24 21 22 23 3syl ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \mathrm{SubGrp}\left({G}\right)\in \mathrm{Moore}\left({\mathrm{Base}}_{{G}}\right)$
25 eqid ${⊢}\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)$
26 25 mrcssv ${⊢}\mathrm{SubGrp}\left({G}\right)\in \mathrm{Moore}\left({\mathrm{Base}}_{{G}}\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)\subseteq {\mathrm{Base}}_{{G}}$
27 dfrab3ss ${⊢}\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)\subseteq {\mathrm{Base}}_{{G}}\to \left\{{x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)|{O}\left({x}\right)={N}\right\}=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)\cap \left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}$
28 24 26 27 3syl ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left\{{x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)|{O}\left({x}\right)={N}\right\}=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)\cap \left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}$
29 incom ${⊢}\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)\cap \left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}=\left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)$
30 simpl1 ${⊢}\left(\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\wedge {x}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {R}\in \mathrm{IDomn}$
31 simpl2 ${⊢}\left(\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\wedge {x}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {N}\in ℕ$
32 simpr ${⊢}\left(\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\wedge {x}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {x}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]$
33 simpl3 ${⊢}\left(\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\wedge {x}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]$
34 1 2 25 proot1mul ${⊢}\left(\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\right)\wedge \left({x}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\right)\to {x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)$
35 30 31 32 33 34 syl22anc ${⊢}\left(\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\wedge {x}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)$
36 35 ex ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left({x}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\to {x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)\right)$
37 36 ssrdv ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {{O}}^{-1}\left[\left\{{N}\right\}\right]\subseteq \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)$
38 7 37 eqsstrrid ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}\subseteq \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)$
39 df-ss ${⊢}\left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}\subseteq \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)↔\left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)=\left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}$
40 38 39 sylib ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)=\left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}$
41 29 40 syl5eq ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)\cap \left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}=\left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}$
42 14 28 41 3eqtrrd ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left\{{x}\in {\mathrm{Base}}_{{G}}|{O}\left({x}\right)={N}\right\}=\left\{{x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)|{O}\left({x}\right)={O}\left({X}\right)\right\}$
43 7 42 syl5eq ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {{O}}^{-1}\left[\left\{{N}\right\}\right]=\left\{{x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)|{O}\left({x}\right)={O}\left({X}\right)\right\}$
44 43 fveq2d ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left|{{O}}^{-1}\left[\left\{{N}\right\}\right]\right|=\left|\left\{{x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)|{O}\left({x}\right)={O}\left({X}\right)\right\}\right|$
45 11 simpld ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {X}\in {\mathrm{Base}}_{{G}}$
46 simp2 ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {N}\in ℕ$
47 12 46 eqeltrd ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to {O}\left({X}\right)\in ℕ$
48 3 2 25 odngen ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {\mathrm{Base}}_{{G}}\wedge {O}\left({X}\right)\in ℕ\right)\to \left|\left\{{x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)|{O}\left({x}\right)={O}\left({X}\right)\right\}\right|=\mathrm{\varphi }\left({O}\left({X}\right)\right)$
49 21 45 47 48 syl3anc ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left|\left\{{x}\in \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\left\{{X}\right\}\right)|{O}\left({x}\right)={O}\left({X}\right)\right\}\right|=\mathrm{\varphi }\left({O}\left({X}\right)\right)$
50 12 fveq2d ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \mathrm{\varphi }\left({O}\left({X}\right)\right)=\mathrm{\varphi }\left({N}\right)$
51 44 49 50 3eqtrd ${⊢}\left({R}\in \mathrm{IDomn}\wedge {N}\in ℕ\wedge {X}\in {{O}}^{-1}\left[\left\{{N}\right\}\right]\right)\to \left|{{O}}^{-1}\left[\left\{{N}\right\}\right]\right|=\mathrm{\varphi }\left({N}\right)$