primrootsunit1

Description: Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025)

	Ref	Expression
Hypotheses	primrootsunit1.1	$⊢ φ \to R \in CMnd$
	primrootsunit1.2	$⊢ φ \to K \in ℕ$
	primrootsunit1.3	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
Assertion	primrootsunit1	$⊢ φ \to (R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K \land R ↾_{𝑠} U \in Abel)$

Proof

Step	Hyp	Ref	Expression
1		primrootsunit1.1	$⊢ φ \to R \in CMnd$
2		primrootsunit1.2	$⊢ φ \to K \in ℕ$
3		primrootsunit1.3	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
4	1	adantr	$⊢ (φ \land c \in (R PrimRoots K)) \to R \in CMnd$
5	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
6	5	adantr	$⊢ (φ \land c \in (R PrimRoots K)) \to K \in ℕ_{0}$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8	4 6 7	isprimroot	$⊢ (φ \land c \in (R PrimRoots K)) \to (c \in (R PrimRoots K) \leftrightarrow (c \in {Base}_{R} \land K \cdot_{R} c = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} c = 0_{R} \to K ∥ l)))$
9	8	biimpd	$⊢ (φ \land c \in (R PrimRoots K)) \to (c \in (R PrimRoots K) \to (c \in {Base}_{R} \land K \cdot_{R} c = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} c = 0_{R} \to K ∥ l)))$
10	9	syldbl2	$⊢ (φ \land c \in (R PrimRoots K)) \to (c \in {Base}_{R} \land K \cdot_{R} c = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} c = 0_{R} \to K ∥ l))$
11	10	simp1d	$⊢ (φ \land c \in (R PrimRoots K)) \to c \in {Base}_{R}$
12	1	cmnmndd	$⊢ φ \to R \in Mnd$
13	12	adantr	$⊢ (φ \land c \in (R PrimRoots K)) \to R \in Mnd$
14		nnm1nn0	$⊢ K \in ℕ \to K - 1 \in ℕ_{0}$
15	2 14	syl	$⊢ φ \to K - 1 \in ℕ_{0}$
16	15	adantr	$⊢ (φ \land c \in (R PrimRoots K)) \to K - 1 \in ℕ_{0}$
17		eqid	$⊢ {Base}_{R} = {Base}_{R}$
18	17 7	mulgnn0cl	$⊢ (R \in Mnd \land K - 1 \in ℕ_{0} \land c \in {Base}_{R}) \to (K - 1) \cdot_{R} c \in {Base}_{R}$
19	13 16 11 18	syl3anc	$⊢ (φ \land c \in (R PrimRoots K)) \to (K - 1) \cdot_{R} c \in {Base}_{R}$
20		simpr	$⊢ ((φ \land c \in (R PrimRoots K)) \land i = (K - 1) \cdot_{R} c) \to i = (K - 1) \cdot_{R} c$
21	20	oveq1d	$⊢ ((φ \land c \in (R PrimRoots K)) \land i = (K - 1) \cdot_{R} c) \to i +_{R} c = ((K - 1) \cdot_{R} c) +_{R} c$
22	21	eqeq1d	$⊢ ((φ \land c \in (R PrimRoots K)) \land i = (K - 1) \cdot_{R} c) \to (i +_{R} c = 0_{R} \leftrightarrow ((K - 1) \cdot_{R} c) +_{R} c = 0_{R})$
23	2	nncnd	$⊢ φ \to K \in ℂ$
24		1cnd	$⊢ φ \to 1 \in ℂ$
25	23 24	npcand	$⊢ φ \to K - 1 + 1 = K$
26	25	eqcomd	$⊢ φ \to K = K - 1 + 1$
27	26	adantr	$⊢ (φ \land c \in (R PrimRoots K)) \to K = K - 1 + 1$
28	27	oveq1d	$⊢ (φ \land c \in (R PrimRoots K)) \to K \cdot_{R} c = (K - 1 + 1) \cdot_{R} c$
29		eqid	$⊢ +_{R} = +_{R}$
30	17 7 29	mulgnn0p1	$⊢ (R \in Mnd \land K - 1 \in ℕ_{0} \land c \in {Base}_{R}) \to (K - 1 + 1) \cdot_{R} c = ((K - 1) \cdot_{R} c) +_{R} c$
31	13 16 11 30	syl3anc	$⊢ (φ \land c \in (R PrimRoots K)) \to (K - 1 + 1) \cdot_{R} c = ((K - 1) \cdot_{R} c) +_{R} c$
32	28 31	eqtr2d	$⊢ (φ \land c \in (R PrimRoots K)) \to ((K - 1) \cdot_{R} c) +_{R} c = K \cdot_{R} c$
33	10	simp2d	$⊢ (φ \land c \in (R PrimRoots K)) \to K \cdot_{R} c = 0_{R}$
34	32 33	eqtrd	$⊢ (φ \land c \in (R PrimRoots K)) \to ((K - 1) \cdot_{R} c) +_{R} c = 0_{R}$
35	19 22 34	rspcedvd	$⊢ (φ \land c \in (R PrimRoots K)) \to \exists i \in {Base}_{R} i +_{R} c = 0_{R}$
36	11 35	jca	$⊢ (φ \land c \in (R PrimRoots K)) \to (c \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} c = 0_{R})$
37		oveq2	$⊢ a = c \to i +_{R} a = i +_{R} c$
38	37	eqeq1d	$⊢ a = c \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} c = 0_{R})$
39	38	rexbidv	$⊢ a = c \to (\exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists i \in {Base}_{R} i +_{R} c = 0_{R})$
40	39	elrab	$⊢ c \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \leftrightarrow (c \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} c = 0_{R})$
41	36 40	sylibr	$⊢ (φ \land c \in (R PrimRoots K)) \to c \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
42	3	eleq2i	$⊢ c \in U \leftrightarrow c \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
43	41 42	sylibr	$⊢ (φ \land c \in (R PrimRoots K)) \to c \in U$
44		simpl	$⊢ (φ \land b \in U) \to φ$
45	3	a1i	$⊢ φ \to U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
46	45	eleq2d	$⊢ φ \to (b \in U \leftrightarrow b \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
47	46	biimpd	$⊢ φ \to (b \in U \to b \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
48	47	imp	$⊢ (φ \land b \in U) \to b \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
49	44 48	jca	$⊢ (φ \land b \in U) \to (φ \land b \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
50		elrabi	$⊢ b \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \to b \in {Base}_{R}$
51	50	adantl	$⊢ (φ \land b \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}) \to b \in {Base}_{R}$
52	49 51	syl	$⊢ (φ \land b \in U) \to b \in {Base}_{R}$
53	52	ex	$⊢ φ \to (b \in U \to b \in {Base}_{R})$
54	53	ssrdv	$⊢ φ \to U \subseteq {Base}_{R}$
55		eqid	$⊢ R ↾_{𝑠} U = R ↾_{𝑠} U$
56	55 17	ressbas2	$⊢ U \subseteq {Base}_{R} \to U = {Base}_{(R ↾_{𝑠} U)}$
57	54 56	syl	$⊢ φ \to U = {Base}_{(R ↾_{𝑠} U)}$
58	57	adantr	$⊢ (φ \land c \in (R PrimRoots K)) \to U = {Base}_{(R ↾_{𝑠} U)}$
59	58	eleq2d	$⊢ (φ \land c \in (R PrimRoots K)) \to (c \in U \leftrightarrow c \in {Base}_{(R ↾_{𝑠} U)})$
60	43 59	mpbid	$⊢ (φ \land c \in (R PrimRoots K)) \to c \in {Base}_{(R ↾_{𝑠} U)}$
61	12	ad2antrr	$⊢ ((φ \land b \in U) \land d \in U) \to R \in Mnd$
62	52	adantr	$⊢ ((φ \land b \in U) \land d \in U) \to b \in {Base}_{R}$
63		simpl	$⊢ (φ \land d \in U) \to φ$
64	45	eleq2d	$⊢ φ \to (d \in U \leftrightarrow d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
65	64	biimpd	$⊢ φ \to (d \in U \to d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
66	65	imp	$⊢ (φ \land d \in U) \to d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
67	63 66	jca	$⊢ (φ \land d \in U) \to (φ \land d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
68		elrabi	$⊢ d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \to d \in {Base}_{R}$
69	68	adantl	$⊢ (φ \land d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}) \to d \in {Base}_{R}$
70	67 69	syl	$⊢ (φ \land d \in U) \to d \in {Base}_{R}$
71	44 70	sylan	$⊢ ((φ \land b \in U) \land d \in U) \to d \in {Base}_{R}$
72	17 29	mndcl	$⊢ (R \in Mnd \land b \in {Base}_{R} \land d \in {Base}_{R}) \to b +_{R} d \in {Base}_{R}$
73	61 62 71 72	syl3anc	$⊢ ((φ \land b \in U) \land d \in U) \to b +_{R} d \in {Base}_{R}$
74	3	eleq2i	$⊢ d \in U \leftrightarrow d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
75		oveq2	$⊢ a = d \to i +_{R} a = i +_{R} d$
76	75	eqeq1d	$⊢ a = d \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} d = 0_{R})$
77	76	rexbidv	$⊢ a = d \to (\exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists i \in {Base}_{R} i +_{R} d = 0_{R})$
78	77	elrab	$⊢ d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \leftrightarrow (d \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} d = 0_{R})$
79	74 78	bitri	$⊢ d \in U \leftrightarrow (d \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} d = 0_{R})$
80	79	biimpi	$⊢ d \in U \to (d \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} d = 0_{R})$
81	80	simprd	$⊢ d \in U \to \exists i \in {Base}_{R} i +_{R} d = 0_{R}$
82	81	adantl	$⊢ ((φ \land b \in U) \land d \in U) \to \exists i \in {Base}_{R} i +_{R} d = 0_{R}$
83	1	ad4antr	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} d = 0_{R}) \to R \in CMnd$
84	71	ad2antrr	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} d = 0_{R}) \to d \in {Base}_{R}$
85		simplr	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} d = 0_{R}) \to i \in {Base}_{R}$
86	17 29	cmncom	$⊢ (R \in CMnd \land d \in {Base}_{R} \land i \in {Base}_{R}) \to d +_{R} i = i +_{R} d$
87	83 84 85 86	syl3anc	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} d = 0_{R}) \to d +_{R} i = i +_{R} d$
88		simpr	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} d = 0_{R}) \to i +_{R} d = 0_{R}$
89	87 88	eqtrd	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} d = 0_{R}) \to d +_{R} i = 0_{R}$
90	89	ex	$⊢ (((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \to (i +_{R} d = 0_{R} \to d +_{R} i = 0_{R})$
91	90	reximdva	$⊢ ((φ \land b \in U) \land d \in U) \to (\exists i \in {Base}_{R} i +_{R} d = 0_{R} \to \exists i \in {Base}_{R} d +_{R} i = 0_{R})$
92	82 91	mpd	$⊢ ((φ \land b \in U) \land d \in U) \to \exists i \in {Base}_{R} d +_{R} i = 0_{R}$
93	17 61 71 92	mndmolinv	$⊢ ((φ \land b \in U) \land d \in U) \to \exists^{*} i \in {Base}_{R} i +_{R} d = 0_{R}$
94	82 93	jca	$⊢ ((φ \land b \in U) \land d \in U) \to (\exists i \in {Base}_{R} i +_{R} d = 0_{R} \land \exists^{*} i \in {Base}_{R} i +_{R} d = 0_{R})$
95		reu5	$⊢ \exists! i \in {Base}_{R} i +_{R} d = 0_{R} \leftrightarrow (\exists i \in {Base}_{R} i +_{R} d = 0_{R} \land \exists^{*} i \in {Base}_{R} i +_{R} d = 0_{R})$
96	94 95	sylibr	$⊢ ((φ \land b \in U) \land d \in U) \to \exists! i \in {Base}_{R} i +_{R} d = 0_{R}$
97		riotacl	$⊢ \exists! i \in {Base}_{R} i +_{R} d = 0_{R} \to (ι i \in {Base}_{R} \| i +_{R} d = 0_{R}) \in {Base}_{R}$
98	96 97	syl	$⊢ ((φ \land b \in U) \land d \in U) \to (ι i \in {Base}_{R} \| i +_{R} d = 0_{R}) \in {Base}_{R}$
99		eqid	$⊢ 0_{R} = 0_{R}$
100		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
101	17 29 99 100	grpinvval	$⊢ d \in {Base}_{R} \to {inv}_{g} (R) (d) = (ι i \in {Base}_{R} \| i +_{R} d = 0_{R})$
102	71 101	syl	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) = (ι i \in {Base}_{R} \| i +_{R} d = 0_{R})$
103	102	eleq1d	$⊢ ((φ \land b \in U) \land d \in U) \to ({inv}_{g} (R) (d) \in {Base}_{R} \leftrightarrow (ι i \in {Base}_{R} \| i +_{R} d = 0_{R}) \in {Base}_{R})$
104	98 103	mpbird	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) \in {Base}_{R}$
105	3	eleq2i	$⊢ b \in U \leftrightarrow b \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
106		oveq2	$⊢ a = b \to i +_{R} a = i +_{R} b$
107	106	eqeq1d	$⊢ a = b \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} b = 0_{R})$
108	107	rexbidv	$⊢ a = b \to (\exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists i \in {Base}_{R} i +_{R} b = 0_{R})$
109	108	elrab	$⊢ b \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \leftrightarrow (b \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} b = 0_{R})$
110	105 109	bitri	$⊢ b \in U \leftrightarrow (b \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} b = 0_{R})$
111	110	biimpi	$⊢ b \in U \to (b \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} b = 0_{R})$
112	111	simprd	$⊢ b \in U \to \exists i \in {Base}_{R} i +_{R} b = 0_{R}$
113	112	ad2antlr	$⊢ ((φ \land b \in U) \land d \in U) \to \exists i \in {Base}_{R} i +_{R} b = 0_{R}$
114	1	ad4antr	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} b = 0_{R}) \to R \in CMnd$
115	62	ad2antrr	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} b = 0_{R}) \to b \in {Base}_{R}$
116		simplr	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} b = 0_{R}) \to i \in {Base}_{R}$
117	17 29	cmncom	$⊢ (R \in CMnd \land b \in {Base}_{R} \land i \in {Base}_{R}) \to b +_{R} i = i +_{R} b$
118	114 115 116 117	syl3anc	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} b = 0_{R}) \to b +_{R} i = i +_{R} b$
119		simpr	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} b = 0_{R}) \to i +_{R} b = 0_{R}$
120	118 119	eqtrd	$⊢ ((((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \land i +_{R} b = 0_{R}) \to b +_{R} i = 0_{R}$
121	120	ex	$⊢ (((φ \land b \in U) \land d \in U) \land i \in {Base}_{R}) \to (i +_{R} b = 0_{R} \to b +_{R} i = 0_{R})$
122	121	reximdva	$⊢ ((φ \land b \in U) \land d \in U) \to (\exists i \in {Base}_{R} i +_{R} b = 0_{R} \to \exists i \in {Base}_{R} b +_{R} i = 0_{R})$
123	113 122	mpd	$⊢ ((φ \land b \in U) \land d \in U) \to \exists i \in {Base}_{R} b +_{R} i = 0_{R}$
124	17 61 62 123	mndmolinv	$⊢ ((φ \land b \in U) \land d \in U) \to \exists^{*} i \in {Base}_{R} i +_{R} b = 0_{R}$
125	113 124	jca	$⊢ ((φ \land b \in U) \land d \in U) \to (\exists i \in {Base}_{R} i +_{R} b = 0_{R} \land \exists^{*} i \in {Base}_{R} i +_{R} b = 0_{R})$
126		reu5	$⊢ \exists! i \in {Base}_{R} i +_{R} b = 0_{R} \leftrightarrow (\exists i \in {Base}_{R} i +_{R} b = 0_{R} \land \exists^{*} i \in {Base}_{R} i +_{R} b = 0_{R})$
127	125 126	sylibr	$⊢ ((φ \land b \in U) \land d \in U) \to \exists! i \in {Base}_{R} i +_{R} b = 0_{R}$
128		riotacl	$⊢ \exists! i \in {Base}_{R} i +_{R} b = 0_{R} \to (ι i \in {Base}_{R} \| i +_{R} b = 0_{R}) \in {Base}_{R}$
129	127 128	syl	$⊢ ((φ \land b \in U) \land d \in U) \to (ι i \in {Base}_{R} \| i +_{R} b = 0_{R}) \in {Base}_{R}$
130	17 29 99 100	grpinvval	$⊢ b \in {Base}_{R} \to {inv}_{g} (R) (b) = (ι i \in {Base}_{R} \| i +_{R} b = 0_{R})$
131	62 130	syl	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (b) = (ι i \in {Base}_{R} \| i +_{R} b = 0_{R})$
132	131	eleq1d	$⊢ ((φ \land b \in U) \land d \in U) \to ({inv}_{g} (R) (b) \in {Base}_{R} \leftrightarrow (ι i \in {Base}_{R} \| i +_{R} b = 0_{R}) \in {Base}_{R})$
133	129 132	mpbird	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (b) \in {Base}_{R}$
134	17 29	mndcl	$⊢ (R \in Mnd \land {inv}_{g} (R) (d) \in {Base}_{R} \land {inv}_{g} (R) (b) \in {Base}_{R}) \to {inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b) \in {Base}_{R}$
135	61 104 133 134	syl3anc	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b) \in {Base}_{R}$
136		oveq1	$⊢ i = {inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b) \to i +_{R} (b +_{R} d) = ({inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b)) +_{R} (b +_{R} d)$
137	136	eqeq1d	$⊢ i = {inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b) \to (i +_{R} (b +_{R} d) = 0_{R} \leftrightarrow ({inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b)) +_{R} (b +_{R} d) = 0_{R})$
138	137	adantl	$⊢ (((φ \land b \in U) \land d \in U) \land i = {inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b)) \to (i +_{R} (b +_{R} d) = 0_{R} \leftrightarrow ({inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b)) +_{R} (b +_{R} d) = 0_{R})$
139	104 133 73	3jca	$⊢ ((φ \land b \in U) \land d \in U) \to ({inv}_{g} (R) (d) \in {Base}_{R} \land {inv}_{g} (R) (b) \in {Base}_{R} \land b +_{R} d \in {Base}_{R})$
140	17 29	mndass	$⊢ (R \in Mnd \land ({inv}_{g} (R) (d) \in {Base}_{R} \land {inv}_{g} (R) (b) \in {Base}_{R} \land b +_{R} d \in {Base}_{R})) \to ({inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b)) +_{R} (b +_{R} d) = {inv}_{g} (R) (d) +_{R} ({inv}_{g} (R) (b) +_{R} (b +_{R} d))$
141	61 139 140	syl2anc	$⊢ ((φ \land b \in U) \land d \in U) \to ({inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b)) +_{R} (b +_{R} d) = {inv}_{g} (R) (d) +_{R} ({inv}_{g} (R) (b) +_{R} (b +_{R} d))$
142	133 62 71	3jca	$⊢ ((φ \land b \in U) \land d \in U) \to ({inv}_{g} (R) (b) \in {Base}_{R} \land b \in {Base}_{R} \land d \in {Base}_{R})$
143	17 29	mndass	$⊢ (R \in Mnd \land ({inv}_{g} (R) (b) \in {Base}_{R} \land b \in {Base}_{R} \land d \in {Base}_{R})) \to ({inv}_{g} (R) (b) +_{R} b) +_{R} d = {inv}_{g} (R) (b) +_{R} (b +_{R} d)$
144	143	eqcomd	$⊢ (R \in Mnd \land ({inv}_{g} (R) (b) \in {Base}_{R} \land b \in {Base}_{R} \land d \in {Base}_{R})) \to {inv}_{g} (R) (b) +_{R} (b +_{R} d) = ({inv}_{g} (R) (b) +_{R} b) +_{R} d$
145	61 142 144	syl2anc	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (b) +_{R} (b +_{R} d) = ({inv}_{g} (R) (b) +_{R} b) +_{R} d$
146	145	oveq2d	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) +_{R} ({inv}_{g} (R) (b) +_{R} (b +_{R} d)) = {inv}_{g} (R) (d) +_{R} (({inv}_{g} (R) (b) +_{R} b) +_{R} d)$
147	62 127	linvh	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (b) +_{R} b = 0_{R}$
148	147	oveq1d	$⊢ ((φ \land b \in U) \land d \in U) \to ({inv}_{g} (R) (b) +_{R} b) +_{R} d = 0_{R} +_{R} d$
149	148	oveq2d	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) +_{R} (({inv}_{g} (R) (b) +_{R} b) +_{R} d) = {inv}_{g} (R) (d) +_{R} (0_{R} +_{R} d)$
150	17 29 99	mndlid	$⊢ (R \in Mnd \land d \in {Base}_{R}) \to 0_{R} +_{R} d = d$
151	61 71 150	syl2anc	$⊢ ((φ \land b \in U) \land d \in U) \to 0_{R} +_{R} d = d$
152	151	oveq2d	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) +_{R} (0_{R} +_{R} d) = {inv}_{g} (R) (d) +_{R} d$
153	71 96	linvh	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) +_{R} d = 0_{R}$
154	152 153	eqtrd	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) +_{R} (0_{R} +_{R} d) = 0_{R}$
155	149 154	eqtrd	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) +_{R} (({inv}_{g} (R) (b) +_{R} b) +_{R} d) = 0_{R}$
156	146 155	eqtrd	$⊢ ((φ \land b \in U) \land d \in U) \to {inv}_{g} (R) (d) +_{R} ({inv}_{g} (R) (b) +_{R} (b +_{R} d)) = 0_{R}$
157	141 156	eqtrd	$⊢ ((φ \land b \in U) \land d \in U) \to ({inv}_{g} (R) (d) +_{R} {inv}_{g} (R) (b)) +_{R} (b +_{R} d) = 0_{R}$
158	135 138 157	rspcedvd	$⊢ ((φ \land b \in U) \land d \in U) \to \exists i \in {Base}_{R} i +_{R} (b +_{R} d) = 0_{R}$
159	73 158	jca	$⊢ ((φ \land b \in U) \land d \in U) \to (b +_{R} d \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} (b +_{R} d) = 0_{R})$
160		oveq2	$⊢ a = b +_{R} d \to i +_{R} a = i +_{R} (b +_{R} d)$
161	160	eqeq1d	$⊢ a = b +_{R} d \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} (b +_{R} d) = 0_{R})$
162	161	rexbidv	$⊢ a = b +_{R} d \to (\exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists i \in {Base}_{R} i +_{R} (b +_{R} d) = 0_{R})$
163	162	elrab	$⊢ b +_{R} d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \leftrightarrow (b +_{R} d \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} (b +_{R} d) = 0_{R})$
164	159 163	sylibr	$⊢ ((φ \land b \in U) \land d \in U) \to b +_{R} d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
165	3	eleq2i	$⊢ b +_{R} d \in U \leftrightarrow b +_{R} d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
166	165	a1i	$⊢ ((φ \land b \in U) \land d \in U) \to (b +_{R} d \in U \leftrightarrow b +_{R} d \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
167	164 166	mpbird	$⊢ ((φ \land b \in U) \land d \in U) \to b +_{R} d \in U$
168	167	ralrimiva	$⊢ (φ \land b \in U) \to \forall d \in U b +_{R} d \in U$
169	168	ralrimiva	$⊢ φ \to \forall b \in U \forall d \in U b +_{R} d \in U$
170		oveq2	$⊢ a = 0_{R} \to i +_{R} a = i +_{R} 0_{R}$
171	170	eqeq1d	$⊢ a = 0_{R} \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} 0_{R} = 0_{R})$
172	171	rexbidv	$⊢ a = 0_{R} \to (\exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists i \in {Base}_{R} i +_{R} 0_{R} = 0_{R})$
173	17 99	mndidcl	$⊢ R \in Mnd \to 0_{R} \in {Base}_{R}$
174	12 173	syl	$⊢ φ \to 0_{R} \in {Base}_{R}$
175	12 174	jca	$⊢ φ \to (R \in Mnd \land 0_{R} \in {Base}_{R})$
176	17 29 99	mndlid	$⊢ (R \in Mnd \land 0_{R} \in {Base}_{R}) \to 0_{R} +_{R} 0_{R} = 0_{R}$
177	175 176	syl	$⊢ φ \to 0_{R} +_{R} 0_{R} = 0_{R}$
178	174 177	jca	$⊢ φ \to (0_{R} \in {Base}_{R} \land 0_{R} +_{R} 0_{R} = 0_{R})$
179		oveq1	$⊢ i = 0_{R} \to i +_{R} 0_{R} = 0_{R} +_{R} 0_{R}$
180	179	eqeq1d	$⊢ i = 0_{R} \to (i +_{R} 0_{R} = 0_{R} \leftrightarrow 0_{R} +_{R} 0_{R} = 0_{R})$
181	180	rspcev	$⊢ (0_{R} \in {Base}_{R} \land 0_{R} +_{R} 0_{R} = 0_{R}) \to \exists i \in {Base}_{R} i +_{R} 0_{R} = 0_{R}$
182	178 181	syl	$⊢ φ \to \exists i \in {Base}_{R} i +_{R} 0_{R} = 0_{R}$
183	172 174 182	elrabd	$⊢ φ \to 0_{R} \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
184	45	eleq2d	$⊢ φ \to (0_{R} \in U \leftrightarrow 0_{R} \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
185	183 184	mpbird	$⊢ φ \to 0_{R} \in U$
186	17 29 99 55	issubmnd	$⊢ (R \in Mnd \land U \subseteq {Base}_{R} \land 0_{R} \in U) \to (R ↾_{𝑠} U \in Mnd \leftrightarrow \forall b \in U \forall d \in U b +_{R} d \in U)$
187	12 54 185 186	syl3anc	$⊢ φ \to (R ↾_{𝑠} U \in Mnd \leftrightarrow \forall b \in U \forall d \in U b +_{R} d \in U)$
188	169 187	mpbird	$⊢ φ \to R ↾_{𝑠} U \in Mnd$
189	45	eleq2d	$⊢ φ \to (q \in U \leftrightarrow q \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
190	189	biimpd	$⊢ φ \to (q \in U \to q \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
191	190	imp	$⊢ (φ \land q \in U) \to q \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
192		oveq2	$⊢ a = q \to i +_{R} a = i +_{R} q$
193	192	eqeq1d	$⊢ a = q \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} q = 0_{R})$
194	193	rexbidv	$⊢ a = q \to (\exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists i \in {Base}_{R} i +_{R} q = 0_{R})$
195	194	elrab	$⊢ q \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \leftrightarrow (q \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} q = 0_{R})$
196	191 195	sylib	$⊢ (φ \land q \in U) \to (q \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} q = 0_{R})$
197	196	simprd	$⊢ (φ \land q \in U) \to \exists i \in {Base}_{R} i +_{R} q = 0_{R}$
198		simprl	$⊢ ((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \to i \in {Base}_{R}$
199	196	simpld	$⊢ (φ \land q \in U) \to q \in {Base}_{R}$
200	199	adantr	$⊢ ((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \to q \in {Base}_{R}$
201		simpr	$⊢ (((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \land j = q) \to j = q$
202	201	oveq1d	$⊢ (((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \land j = q) \to j +_{R} i = q +_{R} i$
203	202	eqeq1d	$⊢ (((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \land j = q) \to (j +_{R} i = 0_{R} \leftrightarrow q +_{R} i = 0_{R})$
204	1	ad2antrr	$⊢ ((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \to R \in CMnd$
205	17 29	cmncom	$⊢ (R \in CMnd \land i \in {Base}_{R} \land q \in {Base}_{R}) \to i +_{R} q = q +_{R} i$
206	204 198 200 205	syl3anc	$⊢ ((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \to i +_{R} q = q +_{R} i$
207		simprr	$⊢ ((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \to i +_{R} q = 0_{R}$
208	206 207	eqtr3d	$⊢ ((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \to q +_{R} i = 0_{R}$
209	200 203 208	rspcedvd	$⊢ ((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \to \exists j \in {Base}_{R} j +_{R} i = 0_{R}$
210	198 209	jca	$⊢ ((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \to (i \in {Base}_{R} \land \exists j \in {Base}_{R} j +_{R} i = 0_{R})$
211		nfv	$⊢ Ⅎ j i +_{R} a = 0_{R}$
212		nfv	$⊢ Ⅎ i j +_{R} a = 0_{R}$
213		oveq1	$⊢ i = j \to i +_{R} a = j +_{R} a$
214	213	eqeq1d	$⊢ i = j \to (i +_{R} a = 0_{R} \leftrightarrow j +_{R} a = 0_{R})$
215	211 212 214	cbvrexw	$⊢ \exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists j \in {Base}_{R} j +_{R} a = 0_{R}$
216	215	rabbii	$⊢ \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} = \{a \in {Base}_{R} \| \exists j \in {Base}_{R} j +_{R} a = 0_{R}\}$
217	3 216	eqtri	$⊢ U = \{a \in {Base}_{R} \| \exists j \in {Base}_{R} j +_{R} a = 0_{R}\}$
218	217	eleq2i	$⊢ i \in U \leftrightarrow i \in \{a \in {Base}_{R} \| \exists j \in {Base}_{R} j +_{R} a = 0_{R}\}$
219		oveq2	$⊢ a = i \to j +_{R} a = j +_{R} i$
220	219	eqeq1d	$⊢ a = i \to (j +_{R} a = 0_{R} \leftrightarrow j +_{R} i = 0_{R})$
221	220	rexbidv	$⊢ a = i \to (\exists j \in {Base}_{R} j +_{R} a = 0_{R} \leftrightarrow \exists j \in {Base}_{R} j +_{R} i = 0_{R})$
222	221	elrab	$⊢ i \in \{a \in {Base}_{R} \| \exists j \in {Base}_{R} j +_{R} a = 0_{R}\} \leftrightarrow (i \in {Base}_{R} \land \exists j \in {Base}_{R} j +_{R} i = 0_{R})$
223	218 222	bitri	$⊢ i \in U \leftrightarrow (i \in {Base}_{R} \land \exists j \in {Base}_{R} j +_{R} i = 0_{R})$
224	210 223	sylibr	$⊢ ((φ \land q \in U) \land (i \in {Base}_{R} \land i +_{R} q = 0_{R})) \to i \in U$
225	197 224 207	reximssdv	$⊢ (φ \land q \in U) \to \exists i \in U i +_{R} q = 0_{R}$
226		fvexd	$⊢ φ \to {Base}_{R} \in V$
227	3 226	rabexd	$⊢ φ \to U \in V$
228	55 29	ressplusg	$⊢ U \in V \to +_{R} = +_{(R ↾_{𝑠} U)}$
229	227 228	syl	$⊢ φ \to +_{R} = +_{(R ↾_{𝑠} U)}$
230	229	eqcomd	$⊢ φ \to +_{(R ↾_{𝑠} U)} = +_{R}$
231	230	adantr	$⊢ (φ \land q \in U) \to +_{(R ↾_{𝑠} U)} = +_{R}$
232	231	adantr	$⊢ ((φ \land q \in U) \land w = i) \to +_{(R ↾_{𝑠} U)} = +_{R}$
233		simpr	$⊢ ((φ \land q \in U) \land w = i) \to w = i$
234		eqidd	$⊢ ((φ \land q \in U) \land w = i) \to q = q$
235	232 233 234	oveq123d	$⊢ ((φ \land q \in U) \land w = i) \to w +_{(R ↾_{𝑠} U)} q = i +_{R} q$
236	55 17 99	ress0g	$⊢ (R \in Mnd \land 0_{R} \in U \land U \subseteq {Base}_{R}) \to 0_{R} = 0_{(R ↾_{𝑠} U)}$
237	12 185 54 236	syl3anc	$⊢ φ \to 0_{R} = 0_{(R ↾_{𝑠} U)}$
238	237	eqcomd	$⊢ φ \to 0_{(R ↾_{𝑠} U)} = 0_{R}$
239	238	adantr	$⊢ (φ \land q \in U) \to 0_{(R ↾_{𝑠} U)} = 0_{R}$
240	239	adantr	$⊢ ((φ \land q \in U) \land w = i) \to 0_{(R ↾_{𝑠} U)} = 0_{R}$
241	235 240	eqeq12d	$⊢ ((φ \land q \in U) \land w = i) \to (w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)} \leftrightarrow i +_{R} q = 0_{R})$
242		eqidd	$⊢ ((φ \land q \in U) \land w = i) \to U = U$
243	241 242	cbvrexdva2	$⊢ (φ \land q \in U) \to (\exists w \in U w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)} \leftrightarrow \exists i \in U i +_{R} q = 0_{R})$
244	225 243	mpbird	$⊢ (φ \land q \in U) \to \exists w \in U w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)}$
245	57	eqcomd	$⊢ φ \to {Base}_{(R ↾_{𝑠} U)} = U$
246	245	adantr	$⊢ (φ \land q \in U) \to {Base}_{(R ↾_{𝑠} U)} = U$
247	244 246	rexeqtrrdv	$⊢ (φ \land q \in U) \to \exists w \in {Base}_{(R ↾_{𝑠} U)} w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)}$
248	247	ex	$⊢ φ \to (q \in U \to \exists w \in {Base}_{(R ↾_{𝑠} U)} w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)})$
249	57	eleq2d	$⊢ φ \to (q \in U \leftrightarrow q \in {Base}_{(R ↾_{𝑠} U)})$
250	249	imbi1d	$⊢ φ \to ((q \in U \to \exists w \in {Base}_{(R ↾_{𝑠} U)} w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)}) \leftrightarrow (q \in {Base}_{(R ↾_{𝑠} U)} \to \exists w \in {Base}_{(R ↾_{𝑠} U)} w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)}))$
251	248 250	mpbid	$⊢ φ \to (q \in {Base}_{(R ↾_{𝑠} U)} \to \exists w \in {Base}_{(R ↾_{𝑠} U)} w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)})$
252	251	imp	$⊢ (φ \land q \in {Base}_{(R ↾_{𝑠} U)}) \to \exists w \in {Base}_{(R ↾_{𝑠} U)} w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)}$
253	252	ralrimiva	$⊢ φ \to \forall q \in {Base}_{(R ↾_{𝑠} U)} \exists w \in {Base}_{(R ↾_{𝑠} U)} w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)}$
254	188 253	jca	$⊢ φ \to (R ↾_{𝑠} U \in Mnd \land \forall q \in {Base}_{(R ↾_{𝑠} U)} \exists w \in {Base}_{(R ↾_{𝑠} U)} w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)})$
255		eqid	$⊢ {Base}_{(R ↾_{𝑠} U)} = {Base}_{(R ↾_{𝑠} U)}$
256		eqid	$⊢ +_{(R ↾_{𝑠} U)} = +_{(R ↾_{𝑠} U)}$
257		eqid	$⊢ 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
258	255 256 257	isgrp	$⊢ R ↾_{𝑠} U \in Grp \leftrightarrow (R ↾_{𝑠} U \in Mnd \land \forall q \in {Base}_{(R ↾_{𝑠} U)} \exists w \in {Base}_{(R ↾_{𝑠} U)} w +_{(R ↾_{𝑠} U)} q = 0_{(R ↾_{𝑠} U)})$
259	254 258	sylibr	$⊢ φ \to R ↾_{𝑠} U \in Grp$
260	259	ad2antrr	$⊢ ((φ \land b \in U) \land d \in U) \to R ↾_{𝑠} U \in Grp$
261		simplr	$⊢ ((φ \land b \in U) \land d \in U) \to b \in U$
262	57	adantr	$⊢ (φ \land b \in U) \to U = {Base}_{(R ↾_{𝑠} U)}$
263	262	adantr	$⊢ ((φ \land b \in U) \land d \in U) \to U = {Base}_{(R ↾_{𝑠} U)}$
264	263	eleq2d	$⊢ ((φ \land b \in U) \land d \in U) \to (b \in U \leftrightarrow b \in {Base}_{(R ↾_{𝑠} U)})$
265	261 264	mpbid	$⊢ ((φ \land b \in U) \land d \in U) \to b \in {Base}_{(R ↾_{𝑠} U)}$
266		simpr	$⊢ ((φ \land b \in U) \land d \in U) \to d \in U$
267	263	eleq2d	$⊢ ((φ \land b \in U) \land d \in U) \to (d \in U \leftrightarrow d \in {Base}_{(R ↾_{𝑠} U)})$
268	266 267	mpbid	$⊢ ((φ \land b \in U) \land d \in U) \to d \in {Base}_{(R ↾_{𝑠} U)}$
269	255 256	grpcl	$⊢ (R ↾_{𝑠} U \in Grp \land b \in {Base}_{(R ↾_{𝑠} U)} \land d \in {Base}_{(R ↾_{𝑠} U)}) \to b +_{(R ↾_{𝑠} U)} d \in {Base}_{(R ↾_{𝑠} U)}$
270	260 265 268 269	syl3anc	$⊢ ((φ \land b \in U) \land d \in U) \to b +_{(R ↾_{𝑠} U)} d \in {Base}_{(R ↾_{𝑠} U)}$
271	263	eleq2d	$⊢ ((φ \land b \in U) \land d \in U) \to (b +_{(R ↾_{𝑠} U)} d \in U \leftrightarrow b +_{(R ↾_{𝑠} U)} d \in {Base}_{(R ↾_{𝑠} U)})$
272	270 271	mpbird	$⊢ ((φ \land b \in U) \land d \in U) \to b +_{(R ↾_{𝑠} U)} d \in U$
273	229	adantr	$⊢ (φ \land b \in U) \to +_{R} = +_{(R ↾_{𝑠} U)}$
274	273	oveqdr	$⊢ ((φ \land b \in U) \land d \in U) \to b +_{R} d = b +_{(R ↾_{𝑠} U)} d$
275	274	eleq1d	$⊢ ((φ \land b \in U) \land d \in U) \to (b +_{R} d \in U \leftrightarrow b +_{(R ↾_{𝑠} U)} d \in U)$
276	272 275	mpbird	$⊢ ((φ \land b \in U) \land d \in U) \to b +_{R} d \in U$
277	276	ralrimiva	$⊢ (φ \land b \in U) \to \forall d \in U b +_{R} d \in U$
278	277	ralrimiva	$⊢ φ \to \forall b \in U \forall d \in U b +_{R} d \in U$
279	278 187	mpbird	$⊢ φ \to R ↾_{𝑠} U \in Mnd$
280	12 279	jca	$⊢ φ \to (R \in Mnd \land R ↾_{𝑠} U \in Mnd)$
281	54 185	jca	$⊢ φ \to (U \subseteq {Base}_{R} \land 0_{R} \in U)$
282	280 281	jca	$⊢ φ \to ((R \in Mnd \land R ↾_{𝑠} U \in Mnd) \land (U \subseteq {Base}_{R} \land 0_{R} \in U))$
283	17 99	issubmndb	$⊢ U \in SubMnd (R) \leftrightarrow ((R \in Mnd \land R ↾_{𝑠} U \in Mnd) \land (U \subseteq {Base}_{R} \land 0_{R} \in U))$
284	282 283	sylibr	$⊢ φ \to U \in SubMnd (R)$
285	284	adantr	$⊢ (φ \land c \in (R PrimRoots K)) \to U \in SubMnd (R)$
286	285 6 43	3jca	$⊢ (φ \land c \in (R PrimRoots K)) \to (U \in SubMnd (R) \land K \in ℕ_{0} \land c \in U)$
287		eqid	$⊢ \cdot_{(R ↾_{𝑠} U)} = \cdot_{(R ↾_{𝑠} U)}$
288	7 55 287	submmulg	$⊢ (U \in SubMnd (R) \land K \in ℕ_{0} \land c \in U) \to K \cdot_{R} c = K \cdot_{(R ↾_{𝑠} U)} c$
289	288	eqcomd	$⊢ (U \in SubMnd (R) \land K \in ℕ_{0} \land c \in U) \to K \cdot_{(R ↾_{𝑠} U)} c = K \cdot_{R} c$
290	286 289	syl	$⊢ (φ \land c \in (R PrimRoots K)) \to K \cdot_{(R ↾_{𝑠} U)} c = K \cdot_{R} c$
291	238	adantr	$⊢ (φ \land c \in (R PrimRoots K)) \to 0_{(R ↾_{𝑠} U)} = 0_{R}$
292	290 291	eqeq12d	$⊢ (φ \land c \in (R PrimRoots K)) \to (K \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \leftrightarrow K \cdot_{R} c = 0_{R})$
293	33 292	mpbird	$⊢ (φ \land c \in (R PrimRoots K)) \to K \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)}$
294	10	simp3d	$⊢ (φ \land c \in (R PrimRoots K)) \to \forall l \in ℕ_{0} (l \cdot_{R} c = 0_{R} \to K ∥ l)$
295		eqidd	$⊢ (φ \land c \in (R PrimRoots K)) \to ℕ_{0} = ℕ_{0}$
296	285	adantr	$⊢ ((φ \land c \in (R PrimRoots K)) \land l \in ℕ_{0}) \to U \in SubMnd (R)$
297		simpr	$⊢ ((φ \land c \in (R PrimRoots K)) \land l \in ℕ_{0}) \to l \in ℕ_{0}$
298	43	adantr	$⊢ ((φ \land c \in (R PrimRoots K)) \land l \in ℕ_{0}) \to c \in U$
299	296 297 298	3jca	$⊢ ((φ \land c \in (R PrimRoots K)) \land l \in ℕ_{0}) \to (U \in SubMnd (R) \land l \in ℕ_{0} \land c \in U)$
300	7 55 287	submmulg	$⊢ (U \in SubMnd (R) \land l \in ℕ_{0} \land c \in U) \to l \cdot_{R} c = l \cdot_{(R ↾_{𝑠} U)} c$
301	299 300	syl	$⊢ ((φ \land c \in (R PrimRoots K)) \land l \in ℕ_{0}) \to l \cdot_{R} c = l \cdot_{(R ↾_{𝑠} U)} c$
302	237	ad2antrr	$⊢ ((φ \land c \in (R PrimRoots K)) \land l \in ℕ_{0}) \to 0_{R} = 0_{(R ↾_{𝑠} U)}$
303	301 302	eqeq12d	$⊢ ((φ \land c \in (R PrimRoots K)) \land l \in ℕ_{0}) \to (l \cdot_{R} c = 0_{R} \leftrightarrow l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)})$
304	303	imbi1d	$⊢ ((φ \land c \in (R PrimRoots K)) \land l \in ℕ_{0}) \to ((l \cdot_{R} c = 0_{R} \to K ∥ l) \leftrightarrow (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
305	295 304	raleqbidva	$⊢ (φ \land c \in (R PrimRoots K)) \to (\forall l \in ℕ_{0} (l \cdot_{R} c = 0_{R} \to K ∥ l) \leftrightarrow \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
306	294 305	mpbid	$⊢ (φ \land c \in (R PrimRoots K)) \to \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l)$
307	60 293 306	3jca	$⊢ (φ \land c \in (R PrimRoots K)) \to (c \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
308	1	3ad2ant1	$⊢ (φ \land b \in U \land d \in U) \to R \in CMnd$
309	62	3impa	$⊢ (φ \land b \in U \land d \in U) \to b \in {Base}_{R}$
310	71	3impa	$⊢ (φ \land b \in U \land d \in U) \to d \in {Base}_{R}$
311	17 29	cmncom	$⊢ (R \in CMnd \land b \in {Base}_{R} \land d \in {Base}_{R}) \to b +_{R} d = d +_{R} b$
312	308 309 310 311	syl3anc	$⊢ (φ \land b \in U \land d \in U) \to b +_{R} d = d +_{R} b$
313	57 229 279 312	iscmnd	$⊢ φ \to R ↾_{𝑠} U \in CMnd$
314	313 5 287	isprimroot	$⊢ φ \to (c \in ((R ↾_{𝑠} U) PrimRoots K) \leftrightarrow (c \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
315	314	adantr	$⊢ (φ \land c \in (R PrimRoots K)) \to (c \in ((R ↾_{𝑠} U) PrimRoots K) \leftrightarrow (c \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
316	307 315	mpbird	$⊢ (φ \land c \in (R PrimRoots K)) \to c \in ((R ↾_{𝑠} U) PrimRoots K)$
317	316	ex	$⊢ φ \to (c \in (R PrimRoots K) \to c \in ((R ↾_{𝑠} U) PrimRoots K))$
318	317	ssrdv	$⊢ φ \to R PrimRoots K \subseteq (R ↾_{𝑠} U) PrimRoots K$
319	313	adantr	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to R ↾_{𝑠} U \in CMnd$
320	5	adantr	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to K \in ℕ_{0}$
321	319 320 287	isprimroot	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to (c \in ((R ↾_{𝑠} U) PrimRoots K) \leftrightarrow (c \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
322	321	biimpd	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to (c \in ((R ↾_{𝑠} U) PrimRoots K) \to (c \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
323	322	syldbl2	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to (c \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
324	323	simp1d	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to c \in {Base}_{(R ↾_{𝑠} U)}$
325	54	sselda	$⊢ (φ \land c \in U) \to c \in {Base}_{R}$
326	325	ex	$⊢ φ \to (c \in U \to c \in {Base}_{R})$
327	57	eleq2d	$⊢ φ \to (c \in U \leftrightarrow c \in {Base}_{(R ↾_{𝑠} U)})$
328	327	imbi1d	$⊢ φ \to ((c \in U \to c \in {Base}_{R}) \leftrightarrow (c \in {Base}_{(R ↾_{𝑠} U)} \to c \in {Base}_{R}))$
329	326 328	mpbid	$⊢ φ \to (c \in {Base}_{(R ↾_{𝑠} U)} \to c \in {Base}_{R})$
330	329	adantr	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to (c \in {Base}_{(R ↾_{𝑠} U)} \to c \in {Base}_{R})$
331	330	imp	$⊢ ((φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \land c \in {Base}_{(R ↾_{𝑠} U)}) \to c \in {Base}_{R}$
332	324 331	mpdan	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to c \in {Base}_{R}$
333	284	adantr	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to U \in SubMnd (R)$
334	327	adantr	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to (c \in U \leftrightarrow c \in {Base}_{(R ↾_{𝑠} U)})$
335	324 334	mpbird	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to c \in U$
336	333 320 335 288	syl3anc	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to K \cdot_{R} c = K \cdot_{(R ↾_{𝑠} U)} c$
337	323	simp2d	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to K \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)}$
338	238	adantr	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to 0_{(R ↾_{𝑠} U)} = 0_{R}$
339	336 337 338	3eqtrd	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to K \cdot_{R} c = 0_{R}$
340	323	simp3d	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l)$
341	333	adantr	$⊢ ((φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \land l \in ℕ_{0}) \to U \in SubMnd (R)$
342		simpr	$⊢ ((φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \land l \in ℕ_{0}) \to l \in ℕ_{0}$
343	335	adantr	$⊢ ((φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \land l \in ℕ_{0}) \to c \in U$
344	341 342 343 300	syl3anc	$⊢ ((φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \land l \in ℕ_{0}) \to l \cdot_{R} c = l \cdot_{(R ↾_{𝑠} U)} c$
345	344	eqcomd	$⊢ ((φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \land l \in ℕ_{0}) \to l \cdot_{(R ↾_{𝑠} U)} c = l \cdot_{R} c$
346	338	adantr	$⊢ ((φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \land l \in ℕ_{0}) \to 0_{(R ↾_{𝑠} U)} = 0_{R}$
347	345 346	eqeq12d	$⊢ ((φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \land l \in ℕ_{0}) \to (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \leftrightarrow l \cdot_{R} c = 0_{R})$
348	347	imbi1d	$⊢ ((φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \land l \in ℕ_{0}) \to ((l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l) \leftrightarrow (l \cdot_{R} c = 0_{R} \to K ∥ l))$
349	348	ralbidva	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to (\forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} c = 0_{(R ↾_{𝑠} U)} \to K ∥ l) \leftrightarrow \forall l \in ℕ_{0} (l \cdot_{R} c = 0_{R} \to K ∥ l))$
350	340 349	mpbid	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to \forall l \in ℕ_{0} (l \cdot_{R} c = 0_{R} \to K ∥ l)$
351	332 339 350	3jca	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to (c \in {Base}_{R} \land K \cdot_{R} c = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} c = 0_{R} \to K ∥ l))$
352	1	adantr	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to R \in CMnd$
353	352 320 7	isprimroot	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to (c \in (R PrimRoots K) \leftrightarrow (c \in {Base}_{R} \land K \cdot_{R} c = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} c = 0_{R} \to K ∥ l)))$
354	351 353	mpbird	$⊢ (φ \land c \in ((R ↾_{𝑠} U) PrimRoots K)) \to c \in (R PrimRoots K)$
355	354	ex	$⊢ φ \to (c \in ((R ↾_{𝑠} U) PrimRoots K) \to c \in (R PrimRoots K))$
356	355	ssrdv	$⊢ φ \to (R ↾_{𝑠} U) PrimRoots K \subseteq R PrimRoots K$
357	318 356	eqssd	$⊢ φ \to R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K$
358	259 313	jca	$⊢ φ \to (R ↾_{𝑠} U \in Grp \land R ↾_{𝑠} U \in CMnd)$
359		isabl	$⊢ R ↾_{𝑠} U \in Abel \leftrightarrow (R ↾_{𝑠} U \in Grp \land R ↾_{𝑠} U \in CMnd)$
360	358 359	sylibr	$⊢ φ \to R ↾_{𝑠} U \in Abel$
361	357 360	jca	$⊢ φ \to (R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K \land R ↾_{𝑠} U \in Abel)$

Metamath Proof Explorer

Theorem primrootsunit1

Proof