Theorem primrootsunit1 41599

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 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
3		primrootsunit1.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℕ)
4	3	nnnn0d 12570	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
5	4	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
6		eqid 2728	. . . . . . . . . . . . . . 15 ⊢ (.g‘𝑅) = (.g‘𝑅)
7	2, 5, 6	isprimroot 41596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
8	7	biimpd 228	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
9	8	syldbl2 839	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
10	9	simp1d 1139	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
11	1	cmnmndd 19766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Mnd)
12	11	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑅 ∈ Mnd)
13		nnm1nn0 12551	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
14	3, 13	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾 − 1) ∈ ℕ0)
15	14	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾 − 1) ∈ ℕ0)
16		eqid 2728	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑅) = (Base‘𝑅)
17	16, 6	mulgnn0cl 19052	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
18	12, 15, 10, 17	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾 − 1)(.g‘𝑅)𝑐) ∈ (Base‘𝑅))
19		simpr 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐))
20	19	oveq1d 7441	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → (𝑖(+g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
21	20	eqeq1d 2730	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑖 = ((𝐾 − 1)(.g‘𝑅)𝑐)) → ((𝑖(+g‘𝑅)𝑐) = (0g‘𝑅) ↔ (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅)))
22	3	nncnd 12266	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℂ)
23		1cnd 11247	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℂ)
24	22, 23	npcand 11613	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
25	24	eqcomd 2734	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 = ((𝐾 − 1) + 1))
26	25	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝐾 = ((𝐾 − 1) + 1))
27	26	oveq1d 7441	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (((𝐾 − 1) + 1)(.g‘𝑅)𝑐))
28		eqid 2728	. . . . . . . . . . . . . . . 16 ⊢ (+g‘𝑅) = (+g‘𝑅)
29	16, 6, 28	mulgnn0p1 19047	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Mnd ∧ (𝐾 − 1) ∈ ℕ0 ∧ 𝑐 ∈ (Base‘𝑅)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
30	12, 15, 10, 29	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1) + 1)(.g‘𝑅)𝑐) = (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐))
31	27, 30	eqtr2d 2769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (𝐾(.g‘𝑅)𝑐))
32	9	simp2d 1140	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
33	31, 32	eqtrd 2768	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (((𝐾 − 1)(.g‘𝑅)𝑐)(+g‘𝑅)𝑐) = (0g‘𝑅))
34	18, 21, 33	rspcedvd 3613	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))
35	10, 34	jca 510	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
36		oveq2 7434	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑐))
37	36	eqeq1d 2730	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
38	37	rexbidv 3176	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
39	38	elrab 3684	. . . . . . . . . 10 ⊢ (𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅)))
40	35, 39	sylibr 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
41		primrootsunit1.3	. . . . . . . . . 10 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}
42	41	eleq2i 2821	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
43	40, 42	sylibr 233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
44		simpl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝜑)
45	41	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
46	45	eleq2d 2815	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
47	46	biimpd 228	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
48	47	imp 405	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
49	44, 48	jca 510	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
50		elrabi 3678	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑏 ∈ (Base‘𝑅))
51	50	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑏 ∈ (Base‘𝑅))
52	49, 51	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
53	52	ex 411	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑏 ∈ 𝑈 → 𝑏 ∈ (Base‘𝑅)))
54	53	ssrdv 3988	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅))
55		eqid 2728	. . . . . . . . . . . 12 ⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈)
56	55, 16	ressbas2 17225	. . . . . . . . . . 11 ⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
57	54, 56	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
58	57	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
59	58	eleq2d 2815	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
60	43, 59	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
61	11	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ Mnd)
62	52	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
63		simpl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝜑)
64	45	eleq2d 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
65	64	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑑 ∈ 𝑈 → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
66	65	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
67	63, 66	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → (𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
68		elrabi 3678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} → 𝑑 ∈ (Base‘𝑅))
69	68	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) → 𝑑 ∈ (Base‘𝑅))
70	67, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
71	44, 70	sylan 578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
72	16, 28	mndcl 18709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
73	61, 62, 71, 72	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))
74	41	eleq2i 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
75		oveq2 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑑 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑑))
76	75	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑑 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
77	76	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑑 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
78	77	elrab 3684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑑 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
79	74, 78	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑑 ∈ 𝑈 ↔ (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
80	79	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑑 ∈ 𝑈 → (𝑑 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
81	80	simprd 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑑 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
82	81	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
83	1	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
84	71	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑑 ∈ (Base‘𝑅))
85		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
86	16, 28	cmncom 19760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑑 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
87	83, 84, 85, 86	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑑))
88		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
89	87, 88	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
90	89	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
91	90	reximdva 3165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅)))
92	82, 91	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑑(+g‘𝑅)𝑖) = (0g‘𝑅))
93	16, 61, 71, 92	mndmolinv 41597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
94	82, 93	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
95		reu5 3376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
96	94, 95	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅))
97		riotacl 7400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅))
99		eqid 2728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (0g‘𝑅) = (0g‘𝑅)
100		eqid 2728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (invg‘𝑅) = (invg‘𝑅)
101	16, 28, 99, 100	grpinvval 18944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑑 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
102	71, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)))
103	102	eleq1d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑑) = (0g‘𝑅)) ∈ (Base‘𝑅)))
104	98, 103	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅))
105	41	eleq2i 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
106		oveq2 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 = 𝑏 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑏))
107	106	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 = 𝑏 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
108	107	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 = 𝑏 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
109	108	elrab 3684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑏 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
110	105, 109	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑏 ∈ 𝑈 ↔ (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
111	110	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑏 ∈ 𝑈 → (𝑏 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
112	111	simprd 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑏 ∈ 𝑈 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
113	112	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
114	1	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑅 ∈ CMnd)
115	62	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑏 ∈ (Base‘𝑅))
116		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → 𝑖 ∈ (Base‘𝑅))
117	16, 28	cmncom 19760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑖 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
118	114, 115, 116, 117	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (𝑖(+g‘𝑅)𝑏))
119		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
120	118, 119	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) ∧ (𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
121	120	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 ∈ (Base‘𝑅)) → ((𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
122	121	reximdva 3165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅)))
123	113, 122	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑏(+g‘𝑅)𝑖) = (0g‘𝑅))
124	16, 61, 62, 123	mndmolinv 41597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
125	113, 124	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
126		reu5 3376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ↔ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) ∧ ∃*𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
127	125, 126	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅))
128		riotacl 7400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃!𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅))
130	16, 28, 99, 100	grpinvval 18944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑏 ∈ (Base‘𝑅) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
131	62, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) = (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)))
132	131	eleq1d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ↔ (℩𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑏) = (0g‘𝑅)) ∈ (Base‘𝑅)))
133	129, 132	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅))
134	16, 28	mndcl 18709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 ∈ Mnd ∧ ((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅)) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
135	61, 104, 133, 134	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) ∈ (Base‘𝑅))
136		oveq1 7433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
137	136	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏)) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
138	137	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) ∧ 𝑖 = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))) → ((𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅) ↔ ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
139	104, 133, 73	3jca 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅)))
140	16, 28	mndass 18710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑑) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ (𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
141	61, 139, 140	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))))
142	133, 62, 71	3jca 1125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)))
143	16, 28	mndass 18710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
144	143	eqcomd 2734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑅 ∈ Mnd ∧ (((invg‘𝑅)‘𝑏) ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅))) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
145	61, 142, 144	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑))
146	145	oveq2d 7442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)))
147	62, 127	linvh 41598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏) = (0g‘𝑅))
148	147	oveq1d 7441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑) = ((0g‘𝑅)(+g‘𝑅)𝑑))
149	148	oveq2d 7442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)))
150	16, 28, 99	mndlid 18721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑅 ∈ Mnd ∧ 𝑑 ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
151	61, 71, 150	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((0g‘𝑅)(+g‘𝑅)𝑑) = 𝑑)
152	151	oveq2d 7442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑))
153	71, 96	linvh 41598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)𝑑) = (0g‘𝑅))
154	152, 153	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((0g‘𝑅)(+g‘𝑅)𝑑)) = (0g‘𝑅))
155	149, 154	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)((((invg‘𝑅)‘𝑏)(+g‘𝑅)𝑏)(+g‘𝑅)𝑑)) = (0g‘𝑅))
156	146, 155	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (((invg‘𝑅)‘𝑑)(+g‘𝑅)(((invg‘𝑅)‘𝑏)(+g‘𝑅)(𝑏(+g‘𝑅)𝑑))) = (0g‘𝑅))
157	141, 156	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((((invg‘𝑅)‘𝑑)(+g‘𝑅)((invg‘𝑅)‘𝑏))(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
158	135, 138, 157	rspcedvd 3613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅))
159	73, 158	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
160		oveq2 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)))
161	160	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
162	161	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (𝑏(+g‘𝑅)𝑑) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
163	162	elrab 3684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ ((𝑏(+g‘𝑅)𝑑) ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(𝑏(+g‘𝑅)𝑑)) = (0g‘𝑅)))
164	159, 163	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
165	41	eleq2i 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
166	165	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘𝑅)𝑑) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
167	164, 166	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
168	167	ralrimiva 3143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
169	168	ralrimiva 3143	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
170		oveq2 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅)))
171	170	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
172	171	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
173	16, 99	mndidcl 18716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ Mnd → (0g‘𝑅) ∈ (Base‘𝑅))
174	11, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅))
175	11, 174	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)))
176	16, 28, 99	mndlid 18721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
178	174, 177	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((0g‘𝑅) ∈ (Base‘𝑅) ∧ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
179		oveq1 7433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 = (0g‘𝑅) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)))
180	179	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 = (0g‘𝑅) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)))
181	180	rspcev 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3686	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
184	45	eleq2d 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((0g‘𝑅) ∈ 𝑈 ↔ (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
185	183, 184	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑈)
186	16, 28, 99, 55	issubmnd 18728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Mnd ∧ 𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈) → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
187	11, 54, 185, 186	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ↔ ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈))
188	169, 187	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
189	45	eleq2d 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
190	189	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}))
191	190	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})
192		oveq2 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑞 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑞))
193	192	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑞 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
194	193	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑞 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
195	194	elrab 3684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑞 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
196	191, 195	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (𝑞 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
197	196	simprd 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
198		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ (Base‘𝑅))
199	196	simpld 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → 𝑞 ∈ (Base‘𝑅))
200	199	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑞 ∈ (Base‘𝑅))
201		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → 𝑗 = 𝑞)
202	201	oveq1d 7441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → (𝑗(+g‘𝑅)𝑖) = (𝑞(+g‘𝑅)𝑖))
203	202	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) ∧ 𝑗 = 𝑞) → ((𝑗(+g‘𝑅)𝑖) = (0g‘𝑅) ↔ (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅)))
204	1	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑅 ∈ CMnd)
205	16, 28	cmncom 19760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ CMnd ∧ 𝑖 ∈ (Base‘𝑅) ∧ 𝑞 ∈ (Base‘𝑅)) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
206	204, 198, 200, 205	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (𝑞(+g‘𝑅)𝑖))
207		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
208	206, 207	eqtr3d 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑞(+g‘𝑅)𝑖) = (0g‘𝑅))
209	200, 203, 208	rspcedvd 3613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅))
210	198, 209	jca 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
211		nfv 1909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑗(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)
212		nfv 1909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ Ⅎ𝑖(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)
213		oveq1 7433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑖 = 𝑗 → (𝑖(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑎))
214	213	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑖 = 𝑗 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)))
215	211, 212, 214	cbvrexw 3302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅))
216	215	rabbii 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
217	41, 216	eqtri 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)}
218	217	eleq2i 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ 𝑈 ↔ 𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)})
219		oveq2 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑎 = 𝑖 → (𝑗(+g‘𝑅)𝑎) = (𝑗(+g‘𝑅)𝑖))
220	219	eqeq1d 2730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑖 → ((𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
221	220	rexbidv 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑖 → (∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
222	221	elrab 3684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
223	218, 222	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑈 ↔ (𝑖 ∈ (Base‘𝑅) ∧ ∃𝑗 ∈ (Base‘𝑅)(𝑗(+g‘𝑅)𝑖) = (0g‘𝑅)))
224	210, 223	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ (𝑖 ∈ (Base‘𝑅) ∧ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))) → 𝑖 ∈ 𝑈)
225	197, 224, 207	reximssdv 3170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅))
226		fvexd 6917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
227	41, 226	rabexd 5339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → 𝑈 ∈ V)
228	55, 28	ressplusg 17278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑈 ∈ V → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
229	227, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
230	229	eqcomd 2734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
231	230	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
232	231	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (+g‘(𝑅 ↾s 𝑈)) = (+g‘𝑅))
233		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑤 = 𝑖)
234		eqidd 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑞 = 𝑞)
235	232, 233, 234	oveq123d 7447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (𝑖(+g‘𝑅)𝑞))
236	55, 16, 99	ress0g 18729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑅 ∈ Mnd ∧ (0g‘𝑅) ∈ 𝑈 ∧ 𝑈 ⊆ (Base‘𝑅)) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
237	11, 185, 54, 236	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
238	237	eqcomd 2734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
239	238	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
240	239	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
241	235, 240	eqeq12d 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → ((𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
242		eqidd 2729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑈) ∧ 𝑤 = 𝑖) → 𝑈 = 𝑈)
243	241, 242	cbvrexdva2 3343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ ∃𝑖 ∈ 𝑈 (𝑖(+g‘𝑅)𝑞) = (0g‘𝑅)))
244	225, 243	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
245	57	eqcomd 2734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
246	245	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (Base‘(𝑅 ↾s 𝑈)) = 𝑈)
247	246	rexeqdv 3324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → (∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)) ↔ ∃𝑤 ∈ 𝑈 (𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
248	244, 247	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑈) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
249	248	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
250	57	eleq2d 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑞 ∈ 𝑈 ↔ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))))
251	250	imbi1d 340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑞 ∈ 𝑈 → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))) ↔ (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))))
252	249, 251	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑅 ↾s 𝑈)) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
253	252	imp 405	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))) → ∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
254	253	ralrimiva 3143	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈)))
255	188, 254	jca 510	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
256		eqid 2728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Base‘(𝑅 ↾s 𝑈)) = (Base‘(𝑅 ↾s 𝑈))
257		eqid 2728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈))
258		eqid 2728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈))
259	256, 257, 258	isgrp 18903	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ↾s 𝑈) ∈ Grp ↔ ((𝑅 ↾s 𝑈) ∈ Mnd ∧ ∀𝑞 ∈ (Base‘(𝑅 ↾s 𝑈))∃𝑤 ∈ (Base‘(𝑅 ↾s 𝑈))(𝑤(+g‘(𝑅 ↾s 𝑈))𝑞) = (0g‘(𝑅 ↾s 𝑈))))
260	255, 259	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp)
261	260	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑅 ↾s 𝑈) ∈ Grp)
262		simplr 767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ 𝑈)
263	57	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
264	263	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑈 = (Base‘(𝑅 ↾s 𝑈)))
265	264	eleq2d 2815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈))))
266	262, 265	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)))
267		simpr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ 𝑈)
268	264	eleq2d 2815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑑 ∈ 𝑈 ↔ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))))
269	267, 268	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈)))
270	256, 257	grpcl 18905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝑏 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ 𝑑 ∈ (Base‘(𝑅 ↾s 𝑈))) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
271	261, 266, 269, 270	syl3anc 1368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈)))
272	264	eleq2d 2815	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ (Base‘(𝑅 ↾s 𝑈))))
273	271, 272	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈)
274	229	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (+g‘𝑅) = (+g‘(𝑅 ↾s 𝑈)))
275	274	oveqdr 7454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑))
276	275	eleq1d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → ((𝑏(+g‘𝑅)𝑑) ∈ 𝑈 ↔ (𝑏(+g‘(𝑅 ↾s 𝑈))𝑑) ∈ 𝑈))
277	273, 276	mpbird 256	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
278	277	ralrimiva 3143	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
279	278	ralrimiva 3143	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑏 ∈ 𝑈 ∀𝑑 ∈ 𝑈 (𝑏(+g‘𝑅)𝑑) ∈ 𝑈)
280	279, 187	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd)
281	11, 280	jca 510	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd))
282	54, 185	jca 510	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈))
283	281, 282	jca 510	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
284	16, 99	issubmndb 18764	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ (SubMnd‘𝑅) ↔ ((𝑅 ∈ Mnd ∧ (𝑅 ↾s 𝑈) ∈ Mnd) ∧ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈)))
285	283, 284	sylibr 233	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘𝑅))
286	285	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
287	286, 5, 43	3jca 1125	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
288		eqid 2728	. . . . . . . . . . . 12 ⊢ (.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈))
289	6, 55, 288	submmulg 19080	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
290	289	eqcomd 2734	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐾 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
291	287, 290	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝐾(.g‘𝑅)𝑐))
292	238	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
293	291, 292	eqeq12d 2744	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ((𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅)))
294	32, 293	mpbird 256	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
295	9	simp3d 1141	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
296		eqidd 2729	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ℕ0 = ℕ0)
297	286	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
298		simpr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
299	43	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
300	297, 298, 299	3jca 1125	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈))
301	6, 55, 288	submmulg 19080	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝑙 ∈ ℕ0 ∧ 𝑐 ∈ 𝑈) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
302	300, 301	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
303	237	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘𝑅) = (0g‘(𝑅 ↾s 𝑈)))
304	302, 303	eqeq12d 2744	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) ↔ (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈))))
305	304	imbi1d 340	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
306	296, 305	raleqbidva 3325	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
307	295, 306	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
308	60, 294, 307	3jca 1125	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
309	1	3ad2ant1 1130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑅 ∈ CMnd)
310	62	3impa 1107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑏 ∈ (Base‘𝑅))
311	71	3impa 1107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → 𝑑 ∈ (Base‘𝑅))
312	16, 28	cmncom 19760	. . . . . . . . . 10 ⊢ ((𝑅 ∈ CMnd ∧ 𝑏 ∈ (Base‘𝑅) ∧ 𝑑 ∈ (Base‘𝑅)) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
313	309, 310, 311, 312	syl3anc 1368	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈) → (𝑏(+g‘𝑅)𝑑) = (𝑑(+g‘𝑅)𝑏))
314	57, 229, 280, 313	iscmnd 19756	. . . . . . . 8 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd)
315	314, 4, 288	isprimroot 41596	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
316	315	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
317	308, 316	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑅 PrimRoots 𝐾)) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
318	317	ex 411	. . . 4 ⊢ (𝜑 → (𝑐 ∈ (𝑅 PrimRoots 𝐾) → 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)))
319	318	ssrdv 3988	. . 3 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) ⊆ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
320	314	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑅 ↾s 𝑈) ∈ CMnd)
321	4	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝐾 ∈ ℕ0)
322	320, 321, 288	isprimroot 41596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
323	322	biimpd 228	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))))
324	323	syldbl2 839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))
325	324	simp1d 1139	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)))
326	54	sselda 3982	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑈) → 𝑐 ∈ (Base‘𝑅))
327	326	ex 411	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)))
328	57	eleq2d 2815	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
329	328	imbi1d 340	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)) ↔ (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅))))
330	327, 329	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
331	330	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘(𝑅 ↾s 𝑈)) → 𝑐 ∈ (Base‘𝑅)))
332	331	imp 405	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))) → 𝑐 ∈ (Base‘𝑅))
333	325, 332	mpdan 685	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (Base‘𝑅))
334	285	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑈 ∈ (SubMnd‘𝑅))
335	328	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ (Base‘(𝑅 ↾s 𝑈))))
336	325, 335	mpbird 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ 𝑈)
337	334, 321, 336, 289	syl3anc 1368	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐))
338	324	simp2d 1140	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)))
339	238	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
340	337, 338, 339	3eqtrd 2772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅))
341	324	simp3d 1141	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))
342	334	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅))
343		simpr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑙 ∈ ℕ0)
344	336	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → 𝑐 ∈ 𝑈)
345	342, 343, 344, 301	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘𝑅)𝑐) = (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐))
346	345	eqcomd 2734	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (𝑙(.g‘𝑅)𝑐))
347	339	adantr 479	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (0g‘(𝑅 ↾s 𝑈)) = (0g‘𝑅))
348	346, 347	eqeq12d 2744	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) ↔ (𝑙(.g‘𝑅)𝑐) = (0g‘𝑅)))
349	348	imbi1d 340	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
350	349	ralbidva 3173	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑐) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
351	341, 350	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))
352	333, 340, 351	3jca 1125	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
353	1	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑅 ∈ CMnd)
354	353, 321, 6	isprimroot 41596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → (𝑐 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑐 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑐) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑐) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
355	352, 354	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) → 𝑐 ∈ (𝑅 PrimRoots 𝐾))
356	355	ex 411	. . . 4 ⊢ (𝜑 → (𝑐 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → 𝑐 ∈ (𝑅 PrimRoots 𝐾)))
357	356	ssrdv 3988	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ⊆ (𝑅 PrimRoots 𝐾))
358	319, 357	eqssd 3999	. 2 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾))
359	260, 314	jca 510	. . 3 ⊢ (𝜑 → ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
360		isabl 19746	. . 3 ⊢ ((𝑅 ↾s 𝑈) ∈ Abel ↔ ((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑅 ↾s 𝑈) ∈ CMnd))
361	359, 360	sylibr 233	. 2 ⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel)
362	358, 361	jca 510	1 ⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ∀wral 3058  ∃wrex 3067  ∃!wreu 3372  ∃*wrmo 3373  {crab 3430  Vcvv 3473   ⊆ wss 3949   class class class wbr 5152  ‘cfv 6553  ℩crio 7381  (class class class)co 7426  1c1 11147   + caddc 11149   − cmin 11482  ℕcn 12250  ℕ₀cn0 12510   ∥ cdvds 16238  Basecbs 17187   ↾_s cress 17216  +_gcplusg 17240  0_gc0g 17428  Mndcmnd 18701  SubMndcsubmnd 18746  Grpcgrp 18897  inv_gcminusg 18898  ._gcmg 19030  CMndccmn 19742  Abelcabl 19743   PrimRoots cprimroots 41594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12251  df-2 12313  df-n0 12511  df-z 12597  df-uz 12861  df-fz 13525  df-seq 14007  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17188  df-ress 17217  df-plusg 17253  df-0g 17430  df-mgm 18607  df-sgrp 18686  df-mnd 18702  df-submnd 18748  df-grp 18900  df-minusg 18901  df-mulg 19031  df-cmn 19744  df-abl 19745  df-primroots 41595

This theorem is referenced by:  primrootsunit  41600