unitscyglem5

	Ref	Expression
Hypotheses	unitscyglem5.1	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
	unitscyglem5.2	$⊢ φ \to R \in IDomn$
	unitscyglem5.3	$⊢ φ \to {Base}_{R} \in Fin$
	unitscyglem5.4	$⊢ φ \to D \in ℕ$
	unitscyglem5.5	$⊢ φ \to D ∥ \|{Base}_{G}\|$
Assertion	unitscyglem5	$⊢ φ \to {mulGrp}_{R} PrimRoots D \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		unitscyglem5.1	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
2		unitscyglem5.2	$⊢ φ \to R \in IDomn$
3		unitscyglem5.3	$⊢ φ \to {Base}_{R} \in Fin$
4		unitscyglem5.4	$⊢ φ \to D \in ℕ$
5		unitscyglem5.5	$⊢ φ \to D ∥ \|{Base}_{G}\|$
6	4	phicld	$⊢ φ \to ϕ (D) \in ℕ$
7		eqid	$⊢ {Base}_{G} = {Base}_{G}$
8		eqid	$⊢ \cdot_{G} = \cdot_{G}$
9	2	idomringd	$⊢ φ \to R \in Ring$
10		eqid	$⊢ Unit (R) = Unit (R)$
11	10 1	unitgrp	$⊢ R \in Ring \to G \in Grp$
12	9 11	syl	$⊢ φ \to G \in Grp$
13		eqid	$⊢ {Base}_{{mulGrp}_{R}} = {Base}_{{mulGrp}_{R}}$
14	1 13	ressbasss	$⊢ {Base}_{G} \subseteq {Base}_{{mulGrp}_{R}}$
15	14	a1i	$⊢ φ \to {Base}_{G} \subseteq {Base}_{{mulGrp}_{R}}$
16		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
17		eqid	$⊢ {Base}_{R} = {Base}_{R}$
18	16 17	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
19	18	a1i	$⊢ φ \to {Base}_{R} = {Base}_{{mulGrp}_{R}}$
20	19	eqimsscd	$⊢ φ \to {Base}_{{mulGrp}_{R}} \subseteq {Base}_{R}$
21	15 20	sstrd	$⊢ φ \to {Base}_{G} \subseteq {Base}_{R}$
22	3 21	ssfid	$⊢ φ \to {Base}_{G} \in Fin$
23	18	eqcomi	$⊢ {Base}_{{mulGrp}_{R}} = {Base}_{R}$
24	23 10	unitss	$⊢ Unit (R) \subseteq {Base}_{{mulGrp}_{R}}$
25	24	a1i	$⊢ φ \to Unit (R) \subseteq {Base}_{{mulGrp}_{R}}$
26	25	adantr	$⊢ (φ \land y \in ℕ) \to Unit (R) \subseteq {Base}_{{mulGrp}_{R}}$
27	26	adantr	$⊢ ((φ \land y \in ℕ) \land z \in {Base}_{G}) \to Unit (R) \subseteq {Base}_{{mulGrp}_{R}}$
28	1 13	ressbasssg	$⊢ {Base}_{G} \subseteq Unit (R) \cap {Base}_{{mulGrp}_{R}}$
29	28	a1i	$⊢ φ \to {Base}_{G} \subseteq Unit (R) \cap {Base}_{{mulGrp}_{R}}$
30		inss1	$⊢ Unit (R) \cap {Base}_{{mulGrp}_{R}} \subseteq Unit (R)$
31	30	a1i	$⊢ φ \to Unit (R) \cap {Base}_{{mulGrp}_{R}} \subseteq Unit (R)$
32	29 31	sstrd	$⊢ φ \to {Base}_{G} \subseteq Unit (R)$
33	32	adantr	$⊢ (φ \land y \in ℕ) \to {Base}_{G} \subseteq Unit (R)$
34	33	sseld	$⊢ (φ \land y \in ℕ) \to (z \in {Base}_{G} \to z \in Unit (R))$
35	34	imp	$⊢ ((φ \land y \in ℕ) \land z \in {Base}_{G}) \to z \in Unit (R)$
36		simpr	$⊢ (φ \land y \in ℕ) \to y \in ℕ$
37	36	adantr	$⊢ ((φ \land y \in ℕ) \land z \in {Base}_{G}) \to y \in ℕ$
38	1 27 35 37	ressmulgnnd	$⊢ ((φ \land y \in ℕ) \land z \in {Base}_{G}) \to y \cdot_{G} z = y \cdot_{{mulGrp}_{R}} z$
39	38	eqeq1d	$⊢ ((φ \land y \in ℕ) \land z \in {Base}_{G}) \to (y \cdot_{G} z = 0_{G} \leftrightarrow y \cdot_{{mulGrp}_{R}} z = 0_{G})$
40	39	rabbidva	$⊢ (φ \land y \in ℕ) \to \{z \in {Base}_{G} \| y \cdot_{G} z = 0_{G}\} = \{z \in {Base}_{G} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}$
41	40	fveq2d	$⊢ (φ \land y \in ℕ) \to \|\{z \in {Base}_{G} \| y \cdot_{G} z = 0_{G}\}\| = \|\{z \in {Base}_{G} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\|$
42		fvex	$⊢ {Base}_{G} \in V$
43	42	rabex	$⊢ \{z \in {Base}_{G} \| y \cdot_{G} z = 0_{G}\} \in V$
44	43	a1i	$⊢ (φ \land y \in ℕ) \to \{z \in {Base}_{G} \| y \cdot_{G} z = 0_{G}\} \in V$
45		hashxrcl	$⊢ \{z \in {Base}_{G} \| y \cdot_{G} z = 0_{G}\} \in V \to \|\{z \in {Base}_{G} \| y \cdot_{G} z = 0_{G}\}\| \in ℝ^{*}$
46	44 45	syl	$⊢ (φ \land y \in ℕ) \to \|\{z \in {Base}_{G} \| y \cdot_{G} z = 0_{G}\}\| \in ℝ^{*}$
47	41 46	eqeltrrd	$⊢ (φ \land y \in ℕ) \to \|\{z \in {Base}_{G} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\| \in ℝ^{*}$
48		fvex	$⊢ {Base}_{R} \in V$
49	48	rabex	$⊢ \{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\} \in V$
50	49	a1i	$⊢ (φ \land y \in ℕ) \to \{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\} \in V$
51		hashxrcl	$⊢ \{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\} \in V \to \|\{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\| \in ℝ^{*}$
52	50 51	syl	$⊢ (φ \land y \in ℕ) \to \|\{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\| \in ℝ^{*}$
53		nnre	$⊢ y \in ℕ \to y \in ℝ$
54	53	adantl	$⊢ (φ \land y \in ℕ) \to y \in ℝ$
55	54	rexrd	$⊢ (φ \land y \in ℕ) \to y \in ℝ^{*}$
56		simprl	$⊢ ((φ \land y \in ℕ) \land (z \in {Base}_{G} \land y \cdot_{{mulGrp}_{R}} z = 0_{G})) \to z \in {Base}_{G}$
57	21	ad2antrr	$⊢ ((φ \land y \in ℕ) \land (z \in {Base}_{G} \land y \cdot_{{mulGrp}_{R}} z = 0_{G})) \to {Base}_{G} \subseteq {Base}_{R}$
58	57	sseld	$⊢ ((φ \land y \in ℕ) \land (z \in {Base}_{G} \land y \cdot_{{mulGrp}_{R}} z = 0_{G})) \to (z \in {Base}_{G} \to z \in {Base}_{R})$
59	56 58	mpd	$⊢ ((φ \land y \in ℕ) \land (z \in {Base}_{G} \land y \cdot_{{mulGrp}_{R}} z = 0_{G})) \to z \in {Base}_{R}$
60	59	rabss3d	$⊢ (φ \land y \in ℕ) \to \{z \in {Base}_{G} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\} \subseteq \{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}$
61	50 60	jca	$⊢ (φ \land y \in ℕ) \to (\{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\} \in V \land \{z \in {Base}_{G} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\} \subseteq \{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\})$
62		hashss	$⊢ (\{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\} \in V \land \{z \in {Base}_{G} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\} \subseteq \{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}) \to \|\{z \in {Base}_{G} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\| \leq \|\{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\|$
63	61 62	syl	$⊢ (φ \land y \in ℕ) \to \|\{z \in {Base}_{G} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\| \leq \|\{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\|$
64	2	adantr	$⊢ (φ \land y \in ℕ) \to R \in IDomn$
65		eqid	$⊢ 1_{R} = 1_{R}$
66	10 1 65	unitgrpid	$⊢ R \in Ring \to 1_{R} = 0_{G}$
67	9 66	syl	$⊢ φ \to 1_{R} = 0_{G}$
68	67	eqcomd	$⊢ φ \to 0_{G} = 1_{R}$
69	17 65	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
70	9 69	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
71	68 70	eqeltrd	$⊢ φ \to 0_{G} \in {Base}_{R}$
72	71	adantr	$⊢ (φ \land y \in ℕ) \to 0_{G} \in {Base}_{R}$
73		eqid	$⊢ \cdot_{{mulGrp}_{R}} = \cdot_{{mulGrp}_{R}}$
74	17 73	idomrootle	$⊢ (R \in IDomn \land 0_{G} \in {Base}_{R} \land y \in ℕ) \to \|\{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\| \leq y$
75	64 72 36 74	syl3anc	$⊢ (φ \land y \in ℕ) \to \|\{z \in {Base}_{R} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\| \leq y$
76	47 52 55 63 75	xrletrd	$⊢ (φ \land y \in ℕ) \to \|\{z \in {Base}_{G} \| y \cdot_{{mulGrp}_{R}} z = 0_{G}\}\| \leq y$
77	41 76	eqbrtrd	$⊢ (φ \land y \in ℕ) \to \|\{z \in {Base}_{G} \| y \cdot_{G} z = 0_{G}\}\| \leq y$
78	77	ralrimiva	$⊢ φ \to \forall y \in ℕ \|\{z \in {Base}_{G} \| y \cdot_{G} z = 0_{G}\}\| \leq y$
79	7 8 12 22 78 4 5	unitscyglem4	$⊢ φ \to \|\{w \in {Base}_{G} \| od (G) (w) = D\}\| = ϕ (D)$
80	79	eleq1d	$⊢ φ \to (\|\{w \in {Base}_{G} \| od (G) (w) = D\}\| \in ℕ \leftrightarrow ϕ (D) \in ℕ)$
81	6 80	mpbird	$⊢ φ \to \|\{w \in {Base}_{G} \| od (G) (w) = D\}\| \in ℕ$
82	81	nngt0d	$⊢ φ \to 0 < \|\{w \in {Base}_{G} \| od (G) (w) = D\}\|$
83	42	rabex	$⊢ \{w \in {Base}_{G} \| od (G) (w) = D\} \in V$
84	83	a1i	$⊢ φ \to \{w \in {Base}_{G} \| od (G) (w) = D\} \in V$
85		hashneq0	$⊢ \{w \in {Base}_{G} \| od (G) (w) = D\} \in V \to (0 < \|\{w \in {Base}_{G} \| od (G) (w) = D\}\| \leftrightarrow \{w \in {Base}_{G} \| od (G) (w) = D\} \neq \emptyset)$
86	84 85	syl	$⊢ φ \to (0 < \|\{w \in {Base}_{G} \| od (G) (w) = D\}\| \leftrightarrow \{w \in {Base}_{G} \| od (G) (w) = D\} \neq \emptyset)$
87	82 86	mpbid	$⊢ φ \to \{w \in {Base}_{G} \| od (G) (w) = D\} \neq \emptyset$
88		n0	$⊢ \{w \in {Base}_{G} \| od (G) (w) = D\} \neq \emptyset \leftrightarrow \exists m m \in \{w \in {Base}_{G} \| od (G) (w) = D\}$
89	87 88	sylib	$⊢ φ \to \exists m m \in \{w \in {Base}_{G} \| od (G) (w) = D\}$
90		nfv	$⊢ Ⅎ m φ$
91		fveqeq2	$⊢ w = m \to (od (G) (w) = D \leftrightarrow od (G) (m) = D)$
92	91	elrab	$⊢ m \in \{w \in {Base}_{G} \| od (G) (w) = D\} \leftrightarrow (m \in {Base}_{G} \land od (G) (m) = D)$
93	92	biimpi	$⊢ m \in \{w \in {Base}_{G} \| od (G) (w) = D\} \to (m \in {Base}_{G} \land od (G) (m) = D)$
94	93	adantl	$⊢ (φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \to (m \in {Base}_{G} \land od (G) (m) = D)$
95		simpll	$⊢ ((φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \land (m \in {Base}_{G} \land od (G) (m) = D)) \to φ$
96		simprl	$⊢ ((φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \land (m \in {Base}_{G} \land od (G) (m) = D)) \to m \in {Base}_{G}$
97		simprr	$⊢ ((φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \land (m \in {Base}_{G} \land od (G) (m) = D)) \to od (G) (m) = D$
98	95 96 97	jca31	$⊢ ((φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \land (m \in {Base}_{G} \land od (G) (m) = D)) \to ((φ \land m \in {Base}_{G}) \land od (G) (m) = D)$
99	2	idomcringd	$⊢ φ \to R \in CRing$
100	16	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
101	99 100	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
102	101	ad2antrr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to {mulGrp}_{R} \in CMnd$
103	4	ad2antrr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \in ℕ$
104	15	sselda	$⊢ (φ \land m \in {Base}_{G}) \to m \in {Base}_{{mulGrp}_{R}}$
105	104	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in {Base}_{{mulGrp}_{R}}$
106	9	ad2antrr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to R \in Ring$
107	10 16	unitsubm	$⊢ R \in Ring \to Unit (R) \in SubMnd ({mulGrp}_{R})$
108	106 107	syl	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to Unit (R) \in SubMnd ({mulGrp}_{R})$
109	105 23	eleqtrdi	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in {Base}_{R}$
110	102	cmnmndd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to {mulGrp}_{R} \in Mnd$
111	4	nnzd	$⊢ φ \to D \in ℤ$
112		1zzd	$⊢ φ \to 1 \in ℤ$
113	111 112	zsubcld	$⊢ φ \to D - 1 \in ℤ$
114		1cnd	$⊢ φ \to 1 \in ℂ$
115	114	addridd	$⊢ φ \to 1 + 0 = 1$
116	4	nnge1d	$⊢ φ \to 1 \leq D$
117	115 116	eqbrtrd	$⊢ φ \to 1 + 0 \leq D$
118		1red	$⊢ φ \to 1 \in ℝ$
119		0red	$⊢ φ \to 0 \in ℝ$
120	4	nnred	$⊢ φ \to D \in ℝ$
121	118 119 120	leaddsub2d	$⊢ φ \to (1 + 0 \leq D \leftrightarrow 0 \leq D - 1)$
122	117 121	mpbid	$⊢ φ \to 0 \leq D - 1$
123	113 122	jca	$⊢ φ \to (D - 1 \in ℤ \land 0 \leq D - 1)$
124		elnn0z	$⊢ D - 1 \in ℕ_{0} \leftrightarrow (D - 1 \in ℤ \land 0 \leq D - 1)$
125	123 124	sylibr	$⊢ φ \to D - 1 \in ℕ_{0}$
126	125	adantr	$⊢ (φ \land m \in {Base}_{G}) \to D - 1 \in ℕ_{0}$
127	126	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D - 1 \in ℕ_{0}$
128	18 73 110 127 109	mulgnn0cld	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to (D - 1) \cdot_{{mulGrp}_{R}} m \in {Base}_{R}$
129		simpr	$⊢ (((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \land o = (D - 1) \cdot_{{mulGrp}_{R}} m) \to o = (D - 1) \cdot_{{mulGrp}_{R}} m$
130	129	oveq1d	$⊢ (((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \land o = (D - 1) \cdot_{{mulGrp}_{R}} m) \to o \cdot_{R} m = ((D - 1) \cdot_{{mulGrp}_{R}} m) \cdot_{R} m$
131	130	eqeq1d	$⊢ (((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \land o = (D - 1) \cdot_{{mulGrp}_{R}} m) \to (o \cdot_{R} m = 1_{R} \leftrightarrow ((D - 1) \cdot_{{mulGrp}_{R}} m) \cdot_{R} m = 1_{R})$
132		eqid	$⊢ \cdot_{R} = \cdot_{R}$
133	16 132	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
134	133	a1i	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to \cdot_{R} = +_{{mulGrp}_{R}}$
135	134	oveqd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to ((D - 1) \cdot_{{mulGrp}_{R}} m) \cdot_{R} m = ((D - 1) \cdot_{{mulGrp}_{R}} m) +_{{mulGrp}_{R}} m$
136	103	nncnd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \in ℂ$
137		1cnd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 1 \in ℂ$
138	136 137	npcand	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D - 1 + 1 = D$
139	138	eqcomd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D = D - 1 + 1$
140	139	oveq1d	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{{mulGrp}_{R}} m = (D - 1 + 1) \cdot_{{mulGrp}_{R}} m$
141		eqid	$⊢ +_{{mulGrp}_{R}} = +_{{mulGrp}_{R}}$
142	13 73 141	mulgnn0p1	$⊢ ({mulGrp}_{R} \in Mnd \land D - 1 \in ℕ_{0} \land m \in {Base}_{{mulGrp}_{R}}) \to (D - 1 + 1) \cdot_{{mulGrp}_{R}} m = ((D - 1) \cdot_{{mulGrp}_{R}} m) +_{{mulGrp}_{R}} m$
143	110 127 105 142	syl3anc	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to (D - 1 + 1) \cdot_{{mulGrp}_{R}} m = ((D - 1) \cdot_{{mulGrp}_{R}} m) +_{{mulGrp}_{R}} m$
144	140 143	eqtr2d	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to ((D - 1) \cdot_{{mulGrp}_{R}} m) +_{{mulGrp}_{R}} m = D \cdot_{{mulGrp}_{R}} m$
145	16 65	ringidval	$⊢ 1_{R} = 0_{{mulGrp}_{R}}$
146	145	a1i	$⊢ φ \to 1_{R} = 0_{{mulGrp}_{R}}$
147	146	eqcomd	$⊢ φ \to 0_{{mulGrp}_{R}} = 1_{R}$
148	10 65	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
149	9 148	syl	$⊢ φ \to 1_{R} \in Unit (R)$
150	147 149	eqeltrd	$⊢ φ \to 0_{{mulGrp}_{R}} \in Unit (R)$
151	150	adantr	$⊢ (φ \land m \in {Base}_{G}) \to 0_{{mulGrp}_{R}} \in Unit (R)$
152	151	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{{mulGrp}_{R}} \in Unit (R)$
153	24	a1i	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to Unit (R) \subseteq {Base}_{{mulGrp}_{R}}$
154		eqid	$⊢ 0_{{mulGrp}_{R}} = 0_{{mulGrp}_{R}}$
155	1 13 154	ress0g	$⊢ ({mulGrp}_{R} \in Mnd \land 0_{{mulGrp}_{R}} \in Unit (R) \land Unit (R) \subseteq {Base}_{{mulGrp}_{R}}) \to 0_{{mulGrp}_{R}} = 0_{G}$
156	110 152 153 155	syl3anc	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{{mulGrp}_{R}} = 0_{G}$
157		simpr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to od (G) (m) = D$
158	157	eqcomd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D = od (G) (m)$
159	158	oveq1d	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{G} m = od (G) (m) \cdot_{G} m$
160		eqid	$⊢ od (G) = od (G)$
161		eqid	$⊢ 0_{G} = 0_{G}$
162	7 160 8 161	odid	$⊢ m \in {Base}_{G} \to od (G) (m) \cdot_{G} m = 0_{G}$
163	162	ad2antlr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to od (G) (m) \cdot_{G} m = 0_{G}$
164	159 163	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{G} m = 0_{G}$
165	164	eqcomd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{G} = D \cdot_{G} m$
166	156 165	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{{mulGrp}_{R}} = D \cdot_{G} m$
167	32	sselda	$⊢ (φ \land m \in {Base}_{G}) \to m \in Unit (R)$
168	167	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in Unit (R)$
169	1 153 168 103	ressmulgnnd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{G} m = D \cdot_{{mulGrp}_{R}} m$
170	166 169	eqtr2d	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{{mulGrp}_{R}} m = 0_{{mulGrp}_{R}}$
171	144 170	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to ((D - 1) \cdot_{{mulGrp}_{R}} m) +_{{mulGrp}_{R}} m = 0_{{mulGrp}_{R}}$
172	145	a1i	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 1_{R} = 0_{{mulGrp}_{R}}$
173	172	eqcomd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{{mulGrp}_{R}} = 1_{R}$
174	171 173	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to ((D - 1) \cdot_{{mulGrp}_{R}} m) +_{{mulGrp}_{R}} m = 1_{R}$
175	135 174	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to ((D - 1) \cdot_{{mulGrp}_{R}} m) \cdot_{R} m = 1_{R}$
176	128 131 175	rspcedvd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to \exists o \in {Base}_{R} o \cdot_{R} m = 1_{R}$
177	109 176	jca	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to (m \in {Base}_{R} \land \exists o \in {Base}_{R} o \cdot_{R} m = 1_{R})$
178		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
179	17 178 132	dvdsr	$⊢ m ∥_{r} (R) 1_{R} \leftrightarrow (m \in {Base}_{R} \land \exists o \in {Base}_{R} o \cdot_{R} m = 1_{R})$
180	177 179	sylibr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m ∥_{r} (R) 1_{R}$
181	99	adantr	$⊢ (φ \land m \in {Base}_{G}) \to R \in CRing$
182	181	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to R \in CRing$
183	10 65 178	crngunit	$⊢ R \in CRing \to (m \in Unit (R) \leftrightarrow m ∥_{r} (R) 1_{R})$
184	182 183	syl	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to (m \in Unit (R) \leftrightarrow m ∥_{r} (R) 1_{R})$
185	180 184	mpbird	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in Unit (R)$
186		eqid	$⊢ od ({mulGrp}_{R}) = od ({mulGrp}_{R})$
187	1 186 160	submod	$⊢ (Unit (R) \in SubMnd ({mulGrp}_{R}) \land m \in Unit (R)) \to od ({mulGrp}_{R}) (m) = od (G) (m)$
188	108 185 187	syl2anc	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to od ({mulGrp}_{R}) (m) = od (G) (m)$
189	188 157	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to od ({mulGrp}_{R}) (m) = D$
190	102 103 105 189	isprimroot2	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in ({mulGrp}_{R} PrimRoots D)$
191	98 190	syl	$⊢ ((φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \land (m \in {Base}_{G} \land od (G) (m) = D)) \to m \in ({mulGrp}_{R} PrimRoots D)$
192	94 191	mpdan	$⊢ (φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \to m \in ({mulGrp}_{R} PrimRoots D)$
193	192	ex	$⊢ φ \to (m \in \{w \in {Base}_{G} \| od (G) (w) = D\} \to m \in ({mulGrp}_{R} PrimRoots D))$
194	90 193	eximd	$⊢ φ \to (\exists m m \in \{w \in {Base}_{G} \| od (G) (w) = D\} \to \exists m m \in ({mulGrp}_{R} PrimRoots D))$
195	89 194	mpd	$⊢ φ \to \exists m m \in ({mulGrp}_{R} PrimRoots D)$
196		n0	$⊢ {mulGrp}_{R} PrimRoots D \neq \emptyset \leftrightarrow \exists m m \in ({mulGrp}_{R} PrimRoots D)$
197	195 196	sylibr	$⊢ φ \to {mulGrp}_{R} PrimRoots D \neq \emptyset$

Metamath Proof Explorer

Theorem unitscyglem5

Proof