Metamath Proof Explorer

Theorem proot1mul

Description: Any primitive N -th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015)

Ref Expression
Hypotheses idomsubgmo.g ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
proot1mul.o ⊢ 𝑂 = ( od ‘ 𝐺 )
proot1mul.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion proot1mul ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑋 ∈ ( 𝐾 ‘ { 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 idomsubgmo.g ⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( Unit ‘ 𝑅 ) )
2 proot1mul.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 proot1mul.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
4 simpll ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑅 ∈ IDomn )
5 isidom ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
6 5 simprbi ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Domn )
7 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
8 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
9 8 1 unitgrp ⊢ ( 𝑅 ∈ Ring → 𝐺 ∈ Grp )
10 4 6 7 9 4syl ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝐺 ∈ Grp )
11 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
12 11 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
13 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
14 10 12 13 3syl ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
15 simprl ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) )
16 11 2 odf ⊢ 𝑂 : ( Base ‘ 𝐺 ) ⟶ ℕ0
17 ffn ⊢ ( 𝑂 : ( Base ‘ 𝐺 ) ⟶ ℕ0 → 𝑂 Fn ( Base ‘ 𝐺 ) )
18 fniniseg ⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↔ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑋 ) = 𝑁 ) ) )
19 16 17 18 mp2b ⊢ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↔ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑋 ) = 𝑁 ) )
20 15 19 sylib ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑋 ) = 𝑁 ) )
21 20 simpld ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
22 21 snssd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → { 𝑋 } ⊆ ( Base ‘ 𝐺 ) )
23 14 3 22 mrcssidd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
24 snssg ⊢ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) → ( 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )
25 15 24 syl ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )
26 23 25 mpbird ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) )
27 1 idomsubgmo ⊢ ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) → ∃* 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 𝑁 )
28 27 adantr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ∃* 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 𝑁 )
29 3 mrccl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ { 𝑋 } ⊆ ( Base ‘ 𝐺 ) ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) )
30 14 22 29 syl2anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) )
31 20 simprd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝑂 ‘ 𝑋 ) = 𝑁 )
32 simplr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑁 ∈ ℕ )
33 31 32 eqeltrd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝑂 ‘ 𝑋 ) ∈ ℕ )
34 11 2 3 odhash2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑋 ) ∈ ℕ ) → ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) = ( 𝑂 ‘ 𝑋 ) )
35 10 21 33 34 syl3anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) = ( 𝑂 ‘ 𝑋 ) )
36 35 31 eqtrd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) = 𝑁 )
37 simprr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) )
38 fniniseg ⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↔ ( 𝑌 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑌 ) = 𝑁 ) ) )
39 16 17 38 mp2b ⊢ ( 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↔ ( 𝑌 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑌 ) = 𝑁 ) )
40 37 39 sylib ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝑌 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑌 ) = 𝑁 ) )
41 40 simpld ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑌 ∈ ( Base ‘ 𝐺 ) )
42 41 snssd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → { 𝑌 } ⊆ ( Base ‘ 𝐺 ) )
43 3 mrccl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ { 𝑌 } ⊆ ( Base ‘ 𝐺 ) ) → ( 𝐾 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝐺 ) )
44 14 42 43 syl2anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝐾 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝐺 ) )
45 40 simprd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝑂 ‘ 𝑌 ) = 𝑁 )
46 45 32 eqeltrd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝑂 ‘ 𝑌 ) ∈ ℕ )
47 11 2 3 odhash2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑌 ) ∈ ℕ ) → ( ♯ ‘ ( 𝐾 ‘ { 𝑌 } ) ) = ( 𝑂 ‘ 𝑌 ) )
48 10 41 46 47 syl3anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( ♯ ‘ ( 𝐾 ‘ { 𝑌 } ) ) = ( 𝑂 ‘ 𝑌 ) )
49 48 45 eqtrd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( ♯ ‘ ( 𝐾 ‘ { 𝑌 } ) ) = 𝑁 )
50 fveqeq2 ⊢ ( 𝑥 = ( 𝐾 ‘ { 𝑋 } ) → ( ( ♯ ‘ 𝑥 ) = 𝑁 ↔ ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) = 𝑁 ) )
51 fveqeq2 ⊢ ( 𝑥 = ( 𝐾 ‘ { 𝑌 } ) → ( ( ♯ ‘ 𝑥 ) = 𝑁 ↔ ( ♯ ‘ ( 𝐾 ‘ { 𝑌 } ) ) = 𝑁 ) )
52 50 51 rmoi ⊢ ( ( ∃* 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑥 ) = 𝑁 ∧ ( ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) = 𝑁 ) ∧ ( ( 𝐾 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ ( 𝐾 ‘ { 𝑌 } ) ) = 𝑁 ) ) → ( 𝐾 ‘ { 𝑋 } ) = ( 𝐾 ‘ { 𝑌 } ) )
53 28 30 36 44 49 52 syl122anc ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → ( 𝐾 ‘ { 𝑋 } ) = ( 𝐾 ‘ { 𝑌 } ) )
54 26 53 eleqtrd ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑋 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ∧ 𝑌 ∈ ( ◡ 𝑂 “ { 𝑁 } ) ) ) → 𝑋 ∈ ( 𝐾 ‘ { 𝑌 } ) )