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	bilani	$⊢ (φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \to (m \in {Base}_{G} \land od (G) (m) = D)$
94		simpll	$⊢ ((φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \land (m \in {Base}_{G} \land od (G) (m) = D)) \to φ$
95		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}$
96		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$
97	94 95 96	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)$
98	2	idomcringd	$⊢ φ \to R \in CRing$
99	16	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
100	98 99	syl	$⊢ φ \to {mulGrp}_{R} \in CMnd$
101	100	ad2antrr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to {mulGrp}_{R} \in CMnd$
102	4	ad2antrr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \in ℕ$
103	15	sselda	$⊢ (φ \land m \in {Base}_{G}) \to m \in {Base}_{{mulGrp}_{R}}$
104	103	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in {Base}_{{mulGrp}_{R}}$
105	9	ad2antrr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to R \in Ring$
106	10 16	unitsubm	$⊢ R \in Ring \to Unit (R) \in SubMnd ({mulGrp}_{R})$
107	105 106	syl	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to Unit (R) \in SubMnd ({mulGrp}_{R})$
108	104 23	eleqtrdi	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in {Base}_{R}$
109	101	cmnmndd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to {mulGrp}_{R} \in Mnd$
110	4	nnzd	$⊢ φ \to D \in ℤ$
111		1zzd	$⊢ φ \to 1 \in ℤ$
112	110 111	zsubcld	$⊢ φ \to D - 1 \in ℤ$
113		1cnd	$⊢ φ \to 1 \in ℂ$
114	113	addridd	$⊢ φ \to 1 + 0 = 1$
115	4	nnge1d	$⊢ φ \to 1 \leq D$
116	114 115	eqbrtrd	$⊢ φ \to 1 + 0 \leq D$
117		1red	$⊢ φ \to 1 \in ℝ$
118		0red	$⊢ φ \to 0 \in ℝ$
119	4	nnred	$⊢ φ \to D \in ℝ$
120	117 118 119	leaddsub2d	$⊢ φ \to (1 + 0 \leq D \leftrightarrow 0 \leq D - 1)$
121	116 120	mpbid	$⊢ φ \to 0 \leq D - 1$
122	112 121	jca	$⊢ φ \to (D - 1 \in ℤ \land 0 \leq D - 1)$
123		elnn0z	$⊢ D - 1 \in ℕ_{0} \leftrightarrow (D - 1 \in ℤ \land 0 \leq D - 1)$
124	122 123	sylibr	$⊢ φ \to D - 1 \in ℕ_{0}$
125	124	adantr	$⊢ (φ \land m \in {Base}_{G}) \to D - 1 \in ℕ_{0}$
126	125	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D - 1 \in ℕ_{0}$
127	18 73 109 126 108	mulgnn0cld	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to (D - 1) \cdot_{{mulGrp}_{R}} m \in {Base}_{R}$
128		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$
129	128	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$
130	129	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})$
131		eqid	$⊢ \cdot_{R} = \cdot_{R}$
132	16 131	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
133	132	a1i	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to \cdot_{R} = +_{{mulGrp}_{R}}$
134	133	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$
135	102	nncnd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \in ℂ$
136		1cnd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 1 \in ℂ$
137	135 136	npcand	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D - 1 + 1 = D$
138	137	eqcomd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D = D - 1 + 1$
139	138	oveq1d	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{{mulGrp}_{R}} m = (D - 1 + 1) \cdot_{{mulGrp}_{R}} m$
140		eqid	$⊢ +_{{mulGrp}_{R}} = +_{{mulGrp}_{R}}$
141	13 73 140	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$
142	109 126 104 141	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$
143	139 142	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$
144	16 65	ringidval	$⊢ 1_{R} = 0_{{mulGrp}_{R}}$
145	144	a1i	$⊢ φ \to 1_{R} = 0_{{mulGrp}_{R}}$
146	145	eqcomd	$⊢ φ \to 0_{{mulGrp}_{R}} = 1_{R}$
147	10 65	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
148	9 147	syl	$⊢ φ \to 1_{R} \in Unit (R)$
149	146 148	eqeltrd	$⊢ φ \to 0_{{mulGrp}_{R}} \in Unit (R)$
150	149	adantr	$⊢ (φ \land m \in {Base}_{G}) \to 0_{{mulGrp}_{R}} \in Unit (R)$
151	150	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{{mulGrp}_{R}} \in Unit (R)$
152	24	a1i	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to Unit (R) \subseteq {Base}_{{mulGrp}_{R}}$
153		eqid	$⊢ 0_{{mulGrp}_{R}} = 0_{{mulGrp}_{R}}$
154	1 13 153	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}$
155	109 151 152 154	syl3anc	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{{mulGrp}_{R}} = 0_{G}$
156		simpr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to od (G) (m) = D$
157	156	eqcomd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D = od (G) (m)$
158	157	oveq1d	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{G} m = od (G) (m) \cdot_{G} m$
159		eqid	$⊢ od (G) = od (G)$
160		eqid	$⊢ 0_{G} = 0_{G}$
161	7 159 8 160	odid	$⊢ m \in {Base}_{G} \to od (G) (m) \cdot_{G} m = 0_{G}$
162	161	ad2antlr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to od (G) (m) \cdot_{G} m = 0_{G}$
163	158 162	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{G} m = 0_{G}$
164	163	eqcomd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{G} = D \cdot_{G} m$
165	155 164	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{{mulGrp}_{R}} = D \cdot_{G} m$
166	32	sselda	$⊢ (φ \land m \in {Base}_{G}) \to m \in Unit (R)$
167	166	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in Unit (R)$
168	1 152 167 102	ressmulgnnd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{G} m = D \cdot_{{mulGrp}_{R}} m$
169	165 168	eqtr2d	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to D \cdot_{{mulGrp}_{R}} m = 0_{{mulGrp}_{R}}$
170	143 169	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to ((D - 1) \cdot_{{mulGrp}_{R}} m) +_{{mulGrp}_{R}} m = 0_{{mulGrp}_{R}}$
171	144	a1i	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 1_{R} = 0_{{mulGrp}_{R}}$
172	171	eqcomd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to 0_{{mulGrp}_{R}} = 1_{R}$
173	170 172	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to ((D - 1) \cdot_{{mulGrp}_{R}} m) +_{{mulGrp}_{R}} m = 1_{R}$
174	134 173	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to ((D - 1) \cdot_{{mulGrp}_{R}} m) \cdot_{R} m = 1_{R}$
175	127 130 174	rspcedvd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to \exists o \in {Base}_{R} o \cdot_{R} m = 1_{R}$
176	108 175	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})$
177		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
178	17 177 131	dvdsr	$⊢ m ∥_{r} (R) 1_{R} \leftrightarrow (m \in {Base}_{R} \land \exists o \in {Base}_{R} o \cdot_{R} m = 1_{R})$
179	176 178	sylibr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m ∥_{r} (R) 1_{R}$
180	98	adantr	$⊢ (φ \land m \in {Base}_{G}) \to R \in CRing$
181	180	adantr	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to R \in CRing$
182	10 65 177	crngunit	$⊢ R \in CRing \to (m \in Unit (R) \leftrightarrow m ∥_{r} (R) 1_{R})$
183	181 182	syl	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to (m \in Unit (R) \leftrightarrow m ∥_{r} (R) 1_{R})$
184	179 183	mpbird	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in Unit (R)$
185		eqid	$⊢ od ({mulGrp}_{R}) = od ({mulGrp}_{R})$
186	1 185 159	submod	$⊢ (Unit (R) \in SubMnd ({mulGrp}_{R}) \land m \in Unit (R)) \to od ({mulGrp}_{R}) (m) = od (G) (m)$
187	107 184 186	syl2anc	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to od ({mulGrp}_{R}) (m) = od (G) (m)$
188	187 156	eqtrd	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to od ({mulGrp}_{R}) (m) = D$
189	101 102 104 188	isprimroot2	$⊢ ((φ \land m \in {Base}_{G}) \land od (G) (m) = D) \to m \in ({mulGrp}_{R} PrimRoots D)$
190	97 189	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)$
191	93 190	mpdan	$⊢ (φ \land m \in \{w \in {Base}_{G} \| od (G) (w) = D\}) \to m \in ({mulGrp}_{R} PrimRoots D)$
192	191	ex	$⊢ φ \to (m \in \{w \in {Base}_{G} \| od (G) (w) = D\} \to m \in ({mulGrp}_{R} PrimRoots D))$
193	90 192	eximd	$⊢ φ \to (\exists m m \in \{w \in {Base}_{G} \| od (G) (w) = D\} \to \exists m m \in ({mulGrp}_{R} PrimRoots D))$
194	89 193	mpd	$⊢ φ \to \exists m m \in ({mulGrp}_{R} PrimRoots D)$
195		n0	$⊢ {mulGrp}_{R} PrimRoots D \neq \emptyset \leftrightarrow \exists m m \in ({mulGrp}_{R} PrimRoots D)$
196	194 195	sylibr	$⊢ φ \to {mulGrp}_{R} PrimRoots D \neq \emptyset$

Metamath Proof Explorer

Theorem unitscyglem5

Proof