Theorem primrootsunit1 43115

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

Hypotheses

Ref	Expression
primrootsunit1.1	⊢ (𝜑 → 𝑅 ∈ CMnd)
primrootsunit1.2	⊢ (𝜑 → 𝐾 ∈ ℕ)
primrootsunit1.3	⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}

Assertion

Ref	Expression
primrootsunit1	⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))

Distinct variable groups:   𝑖,𝐾   𝑅,𝑎,𝑖   𝑈,𝑖   𝜑,𝑖

Allowed substitution hints:   𝜑(𝑎)   𝑈(𝑎)   𝐾(𝑎)

Proof of Theorem primrootsunit1

Dummy variables 𝑐 𝑙 𝑏 𝑑 𝑗 𝑞 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		primrootsunit1.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ CMnd)
2	1	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
3		primrootsunit1.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℕ)
4	3	nnnn0d 12648	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
5	4	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
6		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (.g‘𝑅) = (.g‘𝑅)
7	2, 5, 6	isprimroot 43111	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
8	7	biimpd 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
9	8	syldbl2 855	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
10	9	simp1d 1160	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
11	1	cmnmndd 19998	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Mnd)
12	11	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
13		nnm1nn0 12628	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
14	3, 13	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 − 1) ∈ ℕ0)
15	14	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾 − 1) ∈ ℕ0)
16		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑅) = (Base‘𝑅)
17	16, 6	mulgnn0cl 19280	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
18	12, 15, 10, 17	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
19		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐))
20	19	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → (𝑖(+g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
21	20	eqeq1d 2763	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → ((𝑖(+g‘𝑅)𝑐) = (0g‘𝑅) ↔ (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅)))
22	3	nncnd 12332	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℂ)
23		1cnd 11283	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℂ)
24	22, 23	npcand 11654	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
25	24	eqcomd 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 = ((𝐾 − 1) + 1))
26	25	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 = ((𝐾 − 1) + 1))
27	26	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (((𝐾 − 1) + 1)(.g‘𝑅)𝑐))
28		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (+g‘𝑅) = (+g‘𝑅)
29	16, 6, 28	mulgnn0p1 19275	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
30	12, 15, 10, 29	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
31	27, 30	eqtr2d 2797	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (𝐾(.g‘𝑅)𝑐))
32	9	simp2d 1161	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
33	31, 32	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅))
34	18, 21, 33	rspcedvd 3579	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))
35	10, 34	jca 521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
36		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑐))
37	36	eqeq1d 2763	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
38	37	rexbidv 3187	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
39	38	elrab 3645	. . . . . . . . . 10 ⊢ (𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
40	35, 39	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
41		primrootsunit1.3	. . . . . . . . . 10 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}
42	41	eleq2i 2853	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
43	40, 42	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
44		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝜑)
45	41	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
46	45	eleq2d 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
47	46	biimpd 232	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
48	47	imp 412	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
49	44, 48	jca 521	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
50		elrabi 3641	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑏 ∈ (Base‘𝑅))
51	50	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑏 ∈ (Base‘𝑅))
52	49, 51	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
53	52	ex 418	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ (Base‘𝑅)))
54	53	ssrdv 3937	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
55		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
56	55, 16	ressbas2 17396	. . . . . . . . . . 11 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
57	54, 56	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
58	57	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
59	58	eleq2d 2847	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
60	43, 59	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
61	11	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ Mnd)
62	52	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
63		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝜑)
64	45	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
65	64	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑑 ∈ 𝑈 → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
66	65	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
67	63, 66	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → (𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
68		elrabi 3641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑑 ∈ (Base‘𝑅))
69	68	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑑 ∈ (Base‘𝑅))
70	67, 69	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
71	44, 70	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
72	16, 28	mndcl 18911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
73	61, 62, 71, 72	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
74	41	eleq2i 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
75		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑑 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑑))
76	75	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑑 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
77	76	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑑 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
78	77	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
79	74, 78	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑑 ∈ 𝑈 ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
80	79	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑑 ∈ 𝑈 → (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
81	80	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑑 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
82	81	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
83	1	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
84	71	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑑 ∈ (Base‘𝑅))
85		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
86	16, 28	cmncom 19992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑑 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
87	83, 84, 85, 86	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
88		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
89	87, 88	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
90	89	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
91	90	reximdva 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
92	82, 91	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
93	16, 61, 71, 92	mndmolinv 43113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
94	82, 93	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
95		reu5 3368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
96	94, 95	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
97		riotacl 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
98	96, 97	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
99		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (0g‘𝑅) = (0g‘𝑅)
100		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (invg‘𝑅) = (invg‘𝑅)
101	16, 28, 99, 100	grpinvval 19171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
102	71, 101	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
103	102	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅)))
104	98, 103	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅))
105	41	eleq2i 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
106		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑏 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑏))
107	106	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑏 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
108	107	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑏 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
109	108	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
110	105, 109	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑏 ∈ 𝑈 ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
111	110	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑏 ∈ 𝑈 → (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
112	111	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑏 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
113	112	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
114	1	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
115	62	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑏 ∈ (Base‘𝑅))
116		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
117	16, 28	cmncom 19992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
118	114, 115, 116, 117	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
119		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
120	118, 119	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
121	120	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
122	121	reximdva 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
123	113, 122	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
124	16, 61, 62, 123	mndmolinv 43113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
125	113, 124	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
126		reu5 3368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
127	125, 126	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
128		riotacl 7386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
129	127, 128	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
130	16, 28, 99, 100	grpinvval 19171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑏 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
131	62, 130	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
132	131	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅)))
133	129, 132	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅))
134	16, 28	mndcl 18911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 ∈ Mnd ∧ ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅)) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
135	61, 104, 133, 134	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
136		oveq1 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
137	136	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
138	137	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
139	104, 133, 73	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅)))
140	16, 28	mndass 18912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
141	61, 139, 140	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
142	133, 62, 71	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)))
143	16, 28	mndass 18912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
144	143	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
145	61, 142, 144	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
146	145	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)))
147	62, 127	linvh 43114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏) = (0g‘𝑅))
148	147	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = ((0g‘𝑅)(+g‘𝑅)𝑑))
149	148	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)))
150	16, 28, 99	mndlid 18924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑅 ∈ Mnd ∧ 𝑑 ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
151	61, 71, 150	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
152	151	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑))
153	71, 96	linvh 43114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑) = (0g‘𝑅))
154	152, 153	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (0g‘𝑅))
155	149, 154	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (0g‘𝑅))
156	146, 155	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (0g‘𝑅))
157	141, 156	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
158	135, 138, 157	rspcedvd 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
159	73, 158	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
160		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
161	160	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
162	161	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
163	162	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
164	159, 163	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
165	41	eleq2i 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
166	165	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
167	164, 166	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
168	167	ralrimiva 3155	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
169	168	ralrimiva 3155	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
170		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
171	170	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
172	171	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
173	16, 99	mndidcl 18919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
174	11, 173	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
175	11, 174	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)))
176	16, 28, 99	mndlid 18924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
177	175, 176	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
178	174, 177	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((0g‘𝑅) ∈ (Base‘𝑅) ∧ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
179		oveq1 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (0g‘𝑅) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
180	179	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = (0g‘𝑅) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
181	180	rspcev 3577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((0g‘𝑅) ∈ (Base‘𝑅) ∧ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
182	178, 181	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
183	172, 174, 182	elrabd 3647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
184	45	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((0g‘𝑅) ∈ 𝑈 ↔ (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
185	183, 184	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑈)
186	16, 28, 99, 55	issubmnd 18933	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Mnd ∧ 𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈) → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
187	11, 54, 185, 186	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
188	169, 187	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
189	45	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
190	189	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
191	190	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
192		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑞 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑞))
193	192	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑞 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
194	193	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑞 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
195	194	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
196	191, 195	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
197	196	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
198		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ (Base‘𝑅))
199	196	simpld 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ (Base‘𝑅))
200	199	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑞 ∈ (Base‘𝑅))
201		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → 𝑗 = 𝑞)
202	201	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → (𝑗(+g‘𝑅)𝑖) = (𝑞(+g‘𝑅)𝑖))
203	202	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → ((𝑗(+g‘𝑅)𝑖) = (0g‘𝑅) ↔ (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅)))
204	1	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑅 ∈ CMnd)
205	16, 28	cmncom 19992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ CMnd ∧ 𝑖 ∈ (Base‘𝑅) ∧ 𝑞 ∈ (Base‘𝑅)) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
206	204, 198, 200, 205	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
207		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
208	206, 207	eqtr3d 2798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅))
209	200, 203, 208	rspcedvd 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅))
210	198, 209	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
211		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑗(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)
212		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑖(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)
213		oveq1 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑖 = 𝑗 → (𝑖(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑎))
214	213	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑖 = 𝑗 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)))
215	211, 212, 214	cbvrexw 3306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅))
216	215	rabbii 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
217	41, 216	eqtri 2784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
218	217	eleq2i 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ 𝑈 ↔ 𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)})
219		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑖 → (𝑗(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑖))
220	219	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑖 → ((𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
221	220	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑖 → (∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
222	221	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
223	218, 222	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑈 ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
224	210, 223	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ 𝑈)
225	197, 224, 207	reximssdv 3181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
226		fvexd 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
227	41, 226	rabexd 5301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → 𝑈 ∈ V)
228	55, 28	ressplusg 17442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑈 ∈ V → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
229	227, 228	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
230	229	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
231	230	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
232	231	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
233		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑤 = 𝑖)
234		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑞 = 𝑞)
235	232, 233, 234	oveq123d 7433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (𝑖(+g‘𝑅)𝑞))
236	55, 16, 99	ress0g 18934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝑅)) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
237	11, 185, 54, 236	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
238	237	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
239	238	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
240	239	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
241	235, 240	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → ((𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
242		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑈 = 𝑈)
243	241, 242	cbvrexdva2 3338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
244	225, 243	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
245	57	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
246	245	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
247	244, 246	rexeqtrrdv 3325	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
248	247	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
249	57	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))))
250	249	imbi1d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))) ↔ (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))))
251	248, 250	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
252	251	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
253	252	ralrimiva 3155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
254	188, 253	jca 521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
255		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
256		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
257		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
258	255, 256, 257	isgrp 19130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp ↔ ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
259	254, 258	sylibr 237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
260	259	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑅 ↾s 𝑈) ∈ Grp)
261		simplr 781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ 𝑈)
262	57	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
263	262	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
264	263	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈))))
265	261, 264	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)))
266		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ 𝑈)
267	263	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))))
268	266, 267	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈)))
269	255, 256	grpcl 19132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
270	260, 265, 268, 269	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
271	263	eleq2d 2847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈))))
272	270, 271	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈)
273	229	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
274	273	oveqdr 7440	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑))
275	274	eleq1d 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈))
276	272, 275	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
277	276	ralrimiva 3155	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
278	277	ralrimiva 3155	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
279	278, 187	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
280	11, 279	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd))
281	54, 185	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈))
282	280, 281	jca 521	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
283	16, 99	issubmndb 18980	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubMnd‘𝑅) ↔ ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
284	282, 283	sylibr 237	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘𝑅))
285	284	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
286	285, 5, 43	3jca 1146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
287		eqid 2761	. . . . . . . . . . . 12 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
288	6, 55, 287	submmulg 19308	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
289	288	eqcomd 2767	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
290	286, 289	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
291	238	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
292	290, 291	eqeq12d 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅)))
293	32, 292	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
294	9	simp3d 1162	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
295		eqidd 2762	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ℕ0 = ℕ0)
296	285	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
297		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
298	43	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
299	296, 297, 298	3jca 1146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
300	6, 55, 287	submmulg 19308	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
301	299, 300	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
302	237	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
303	301, 302	eqeq12d 2777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) ↔ (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈))))
304	303	imbi1d 344	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
305	295, 304	raleqbidva 3326	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
306	294, 305	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
307	60, 293, 306	3jca 1146	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
308	1	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ CMnd)
309	62	3impa 1127	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
310	71	3impa 1127	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
311	16, 28	cmncom 19992	. . . . . . . . . 10 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
312	308, 309, 310, 311	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
313	57, 229, 279, 312	iscmnd 19988	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
314	313, 4, 287	isprimroot 43111	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
315	314	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
316	307, 315	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
317	316	ex 418	. . . 4 ⊢ (𝜑 → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
318	317	ssrdv 3937	. . 3 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
319	313	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ CMnd)
320	4	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
321	319, 320, 287	isprimroot 43111	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
322	321	biimpd 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
323	322	syldbl2 855	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
324	323	simp1d 1160	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
325	54	sselda 3931	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑈) → 𝑐 ∈ (Base‘𝑅))
326	325	ex 418	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)))
327	57	eleq2d 2847	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
328	327	imbi1d 344	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅))))
329	326, 328	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
330	329	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
331	330	imp 412	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))) → 𝑐 ∈ (Base‘𝑅))
332	324, 331	mpdan 700	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
333	284	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
334	327	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
335	324, 334	mpbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
336	333, 320, 335, 288	syl3anc 1398	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
337	323	simp2d 1161	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
338	238	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
339	336, 337, 338	3eqtrd 2800	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
340	323	simp3d 1162	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
341	333	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
342		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
343	335	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
344	341, 342, 343, 300	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
345	344	eqcomd 2767	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝑙(.g‘𝑅)𝑐))
346	338	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
347	345, 346	eqeq12d 2777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑙(.g‘𝑅)𝑐) = (0g‘𝑅)))
348	347	imbi1d 344	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
349	348	ralbidva 3184	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
350	340, 349	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
351	332, 339, 350	3jca 1146	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
352	1	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
353	352, 320, 6	isprimroot 43111	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
354	351, 353	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (𝑅 PrimRoots 𝐾))
355	354	ex 418	. . . 4 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑐 ∈ (𝑅 PrimRoots 𝐾)))
356	355	ssrdv 3937	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ (𝑅 PrimRoots 𝐾))
357	318, 356	eqssd 3948	. 2 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
358	259, 313	jca 521	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
359		isabl 19978	. . 3 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel ↔ ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
360	358, 359	sylibr 237	. 2 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
361	357, 360	jca 521	1 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  ∃!wreu 3364  ∃*wrmo 3365  {crab 3413  Vcvv 3451   ⊆ wss 3899   class class class wbr 5103  ‘cfv 6531  ℩crio 7368  (class class class)co 7412  1c1 11182   + caddc 11184   − cmin 11522  ℕcn 12316  ℕ₀cn0 12587   ∥ cdvds 16402  Basecbs 17367   ↾_s cress 17388  +_gcplusg 17408  0_gc0g 17590  Mndcmnd 18903  SubMndcsubmnd 18957  Grpcgrp 19124  inv_gcminusg 19125  ._gcmg 19257  CMndccmn 19974  Abelcabl 19975   PrimRoots cprimroots 43109

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-er 8701  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-nn 12317  df-2 12386  df-n0 12588  df-z 12675  df-uz 12947  df-fz 13621  df-seq 14125  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-ress 17389  df-plusg 17421  df-0g 17592  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-submnd 18959  df-grp 19127  df-minusg 19128  df-mulg 19258  df-cmn 19976  df-abl 19977  df-primroots 43110

This theorem is used by:  primrootsunit  43116