Theorem primrootsunit1 42098

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 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
3		primrootsunit1.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℕ)
4	3	nnnn0d 12587	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
5	4	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
6		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (.g‘𝑅) = (.g‘𝑅)
7	2, 5, 6	isprimroot 42094	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
8	7	biimpd 229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
9	8	syldbl2 842	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
10	9	simp1d 1143	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
11	1	cmnmndd 19822	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Mnd)
12	11	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
13		nnm1nn0 12567	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
14	3, 13	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 − 1) ∈ ℕ0)
15	14	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾 − 1) ∈ ℕ0)
16		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑅) = (Base‘𝑅)
17	16, 6	mulgnn0cl 19108	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
18	12, 15, 10, 17	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
19		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐))
20	19	oveq1d 7446	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → (𝑖(+g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
21	20	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → ((𝑖(+g‘𝑅)𝑐) = (0g‘𝑅) ↔ (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅)))
22	3	nncnd 12282	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℂ)
23		1cnd 11256	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℂ)
24	22, 23	npcand 11624	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
25	24	eqcomd 2743	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 = ((𝐾 − 1) + 1))
26	25	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 = ((𝐾 − 1) + 1))
27	26	oveq1d 7446	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (((𝐾 − 1) + 1)(.g‘𝑅)𝑐))
28		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (+g‘𝑅) = (+g‘𝑅)
29	16, 6, 28	mulgnn0p1 19103	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
30	12, 15, 10, 29	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
31	27, 30	eqtr2d 2778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (𝐾(.g‘𝑅)𝑐))
32	9	simp2d 1144	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
33	31, 32	eqtrd 2777	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅))
34	18, 21, 33	rspcedvd 3624	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))
35	10, 34	jca 511	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
36		oveq2 7439	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑐))
37	36	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
38	37	rexbidv 3179	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
39	38	elrab 3692	. . . . . . . . . 10 ⊢ (𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
40	35, 39	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
41		primrootsunit1.3	. . . . . . . . . 10 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}
42	41	eleq2i 2833	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
43	40, 42	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
44		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝜑)
45	41	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
46	45	eleq2d 2827	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
47	46	biimpd 229	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
48	47	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
49	44, 48	jca 511	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
50		elrabi 3687	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑏 ∈ (Base‘𝑅))
51	50	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑏 ∈ (Base‘𝑅))
52	49, 51	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
53	52	ex 412	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ (Base‘𝑅)))
54	53	ssrdv 3989	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
55		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
56	55, 16	ressbas2 17283	. . . . . . . . . . 11 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
57	54, 56	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
58	57	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
59	58	eleq2d 2827	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
60	43, 59	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
61	11	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ Mnd)
62	52	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
63		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝜑)
64	45	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
65	64	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑑 ∈ 𝑈 → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
66	65	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
67	63, 66	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → (𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
68		elrabi 3687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑑 ∈ (Base‘𝑅))
69	68	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑑 ∈ (Base‘𝑅))
70	67, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
71	44, 70	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
72	16, 28	mndcl 18755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
73	61, 62, 71, 72	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
74	41	eleq2i 2833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
75		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑑 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑑))
76	75	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑑 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
77	76	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑑 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
78	77	elrab 3692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
79	74, 78	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑑 ∈ 𝑈 ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
80	79	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑑 ∈ 𝑈 → (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
81	80	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑑 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
82	81	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
83	1	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
84	71	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑑 ∈ (Base‘𝑅))
85		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
86	16, 28	cmncom 19816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑑 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
87	83, 84, 85, 86	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
88		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
89	87, 88	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
90	89	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
91	90	reximdva 3168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
92	82, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
93	16, 61, 71, 92	mndmolinv 42096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
94	82, 93	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
95		reu5 3382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
96	94, 95	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
97		riotacl 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
99		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (0g‘𝑅) = (0g‘𝑅)
100		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (invg‘𝑅) = (invg‘𝑅)
101	16, 28, 99, 100	grpinvval 18998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
102	71, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
103	102	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅)))
104	98, 103	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅))
105	41	eleq2i 2833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
106		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑏 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑏))
107	106	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑏 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
108	107	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑏 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
109	108	elrab 3692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
110	105, 109	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑏 ∈ 𝑈 ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
111	110	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑏 ∈ 𝑈 → (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
112	111	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑏 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
113	112	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
114	1	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
115	62	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑏 ∈ (Base‘𝑅))
116		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
117	16, 28	cmncom 19816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
118	114, 115, 116, 117	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
119		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
120	118, 119	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
121	120	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
122	121	reximdva 3168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
123	113, 122	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
124	16, 61, 62, 123	mndmolinv 42096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
125	113, 124	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
126		reu5 3382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
127	125, 126	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
128		riotacl 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
130	16, 28, 99, 100	grpinvval 18998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑏 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
131	62, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
132	131	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅)))
133	129, 132	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅))
134	16, 28	mndcl 18755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 ∈ Mnd ∧ ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅)) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
135	61, 104, 133, 134	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
136		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
137	136	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
138	137	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
139	104, 133, 73	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅)))
140	16, 28	mndass 18756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
141	61, 139, 140	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
142	133, 62, 71	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)))
143	16, 28	mndass 18756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
144	143	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
145	61, 142, 144	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
146	145	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)))
147	62, 127	linvh 42097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏) = (0g‘𝑅))
148	147	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = ((0g‘𝑅)(+g‘𝑅)𝑑))
149	148	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)))
150	16, 28, 99	mndlid 18767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑅 ∈ Mnd ∧ 𝑑 ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
151	61, 71, 150	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
152	151	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑))
153	71, 96	linvh 42097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑) = (0g‘𝑅))
154	152, 153	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (0g‘𝑅))
155	149, 154	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (0g‘𝑅))
156	146, 155	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (0g‘𝑅))
157	141, 156	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
158	135, 138, 157	rspcedvd 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
159	73, 158	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
160		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
161	160	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
162	161	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
163	162	elrab 3692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
164	159, 163	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
165	41	eleq2i 2833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
166	165	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
167	164, 166	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
168	167	ralrimiva 3146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
169	168	ralrimiva 3146	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
170		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
171	170	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
172	171	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
173	16, 99	mndidcl 18762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
174	11, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
175	11, 174	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)))
176	16, 28, 99	mndlid 18767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
178	174, 177	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((0g‘𝑅) ∈ (Base‘𝑅) ∧ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
179		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (0g‘𝑅) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
180	179	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = (0g‘𝑅) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
181	180	rspcev 3622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((0g‘𝑅) ∈ (Base‘𝑅) ∧ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
182	178, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
183	172, 174, 182	elrabd 3694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
184	45	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((0g‘𝑅) ∈ 𝑈 ↔ (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
185	183, 184	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑈)
186	16, 28, 99, 55	issubmnd 18774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Mnd ∧ 𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈) → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
187	11, 54, 185, 186	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
188	169, 187	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
189	45	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
190	189	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
191	190	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
192		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑞 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑞))
193	192	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑞 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
194	193	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑞 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
195	194	elrab 3692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
196	191, 195	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
197	196	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
198		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ (Base‘𝑅))
199	196	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ (Base‘𝑅))
200	199	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑞 ∈ (Base‘𝑅))
201		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → 𝑗 = 𝑞)
202	201	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → (𝑗(+g‘𝑅)𝑖) = (𝑞(+g‘𝑅)𝑖))
203	202	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → ((𝑗(+g‘𝑅)𝑖) = (0g‘𝑅) ↔ (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅)))
204	1	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑅 ∈ CMnd)
205	16, 28	cmncom 19816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ CMnd ∧ 𝑖 ∈ (Base‘𝑅) ∧ 𝑞 ∈ (Base‘𝑅)) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
206	204, 198, 200, 205	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
207		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
208	206, 207	eqtr3d 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅))
209	200, 203, 208	rspcedvd 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅))
210	198, 209	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
211		nfv 1914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑗(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)
212		nfv 1914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑖(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)
213		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑖 = 𝑗 → (𝑖(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑎))
214	213	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑖 = 𝑗 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)))
215	211, 212, 214	cbvrexw 3307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅))
216	215	rabbii 3442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
217	41, 216	eqtri 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
218	217	eleq2i 2833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ 𝑈 ↔ 𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)})
219		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑖 → (𝑗(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑖))
220	219	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑖 → ((𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
221	220	rexbidv 3179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑖 → (∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
222	221	elrab 3692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
223	218, 222	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑈 ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
224	210, 223	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ 𝑈)
225	197, 224, 207	reximssdv 3173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
226		fvexd 6921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
227	41, 226	rabexd 5340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → 𝑈 ∈ V)
228	55, 28	ressplusg 17334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑈 ∈ V → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
229	227, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
230	229	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
231	230	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
232	231	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
233		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑤 = 𝑖)
234		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑞 = 𝑞)
235	232, 233, 234	oveq123d 7452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (𝑖(+g‘𝑅)𝑞))
236	55, 16, 99	ress0g 18775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝑅)) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
237	11, 185, 54, 236	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
238	237	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
239	238	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
240	239	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
241	235, 240	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → ((𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
242		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑈 = 𝑈)
243	241, 242	cbvrexdva2 3349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
244	225, 243	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
245	57	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
246	245	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
247	244, 246	rexeqtrrdv 3331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
248	247	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
249	57	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))))
250	249	imbi1d 341	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))) ↔ (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))))
251	248, 250	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
252	251	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
253	252	ralrimiva 3146	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
254	188, 253	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
255		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
256		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
257		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
258	255, 256, 257	isgrp 18957	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp ↔ ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
259	254, 258	sylibr 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
260	259	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑅 ↾s 𝑈) ∈ Grp)
261		simplr 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ 𝑈)
262	57	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
263	262	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
264	263	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈))))
265	261, 264	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)))
266		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ 𝑈)
267	263	eleq2d 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))))
268	266, 267	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈)))
269	255, 256	grpcl 18959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
270	260, 265, 268, 269	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
271	263	eleq2d 2827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈))))
272	270, 271	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈)
273	229	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
274	273	oveqdr 7459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑))
275	274	eleq1d 2826	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈))
276	272, 275	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
277	276	ralrimiva 3146	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
278	277	ralrimiva 3146	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
279	278, 187	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
280	11, 279	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd))
281	54, 185	jca 511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈))
282	280, 281	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
283	16, 99	issubmndb 18818	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubMnd‘𝑅) ↔ ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
284	282, 283	sylibr 234	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘𝑅))
285	284	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
286	285, 5, 43	3jca 1129	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
287		eqid 2737	. . . . . . . . . . . 12 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
288	6, 55, 287	submmulg 19136	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
289	288	eqcomd 2743	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
290	286, 289	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
291	238	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
292	290, 291	eqeq12d 2753	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅)))
293	32, 292	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
294	9	simp3d 1145	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
295		eqidd 2738	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ℕ0 = ℕ0)
296	285	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
297		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
298	43	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
299	296, 297, 298	3jca 1129	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
300	6, 55, 287	submmulg 19136	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
301	299, 300	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
302	237	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
303	301, 302	eqeq12d 2753	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) ↔ (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈))))
304	303	imbi1d 341	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
305	295, 304	raleqbidva 3332	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
306	294, 305	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
307	60, 293, 306	3jca 1129	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
308	1	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ CMnd)
309	62	3impa 1110	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
310	71	3impa 1110	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
311	16, 28	cmncom 19816	. . . . . . . . . 10 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
312	308, 309, 310, 311	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
313	57, 229, 279, 312	iscmnd 19812	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
314	313, 4, 287	isprimroot 42094	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
315	314	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
316	307, 315	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
317	316	ex 412	. . . 4 ⊢ (𝜑 → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
318	317	ssrdv 3989	. . 3 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
319	313	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ CMnd)
320	4	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
321	319, 320, 287	isprimroot 42094	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
322	321	biimpd 229	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
323	322	syldbl2 842	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
324	323	simp1d 1143	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
325	54	sselda 3983	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑈) → 𝑐 ∈ (Base‘𝑅))
326	325	ex 412	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)))
327	57	eleq2d 2827	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
328	327	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅))))
329	326, 328	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
330	329	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
331	330	imp 406	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))) → 𝑐 ∈ (Base‘𝑅))
332	324, 331	mpdan 687	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
333	284	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
334	327	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
335	324, 334	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
336	333, 320, 335, 288	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
337	323	simp2d 1144	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
338	238	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
339	336, 337, 338	3eqtrd 2781	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
340	323	simp3d 1145	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
341	333	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
342		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
343	335	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
344	341, 342, 343, 300	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
345	344	eqcomd 2743	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝑙(.g‘𝑅)𝑐))
346	338	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
347	345, 346	eqeq12d 2753	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑙(.g‘𝑅)𝑐) = (0g‘𝑅)))
348	347	imbi1d 341	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
349	348	ralbidva 3176	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
350	340, 349	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
351	332, 339, 350	3jca 1129	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
352	1	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
353	352, 320, 6	isprimroot 42094	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
354	351, 353	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (𝑅 PrimRoots 𝐾))
355	354	ex 412	. . . 4 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑐 ∈ (𝑅 PrimRoots 𝐾)))
356	355	ssrdv 3989	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ (𝑅 PrimRoots 𝐾))
357	318, 356	eqssd 4001	. 2 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
358	259, 313	jca 511	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
359		isabl 19802	. . 3 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel ↔ ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
360	358, 359	sylibr 234	. 2 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
361	357, 360	jca 511	1 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070  ∃!wreu 3378  ∃*wrmo 3379  {crab 3436  Vcvv 3480   ⊆ wss 3951   class class class wbr 5143  ‘cfv 6561  ℩crio 7387  (class class class)co 7431  1c1 11156   + caddc 11158   − cmin 11492  ℕcn 12266  ℕ₀cn0 12526   ∥ cdvds 16290  Basecbs 17247   ↾_s cress 17274  +_gcplusg 17297  0_gc0g 17484  Mndcmnd 18747  SubMndcsubmnd 18795  Grpcgrp 18951  inv_gcminusg 18952  ._gcmg 19085  CMndccmn 19798  Abelcabl 19799   PrimRoots cprimroots 42092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-seq 14043  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-grp 18954  df-minusg 18955  df-mulg 19086  df-cmn 19800  df-abl 19801  df-primroots 42093

This theorem is referenced by:  primrootsunit  42099