Theorem primrootsunit1 42589

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 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
3		primrootsunit1.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℕ)
4	3	nnnn0d 12496	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
5	4	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
6		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (.g‘𝑅) = (.g‘𝑅)
7	2, 5, 6	isprimroot 42585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
8	7	biimpd 230	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
9	8	syldbl2 847	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
10	9	simp1d 1148	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
11	1	cmnmndd 19777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Mnd)
12	11	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
13		nnm1nn0 12476	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
14	3, 13	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 − 1) ∈ ℕ0)
15	14	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾 − 1) ∈ ℕ0)
16		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑅) = (Base‘𝑅)
17	16, 6	mulgnn0cl 19064	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
18	12, 15, 10, 17	syl3anc 1379	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
19		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐))
20	19	oveq1d 7378	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → (𝑖(+g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
21	20	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → ((𝑖(+g‘𝑅)𝑐) = (0g‘𝑅) ↔ (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅)))
22	3	nncnd 12188	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℂ)
23		1cnd 11137	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℂ)
24	22, 23	npcand 11507	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
25	24	eqcomd 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 = ((𝐾 − 1) + 1))
26	25	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 = ((𝐾 − 1) + 1))
27	26	oveq1d 7378	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (((𝐾 − 1) + 1)(.g‘𝑅)𝑐))
28		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (+g‘𝑅) = (+g‘𝑅)
29	16, 6, 28	mulgnn0p1 19059	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
30	12, 15, 10, 29	syl3anc 1379	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
31	27, 30	eqtr2d 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (𝐾(.g‘𝑅)𝑐))
32	9	simp2d 1149	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
33	31, 32	eqtrd 2775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅))
34	18, 21, 33	rspcedvd 3569	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))
35	10, 34	jca 516	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
36		oveq2 7371	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑐))
37	36	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
38	37	rexbidv 3164	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
39	38	elrab 3636	. . . . . . . . . 10 ⊢ (𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
40	35, 39	sylibr 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
41		primrootsunit1.3	. . . . . . . . . 10 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}
42	41	eleq2i 2832	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
43	40, 42	sylibr 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
44		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝜑)
45	41	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
46	45	eleq2d 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
47	46	biimpd 230	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
48	47	imp 407	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
49	44, 48	jca 516	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
50		elrabi 3632	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑏 ∈ (Base‘𝑅))
51	50	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑏 ∈ (Base‘𝑅))
52	49, 51	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
53	52	ex 413	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ (Base‘𝑅)))
54	53	ssrdv 3928	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
55		eqid 2740	. . . . . . . . . . . 12 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
56	55, 16	ressbas2 17206	. . . . . . . . . . 11 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
57	54, 56	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
58	57	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
59	58	eleq2d 2826	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
60	43, 59	mpbid 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
61	11	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ Mnd)
62	52	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
63		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝜑)
64	45	eleq2d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
65	64	biimpd 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑑 ∈ 𝑈 → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
66	65	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
67	63, 66	jca 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → (𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
68		elrabi 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑑 ∈ (Base‘𝑅))
69	68	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑑 ∈ (Base‘𝑅))
70	67, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
71	44, 70	sylan 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
72	16, 28	mndcl 18708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
73	61, 62, 71, 72	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
74	41	eleq2i 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
75		oveq2 7371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑑 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑑))
76	75	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑑 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
77	76	rexbidv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑑 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
78	77	elrab 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
79	74, 78	bitri 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑑 ∈ 𝑈 ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
80	79	biimpi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑑 ∈ 𝑈 → (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
81	80	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑑 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
82	81	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
83	1	ad4antr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
84	71	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑑 ∈ (Base‘𝑅))
85		simplr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
86	16, 28	cmncom 19771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑑 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
87	83, 84, 85, 86	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
88		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
89	87, 88	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
90	89	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
91	90	reximdva 3153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
92	82, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
93	16, 61, 71, 92	mndmolinv 42587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
94	82, 93	jca 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
95		reu5 3347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
96	94, 95	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
97		riotacl 7337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
99		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (0g‘𝑅) = (0g‘𝑅)
100		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (invg‘𝑅) = (invg‘𝑅)
101	16, 28, 99, 100	grpinvval 18954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
102	71, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
103	102	eleq1d 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅)))
104	98, 103	mpbird 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅))
105	41	eleq2i 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
106		oveq2 7371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑏 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑏))
107	106	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑏 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
108	107	rexbidv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑏 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
109	108	elrab 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
110	105, 109	bitri 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑏 ∈ 𝑈 ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
111	110	biimpi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑏 ∈ 𝑈 → (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
112	111	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑏 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
113	112	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
114	1	ad4antr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
115	62	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑏 ∈ (Base‘𝑅))
116		simplr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
117	16, 28	cmncom 19771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
118	114, 115, 116, 117	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
119		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
120	118, 119	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
121	120	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
122	121	reximdva 3153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
123	113, 122	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
124	16, 61, 62, 123	mndmolinv 42587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
125	113, 124	jca 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
126		reu5 3347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
127	125, 126	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
128		riotacl 7337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
130	16, 28, 99, 100	grpinvval 18954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑏 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
131	62, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
132	131	eleq1d 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅)))
133	129, 132	mpbird 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅))
134	16, 28	mndcl 18708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 ∈ Mnd ∧ ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅)) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
135	61, 104, 133, 134	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
136		oveq1 7370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
137	136	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
138	137	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
139	104, 133, 73	3jca 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅)))
140	16, 28	mndass 18709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
141	61, 139, 140	syl2anc 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
142	133, 62, 71	3jca 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)))
143	16, 28	mndass 18709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
144	143	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
145	61, 142, 144	syl2anc 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
146	145	oveq2d 7379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)))
147	62, 127	linvh 42588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏) = (0g‘𝑅))
148	147	oveq1d 7378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = ((0g‘𝑅)(+g‘𝑅)𝑑))
149	148	oveq2d 7379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)))
150	16, 28, 99	mndlid 18720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑅 ∈ Mnd ∧ 𝑑 ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
151	61, 71, 150	syl2anc 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
152	151	oveq2d 7379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑))
153	71, 96	linvh 42588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑) = (0g‘𝑅))
154	152, 153	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (0g‘𝑅))
155	149, 154	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (0g‘𝑅))
156	146, 155	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (0g‘𝑅))
157	141, 156	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
158	135, 138, 157	rspcedvd 3569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
159	73, 158	jca 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
160		oveq2 7371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
161	160	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
162	161	rexbidv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
163	162	elrab 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
164	159, 163	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
165	41	eleq2i 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
166	165	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
167	164, 166	mpbird 258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
168	167	ralrimiva 3132	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
169	168	ralrimiva 3132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
170		oveq2 7371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
171	170	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
172	171	rexbidv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
173	16, 99	mndidcl 18715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
174	11, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
175	11, 174	jca 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)))
176	16, 28, 99	mndlid 18720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
178	174, 177	jca 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((0g‘𝑅) ∈ (Base‘𝑅) ∧ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
179		oveq1 7370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (0g‘𝑅) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
180	179	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = (0g‘𝑅) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
181	180	rspcev 3567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3638	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
184	45	eleq2d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((0g‘𝑅) ∈ 𝑈 ↔ (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
185	183, 184	mpbird 258	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑈)
186	16, 28, 99, 55	issubmnd 18727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Mnd ∧ 𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈) → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
187	11, 54, 185, 186	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
188	169, 187	mpbird 258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
189	45	eleq2d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
190	189	biimpd 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
191	190	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
192		oveq2 7371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑞 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑞))
193	192	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑞 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
194	193	rexbidv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑞 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
195	194	elrab 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
196	191, 195	sylib 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
197	196	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
198		simprl 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ (Base‘𝑅))
199	196	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ (Base‘𝑅))
200	199	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑞 ∈ (Base‘𝑅))
201		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → 𝑗 = 𝑞)
202	201	oveq1d 7378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → (𝑗(+g‘𝑅)𝑖) = (𝑞(+g‘𝑅)𝑖))
203	202	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → ((𝑗(+g‘𝑅)𝑖) = (0g‘𝑅) ↔ (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅)))
204	1	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑅 ∈ CMnd)
205	16, 28	cmncom 19771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ CMnd ∧ 𝑖 ∈ (Base‘𝑅) ∧ 𝑞 ∈ (Base‘𝑅)) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
206	204, 198, 200, 205	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
207		simprr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
208	206, 207	eqtr3d 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅))
209	200, 203, 208	rspcedvd 3569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅))
210	198, 209	jca 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
211		nfv 1921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑗(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)
212		nfv 1921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑖(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)
213		oveq1 7370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑖 = 𝑗 → (𝑖(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑎))
214	213	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑖 = 𝑗 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)))
215	211, 212, 214	cbvrexw 3283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅))
216	215	rabbii 3397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
217	41, 216	eqtri 2763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
218	217	eleq2i 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ 𝑈 ↔ 𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)})
219		oveq2 7371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑖 → (𝑗(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑖))
220	219	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑖 → ((𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
221	220	rexbidv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑖 → (∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
222	221	elrab 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
223	218, 222	bitri 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑈 ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
224	210, 223	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ 𝑈)
225	197, 224, 207	reximssdv 3158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
226		fvexd 6849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
227	41, 226	rabexd 5275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → 𝑈 ∈ V)
228	55, 28	ressplusg 17252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑈 ∈ V → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
229	227, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
230	229	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
231	230	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
232	231	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
233		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑤 = 𝑖)
234		eqidd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑞 = 𝑞)
235	232, 233, 234	oveq123d 7384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (𝑖(+g‘𝑅)𝑞))
236	55, 16, 99	ress0g 18728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝑅)) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
237	11, 185, 54, 236	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
238	237	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
239	238	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
240	239	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
241	235, 240	eqeq12d 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → ((𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
242		eqidd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑈 = 𝑈)
243	241, 242	cbvrexdva2 3317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
244	225, 243	mpbird 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
245	57	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
246	245	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
247	244, 246	rexeqtrrdv 3303	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
248	247	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
249	57	eleq2d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))))
250	249	imbi1d 342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))) ↔ (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))))
251	248, 250	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
252	251	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
253	252	ralrimiva 3132	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
254	188, 253	jca 516	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
255		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
256		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
257		eqid 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
258	255, 256, 257	isgrp 18913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp ↔ ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
259	254, 258	sylibr 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
260	259	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑅 ↾s 𝑈) ∈ Grp)
261		simplr 774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ 𝑈)
262	57	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
263	262	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
264	263	eleq2d 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈))))
265	261, 264	mpbid 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)))
266		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ 𝑈)
267	263	eleq2d 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))))
268	266, 267	mpbid 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈)))
269	255, 256	grpcl 18915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
270	260, 265, 268, 269	syl3anc 1379	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
271	263	eleq2d 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈))))
272	270, 271	mpbird 258	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈)
273	229	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
274	273	oveqdr 7391	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑))
275	274	eleq1d 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈))
276	272, 275	mpbird 258	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
277	276	ralrimiva 3132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
278	277	ralrimiva 3132	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
279	278, 187	mpbird 258	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
280	11, 279	jca 516	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd))
281	54, 185	jca 516	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈))
282	280, 281	jca 516	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
283	16, 99	issubmndb 18771	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubMnd‘𝑅) ↔ ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
284	282, 283	sylibr 235	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘𝑅))
285	284	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
286	285, 5, 43	3jca 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
287		eqid 2740	. . . . . . . . . . . 12 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
288	6, 55, 287	submmulg 19092	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
289	288	eqcomd 2746	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
290	286, 289	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
291	238	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
292	290, 291	eqeq12d 2756	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅)))
293	32, 292	mpbird 258	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
294	9	simp3d 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
295		eqidd 2741	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ℕ0 = ℕ0)
296	285	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
297		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
298	43	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
299	296, 297, 298	3jca 1134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
300	6, 55, 287	submmulg 19092	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
301	299, 300	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
302	237	ad2antrr 732	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
303	301, 302	eqeq12d 2756	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) ↔ (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈))))
304	303	imbi1d 342	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
305	295, 304	raleqbidva 3304	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
306	294, 305	mpbid 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
307	60, 293, 306	3jca 1134	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
308	1	3ad2ant1 1139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ CMnd)
309	62	3impa 1115	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
310	71	3impa 1115	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
311	16, 28	cmncom 19771	. . . . . . . . . 10 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
312	308, 309, 310, 311	syl3anc 1379	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
313	57, 229, 279, 312	iscmnd 19767	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
314	313, 4, 287	isprimroot 42585	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
315	314	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
316	307, 315	mpbird 258	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
317	316	ex 413	. . . 4 ⊢ (𝜑 → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
318	317	ssrdv 3928	. . 3 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
319	313	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ CMnd)
320	4	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
321	319, 320, 287	isprimroot 42585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
322	321	biimpd 230	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
323	322	syldbl2 847	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
324	323	simp1d 1148	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
325	54	sselda 3922	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑈) → 𝑐 ∈ (Base‘𝑅))
326	325	ex 413	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)))
327	57	eleq2d 2826	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
328	327	imbi1d 342	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅))))
329	326, 328	mpbid 233	. . . . . . . . . 10 ⊢ (𝜑 → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
330	329	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
331	330	imp 407	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))) → 𝑐 ∈ (Base‘𝑅))
332	324, 331	mpdan 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
333	284	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
334	327	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
335	324, 334	mpbird 258	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
336	333, 320, 335, 288	syl3anc 1379	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
337	323	simp2d 1149	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
338	238	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
339	336, 337, 338	3eqtrd 2779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
340	323	simp3d 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
341	333	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
342		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
343	335	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
344	341, 342, 343, 300	syl3anc 1379	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
345	344	eqcomd 2746	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝑙(.g‘𝑅)𝑐))
346	338	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
347	345, 346	eqeq12d 2756	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑙(.g‘𝑅)𝑐) = (0g‘𝑅)))
348	347	imbi1d 342	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
349	348	ralbidva 3161	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
350	340, 349	mpbid 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
351	332, 339, 350	3jca 1134	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
352	1	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
353	352, 320, 6	isprimroot 42585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
354	351, 353	mpbird 258	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (𝑅 PrimRoots 𝐾))
355	354	ex 413	. . . 4 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑐 ∈ (𝑅 PrimRoots 𝐾)))
356	355	ssrdv 3928	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ (𝑅 PrimRoots 𝐾))
357	318, 356	eqssd 3939	. 2 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
358	259, 313	jca 516	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
359		isabl 19757	. . 3 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel ↔ ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
360	358, 359	sylibr 235	. 2 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
361	357, 360	jca 516	1 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ∃wrex 3064  ∃!wreu 3343  ∃*wrmo 3344  {crab 3392  Vcvv 3432   ⊆ wss 3890   class class class wbr 5079  ‘cfv 6492  ℩crio 7319  (class class class)co 7363  1c1 11037   + caddc 11039   − cmin 11375  ℕcn 12172  ℕ₀cn0 12435   ∥ cdvds 16219  Basecbs 17177   ↾_s cress 17198  +_gcplusg 17218  0_gc0g 17400  Mndcmnd 18700  SubMndcsubmnd 18748  Grpcgrp 18907  inv_gcminusg 18908  ._gcmg 19041  CMndccmn 19753  Abelcabl 19754   PrimRoots cprimroots 42583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-1st 7938  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-nn 12173  df-2 12242  df-n0 12436  df-z 12523  df-uz 12787  df-fz 13460  df-seq 13962  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17178  df-ress 17199  df-plusg 17231  df-0g 17402  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-submnd 18750  df-grp 18910  df-minusg 18911  df-mulg 19042  df-cmn 19755  df-abl 19756  df-primroots 42584

This theorem is referenced by:  primrootsunit  42590