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	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
	proot1mul.o	$⊢ O = od (G)$
	proot1mul.k	$⊢ K = mrCls (SubGrp (G))$
Assertion	proot1mul	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to X \in K (\{Y\})$

Proof

Step	Hyp	Ref	Expression
1		idomsubgmo.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
2		proot1mul.o	$⊢ O = od (G)$
3		proot1mul.k	$⊢ K = mrCls (SubGrp (G))$
4		simpll	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to R \in IDomn$
5		isidom	$⊢ R \in IDomn \leftrightarrow (R \in CRing \land R \in Domn)$
6	5	simprbi	$⊢ R \in IDomn \to R \in Domn$
7		domnring	$⊢ R \in Domn \to R \in Ring$
8		eqid	$⊢ Unit (R) = Unit (R)$
9	8 1	unitgrp	$⊢ R \in Ring \to G \in Grp$
10	4 6 7 9	4syl	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to G \in Grp$
11		eqid	$⊢ {Base}_{G} = {Base}_{G}$
12	11	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
13		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
14	10 12 13	3syl	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to SubGrp (G) \in Moore ({Base}_{G})$
15		simprl	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to X \in O^{-1} [\{N\}]$
16	11 2	odf	$⊢ O : {Base}_{G} ⟶ ℕ_{0}$
17		ffn	$⊢ O : {Base}_{G} ⟶ ℕ_{0} \to O Fn {Base}_{G}$
18		fniniseg	$⊢ O Fn {Base}_{G} \to (X \in O^{-1} [\{N\}] \leftrightarrow (X \in {Base}_{G} \land O (X) = N))$
19	16 17 18	mp2b	$⊢ X \in O^{-1} [\{N\}] \leftrightarrow (X \in {Base}_{G} \land O (X) = N)$
20	15 19	sylib	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to (X \in {Base}_{G} \land O (X) = N)$
21	20	simpld	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to X \in {Base}_{G}$
22	21	snssd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to \{X\} \subseteq {Base}_{G}$
23	14 3 22	mrcssidd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to \{X\} \subseteq K (\{X\})$
24		snssg	$⊢ X \in O^{-1} [\{N\}] \to (X \in K (\{X\}) \leftrightarrow \{X\} \subseteq K (\{X\}))$
25	15 24	syl	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to (X \in K (\{X\}) \leftrightarrow \{X\} \subseteq K (\{X\}))$
26	23 25	mpbird	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to X \in K (\{X\})$
27	1	idomsubgmo	$⊢ (R \in IDomn \land N \in ℕ) \to \exists^{*} x \in SubGrp (G) \|x\| = N$
28	27	adantr	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to \exists^{*} x \in SubGrp (G) \|x\| = N$
29	3	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land \{X\} \subseteq {Base}_{G}) \to K (\{X\}) \in SubGrp (G)$
30	14 22 29	syl2anc	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to K (\{X\}) \in SubGrp (G)$
31	20	simprd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to O (X) = N$
32		simplr	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to N \in ℕ$
33	31 32	eqeltrd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to O (X) \in ℕ$
34	11 2 3	odhash2	$⊢ (G \in Grp \land X \in {Base}_{G} \land O (X) \in ℕ) \to \|K (\{X\})\| = O (X)$
35	10 21 33 34	syl3anc	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to \|K (\{X\})\| = O (X)$
36	35 31	eqtrd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to \|K (\{X\})\| = N$
37		simprr	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to Y \in O^{-1} [\{N\}]$
38		fniniseg	$⊢ O Fn {Base}_{G} \to (Y \in O^{-1} [\{N\}] \leftrightarrow (Y \in {Base}_{G} \land O (Y) = N))$
39	16 17 38	mp2b	$⊢ Y \in O^{-1} [\{N\}] \leftrightarrow (Y \in {Base}_{G} \land O (Y) = N)$
40	37 39	sylib	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to (Y \in {Base}_{G} \land O (Y) = N)$
41	40	simpld	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to Y \in {Base}_{G}$
42	41	snssd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to \{Y\} \subseteq {Base}_{G}$
43	3	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land \{Y\} \subseteq {Base}_{G}) \to K (\{Y\}) \in SubGrp (G)$
44	14 42 43	syl2anc	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to K (\{Y\}) \in SubGrp (G)$
45	40	simprd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to O (Y) = N$
46	45 32	eqeltrd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to O (Y) \in ℕ$
47	11 2 3	odhash2	$⊢ (G \in Grp \land Y \in {Base}_{G} \land O (Y) \in ℕ) \to \|K (\{Y\})\| = O (Y)$
48	10 41 46 47	syl3anc	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to \|K (\{Y\})\| = O (Y)$
49	48 45	eqtrd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to \|K (\{Y\})\| = N$
50		fveqeq2	$⊢ x = K (\{X\}) \to (\|x\| = N \leftrightarrow \|K (\{X\})\| = N)$
51		fveqeq2	$⊢ x = K (\{Y\}) \to (\|x\| = N \leftrightarrow \|K (\{Y\})\| = N)$
52	50 51	rmoi	$⊢ (\exists^{*} x \in SubGrp (G) \|x\| = N \land (K (\{X\}) \in SubGrp (G) \land \|K (\{X\})\| = N) \land (K (\{Y\}) \in SubGrp (G) \land \|K (\{Y\})\| = N)) \to K (\{X\}) = K (\{Y\})$
53	28 30 36 44 49 52	syl122anc	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to K (\{X\}) = K (\{Y\})$
54	26 53	eleqtrd	$⊢ ((R \in IDomn \land N \in ℕ) \land (X \in O^{-1} [\{N\}] \land Y \in O^{-1} [\{N\}])) \to X \in K (\{Y\})$

Metamath Proof Explorer

Theorem proot1mul

Proof