Theorem elrgspnlem1 33342

Description: Lemma for elrgspn 33346. (Contributed by Thierry Arnoux, 5-Oct-2025.)

Hypotheses

Ref	Expression
elrgspn.b	⊢ 𝐵 = (Base‘𝑅)
elrgspn.m	⊢ 𝑀 = (mulGrp‘𝑅)
elrgspn.x	⊢ · = (.g‘𝑅)
elrgspn.n	⊢ 𝑁 = (RingSpan‘𝑅)
elrgspn.f	⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}
elrgspn.r	⊢ (𝜑 → 𝑅 ∈ Ring)
elrgspn.a	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
elrgspnlem1.1	⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))

Assertion

Ref	Expression
elrgspnlem1	⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))

Distinct variable groups:   · ,𝑓,𝑔,𝑤   𝐴,𝑓,𝑔,𝑤   𝐵,𝑓,𝑔,𝑤   𝑓,𝐹,𝑔,𝑤   𝑓,𝑀,𝑔,𝑤   𝑅,𝑓,𝑔,𝑤   𝑆,𝑔,𝑤   𝜑,𝑓,𝑔,𝑤

Allowed substitution hints:   𝑆(𝑓)   𝑁(𝑤,𝑓,𝑔)

Proof of Theorem elrgspnlem1

Dummy variables ℎ 𝑖 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elrgspn.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
2	1	ringgrpd 20194	. 2 ⊢ (𝜑 → 𝑅 ∈ Grp)
3		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
4		elrgspn.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑅)
5		eqid 2737	. . . . . . . . . 10 ⊢ (0g‘𝑅) = (0g‘𝑅)
6	1	ringcmnd 20236	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ CMnd)
7	6	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑅 ∈ CMnd)
8	4	fvexi 6858	. . . . . . . . . . . . . 14 ⊢ 𝐵 ∈ V
9	8	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ V)
10		elrgspn.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
11	9, 10	ssexd 5273	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ V)
12		wrdexg 14461	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ V → Word 𝐴 ∈ V)
13	11, 12	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → Word 𝐴 ∈ V)
14	13	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ∈ V)
15		elrgspn.x	. . . . . . . . . . . 12 ⊢ · = (.g‘𝑅)
16	2	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
17		elrgspn.f	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}
18	17	ssrab3 4036	. . . . . . . . . . . . . . . 16 ⊢ 𝐹 ⊆ (ℤ ↑m Word 𝐴)
19	18	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word 𝐴))
20	19	sselda 3935	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word 𝐴))
21		zex 12511	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ∈ V
22	21	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℤ ∈ V)
23	22, 13	elmapd 8791	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
24	23	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
25	20, 24	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
26	25	ffvelcdmda 7040	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
27		elrgspn.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (mulGrp‘𝑅)
28	27	ringmgp 20191	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
29	1, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ Mnd)
30		sswrd 14459	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
31	10, 30	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
32	31	sselda 3935	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
33	27, 4	mgpbas 20097	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝑀)
34	33	gsumwcl 18778	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
35	29, 32, 34	syl2an2r 686	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
36	35	adantlr 716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
37	4, 15, 16, 26, 36	mulgcld 19043	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
38	37	fmpttd 7071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵)
39		fvexd 6859	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V)
40		0zd 12514	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ)
41		ssidd 3959	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴)
42		breq1 5103	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
43	42, 17	elrab2 3651	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
44	43	simprbi 497	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
45	44	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
46	4, 5, 15	mulg0 19021	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅))
47	46	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅))
48	39, 40, 14, 41, 36, 25, 45, 47	fisuppov1 32779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
49	4, 5, 7, 14, 38, 48	gsumcl 19861	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
50	49	ad4ant13 752	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
51	3, 50	eqeltrd 2837	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 ∈ 𝐵)
52		elrgspnlem1.1	. . . . . . . . . 10 ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
53	52	eleq2i 2829	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
54		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
55	54	elrnmpt 5917	. . . . . . . . . 10 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
56	55	elv 3447	. . . . . . . . 9 ⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
57	53, 56	sylbb 219	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑆 → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
58	57	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
59	51, 58	r19.29a 3146	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵)
60	59, 4	eleqtrdi 2847	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑅))
61	60	ex 412	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ (Base‘𝑅)))
62	61	ssrdv 3941	. . 3 ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑅))
63	62, 4	sseqtrrdi 3977	. 2 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
64		breq1 5103	. . . . . . . 8 ⊢ (𝑓 = (Word 𝐴 × {0}) → (𝑓 finSupp 0 ↔ (Word 𝐴 × {0}) finSupp 0))
65		0z 12513	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
66	65	fconst6 6734	. . . . . . . . . 10 ⊢ (Word 𝐴 × {0}):Word 𝐴⟶ℤ
67	66	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (Word 𝐴 × {0}):Word 𝐴⟶ℤ)
68	22, 13, 67	elmapdd 8792	. . . . . . . 8 ⊢ (𝜑 → (Word 𝐴 × {0}) ∈ (ℤ ↑m Word 𝐴))
69		c0ex 11140	. . . . . . . . . 10 ⊢ 0 ∈ V
70	69	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ V)
71	13, 70	fczfsuppd 9303	. . . . . . . 8 ⊢ (𝜑 → (Word 𝐴 × {0}) finSupp 0)
72	64, 68, 71	elrabd 3650	. . . . . . 7 ⊢ (𝜑 → (Word 𝐴 × {0}) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
73	72, 17	eleqtrrdi 2848	. . . . . 6 ⊢ (𝜑 → (Word 𝐴 × {0}) ∈ 𝐹)
74		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → 𝑔 = (Word 𝐴 × {0}))
75	74	fveq1d 6846	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = ((Word 𝐴 × {0})‘𝑤))
76	69	fconst 6730	. . . . . . . . . . . . . . 15 ⊢ (Word 𝐴 × {0}):Word 𝐴⟶{0}
77	76	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (Word 𝐴 × {0}):Word 𝐴⟶{0})
78		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
79		fvconst 7120	. . . . . . . . . . . . . 14 ⊢ (((Word 𝐴 × {0}):Word 𝐴⟶{0} ∧ 𝑤 ∈ Word 𝐴) → ((Word 𝐴 × {0})‘𝑤) = 0)
80	77, 78, 79	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((Word 𝐴 × {0})‘𝑤) = 0)
81	75, 80	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = 0)
82	81	oveq1d 7385	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
83	35	adantlr 716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
84	4, 5, 15	mulg0 19021	. . . . . . . . . . . 12 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
85	83, 84	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
86	82, 85	eqtrd 2772	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
87	86	mpteq2dva 5193	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))
88	87	oveq2d 7386	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))))
89	6	cmnmndd 19750	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Mnd)
90	5	gsumz 18775	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Mnd ∧ Word 𝐴 ∈ V) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅))
91	89, 13, 90	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅))
92	91	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅))
93	88, 92	eqtrd 2772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (0g‘𝑅))
94	93	eqeq2d 2748	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → ((0g‘𝑅) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (0g‘𝑅) = (0g‘𝑅)))
95		eqidd 2738	. . . . . 6 ⊢ (𝜑 → (0g‘𝑅) = (0g‘𝑅))
96	73, 94, 95	rspcedvd 3580	. . . . 5 ⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (0g‘𝑅) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
97		fvexd 6859	. . . . 5 ⊢ (𝜑 → (0g‘𝑅) ∈ V)
98	54, 96, 97	elrnmptd 5922	. . . 4 ⊢ (𝜑 → (0g‘𝑅) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
99	98, 52	eleqtrrdi 2848	. . 3 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑆)
100	99	ne0d 4296	. 2 ⊢ (𝜑 → 𝑆 ≠ ∅)
101		simpllr 776	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
102		simpr 484	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
103	101, 102	oveq12d 7388	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
104		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (+g‘𝑅) = (+g‘𝑅)
105	7	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ CMnd)
106	14	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ∈ V)
107	37	adantlr 716	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
108	2	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
109		breq1 5103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0))
110	109, 17	elrab2 3651	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑖 finSupp 0))
111	110	simplbi 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word 𝐴))
112	111	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word 𝐴))
113	22, 13	elmapd 8791	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
114	113	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
115	112, 114	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
116	115	ffvelcdmda 7040	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ)
117	35	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
118	4, 15, 108, 116, 117	mulgcld 19043	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
119	118	adantllr 720	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
120		eqidd 2738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
121		eqidd 2738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
122	48	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
123	48	ralrimiva 3130	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
124		fveq1 6843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤))
125	124	oveq1d 7385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
126	125	mpteq2dv 5194	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
127	126	breq1d 5110	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅)))
128	127	cbvralvw 3216	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
129	123, 128	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
130	129	r19.21bi 3230	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
131	130	adantlr 716	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
132	4, 5, 104, 105, 106, 107, 119, 120, 121, 122, 131	gsummptfsadd 19870	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
133	25	ffnd 6673	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
134	133	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
135	115	ffnd 6673	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
136	135	adantlr 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
137		inidm 4181	. . . . . . . . . . . . . . . . . 18 ⊢ (Word 𝐴 ∩ Word 𝐴) = Word 𝐴
138		eqidd 2738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = (𝑔‘𝑤))
139		eqidd 2738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) = (𝑖‘𝑤))
140	134, 136, 106, 106, 137, 138, 139	ofval 7645	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔 ∘f + 𝑖)‘𝑤) = ((𝑔‘𝑤) + (𝑖‘𝑤)))
141	140	oveq1d 7385	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)))
142	16	adantlr 716	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
143	26	adantlr 716	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
144	116	adantllr 720	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ)
145	36	adantlr 716	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
146	4, 15, 104	mulgdir 19053	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
147	142, 143, 144, 145, 146	syl13anc 1375	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
148	141, 147	eqtr2d 2773	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))
149	148	mpteq2dva 5193	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))
150	149	oveq2d 7386	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
151	132, 150	eqtr3d 2774	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
152		fveq1 6843	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤))
153	152	oveq1d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))
154	153	mpteq2dv 5194	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))
155	154	oveq2d 7386	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
156	155	cbvmptv 5204	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
157		fveq1 6843	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → (ℎ‘𝑤) = ((𝑔 ∘f + 𝑖)‘𝑤))
158	157	oveq1d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))
159	158	mpteq2dv 5194	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))
160	159	oveq2d 7386	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
161	160	eqeq2d 2748	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))))
162		breq1 5103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑔 ∘f + 𝑖) → (𝑓 finSupp 0 ↔ (𝑔 ∘f + 𝑖) finSupp 0))
163	21	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V)
164		zaddcl 12545	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 + 𝑦) ∈ ℤ)
165	164	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 + 𝑦) ∈ ℤ)
166	25	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
167	115	adantlr 716	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
168	165, 166, 167, 106, 106, 137	off 7652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖):Word 𝐴⟶ℤ)
169	163, 106, 168	elmapdd 8792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ (ℤ ↑m Word 𝐴))
170		zringring 21421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℤring ∈ Ring
171		ringmnd 20195	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℤring ∈ Ring → ℤring ∈ Mnd)
172	170, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℤring ∈ Mnd
173	172	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤring ∈ Mnd)
174	20	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word 𝐴))
175	111	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word 𝐴))
176	45	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 finSupp 0)
177		zring0 21430	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 = (0g‘ℤring)
178	176, 177	breqtrdi 5141	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 finSupp (0g‘ℤring))
179	110	simprbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0)
180	179	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0)
181	180, 177	breqtrdi 5141	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp (0g‘ℤring))
182		zringbas 21425	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℤ = (Base‘ℤring)
183	182	mndpfsupp 18706	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ℤring ∈ Mnd ∧ Word 𝐴 ∈ V) ∧ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑖 ∈ (ℤ ↑m Word 𝐴)) ∧ (𝑔 finSupp (0g‘ℤring) ∧ 𝑖 finSupp (0g‘ℤring))) → (𝑔 ∘f (+g‘ℤring)𝑖) finSupp (0g‘ℤring))
184	173, 106, 174, 175, 178, 181, 183	syl222anc 1389	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f (+g‘ℤring)𝑖) finSupp (0g‘ℤring))
185		zringplusg 21426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ + = (+g‘ℤring)
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → + = (+g‘ℤring))
187	186	ofeqd 7636	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∘f + = ∘f (+g‘ℤring))
188	187	oveqd 7387	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) = (𝑔 ∘f (+g‘ℤring)𝑖))
189	177	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 = (0g‘ℤring))
190	184, 188, 189	3brtr4d 5132	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) finSupp 0)
191	162, 169, 190	elrabd 3650	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
192	191, 17	eleqtrrdi 2848	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ 𝐹)
193		eqidd 2738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
194	161, 192, 193	rspcedvdw 3581	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
195		ovexd 7405	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V)
196	156, 194, 195	elrnmptd 5922	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
197	196, 52	eleqtrrdi 2848	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
198	151, 197	eqeltrd 2837	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
199	198	adantllr 720	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
200	199	adantllr 720	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
201	200	ad4ant13 752	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
202	103, 201	eqeltrd 2837	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆)
203	52	eleq2i 2829	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
204	126	oveq2d 7386	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
205	204	cbvmptv 5204	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
206	205	elrnmpt 5917	. . . . . . . . . . 11 ⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
207	206	elv 3447	. . . . . . . . . 10 ⊢ (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
208	203, 207	sylbb 219	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑆 → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
209	208	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
210	209	ad2antrr 727	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
211	202, 210	r19.29a 3146	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆)
212	58	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
213	211, 212	r19.29a 3146	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆)
214	213	ralrimiva 3130	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆)
215	2	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑅 ∈ Grp)
216	26	znegcld 12612	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) ∈ ℤ)
217	4, 15, 16, 216, 36	mulgcld 19043	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
218	217	fmpttd 7071	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵)
219	25	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑔:Word 𝐴⟶ℤ)
220		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
221	219, 220	fvco3d 6944	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤)))
222		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℤ ↦ -𝑧) = (𝑧 ∈ ℤ ↦ -𝑧)
223		negeq 11386	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑔‘𝑤) → -𝑧 = -(𝑔‘𝑤))
224	222, 223, 26, 216	fvmptd3 6975	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤)) = -(𝑔‘𝑤))
225	221, 224	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = -(𝑔‘𝑤))
226	225	oveq1d 7385	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤)) = (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))
227	226	mpteq2dva 5193	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
228		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
229	228	znegcld 12612	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → -𝑧 ∈ ℤ)
230	229	fmpttd 7071	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ)
231	230	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ)
232	231, 25	fcod 6697	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔):Word 𝐴⟶ℤ)
233	21	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ℤ ∈ V)
234		negeq 11386	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 0 → -𝑧 = -0)
235		neg0 11441	. . . . . . . . . . . . . . 15 ⊢ -0 = 0
236	234, 235	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → -𝑧 = 0)
237		0zd 12514	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ ℤ)
238	222, 236, 237, 237	fvmptd3 6975	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0)
239	238	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0)
240	40, 25, 231, 14, 233, 45, 239	fsuppco2 9320	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔) finSupp 0)
241	39, 40, 14, 41, 36, 232, 240, 47	fisuppov1 32779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
242	227, 241	eqbrtrrd 5124	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
243	4, 5, 7, 14, 218, 242	gsumcl 19861	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
244	243	ad4ant13 752	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
245	3	oveq1d 7385	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
246		eqidd 2738	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
247		eqidd 2738	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
248	4, 5, 104, 7, 14, 37, 217, 246, 247, 48, 242	gsummptfsadd 19870	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
249	248	ad4ant13 752	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
250	26	zcnd 12611	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℂ)
251	250	negidd 11496	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) + -(𝑔‘𝑤)) = 0)
252	251	oveq1d 7385	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
253	4, 15, 104	mulgdir 19053	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ -(𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
254	16, 26, 216, 36, 253	syl13anc 1375	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
255	36, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
256	252, 254, 255	3eqtr3d 2780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (0g‘𝑅))
257	256	mpteq2dva 5193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))
258	257	oveq2d 7386	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))))
259	91	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅))
260	258, 259	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (0g‘𝑅))
261	260	ad4ant13 752	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (0g‘𝑅))
262	245, 249, 261	3eqtr2d 2778	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (0g‘𝑅))
263		eqid 2737	. . . . . . . . 9 ⊢ (invg‘𝑅) = (invg‘𝑅)
264	4, 104, 5, 263	grpinvid1 18938	. . . . . . . 8 ⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) → (((invg‘𝑅)‘𝑥) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (0g‘𝑅)))
265	264	biimpar 477	. . . . . . 7 ⊢ (((𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) ∧ (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (0g‘𝑅)) → ((invg‘𝑅)‘𝑥) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
266	215, 51, 244, 262, 265	syl31anc 1376	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ((invg‘𝑅)‘𝑥) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
267		fveq1 6843	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (ℎ‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤))
268	267	oveq1d 7385	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))
269	268	mpteq2dv 5194	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))
270	269	oveq2d 7386	. . . . . . . . . . 11 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))))
271	270	eqeq2d 2748	. . . . . . . . . 10 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))))
272		breq1 5103	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0))
273	25	ffvelcdmda 7040	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑔‘𝑣) ∈ ℤ)
274	273	znegcld 12612	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → -(𝑔‘𝑣) ∈ ℤ)
275	274	fmpttd 7071	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)):Word 𝐴⟶ℤ)
276	233, 14, 275	elmapdd 8792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ (ℤ ↑m Word 𝐴))
277	275	ffund 6676	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Fun (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)))
278	133	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 𝑔 Fn Word 𝐴)
279	14	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → Word 𝐴 ∈ V)
280		0zd 12514	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 0 ∈ ℤ)
281		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
282	278, 279, 280, 281	fvdifsupp 8125	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → (𝑔‘𝑣) = 0)
283	282	negeqd 11388	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = -0)
284	283, 235	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = 0)
285	284, 14	suppss2 8154	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) supp 0) ⊆ (𝑔 supp 0))
286	276, 40, 277, 45, 285	fsuppsssuppgd 9299	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0)
287	272, 276, 286	elrabd 3650	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
288	287, 17	eleqtrrdi 2848	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ 𝐹)
289		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))
290		fveq2 6844	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑤 → (𝑔‘𝑣) = (𝑔‘𝑤))
291	290	negeqd 11388	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑤 → -(𝑔‘𝑣) = -(𝑔‘𝑤))
292	289, 291, 220, 216	fvmptd3 6975	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) = -(𝑔‘𝑤))
293	292	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤))
294	293	oveq1d 7385	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))
295	294	mpteq2dva 5193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))
296	295	oveq2d 7386	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))))
297	271, 288, 296	rspcedvdw 3581	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
298	156, 297, 243	elrnmptd 5922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
299	298, 52	eleqtrrdi 2848	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
300	299	ad4ant13 752	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
301	266, 300	eqeltrd 2837	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ((invg‘𝑅)‘𝑥) ∈ 𝑆)
302	301, 58	r19.29a 3146	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((invg‘𝑅)‘𝑥) ∈ 𝑆)
303	214, 302	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))
304	303	ralrimiva 3130	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))
305	4, 104, 263	issubg2 19088	. . 3 ⊢ (𝑅 ∈ Grp → (𝑆 ∈ (SubGrp‘𝑅) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))))
306	305	biimpar 477	. 2 ⊢ ((𝑅 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))) → 𝑆 ∈ (SubGrp‘𝑅))
307	2, 63, 100, 304, 306	syl13anc 1375	1 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ∖ cdif 3900   ⊆ wss 3903  ∅c0 4287  {csn 4582   class class class wbr 5100   ↦ cmpt 5181   × cxp 5632  ran crn 5635   ∘ ccom 5638   Fn wfn 6497  ⟶wf 6498  ‘cfv 6502  (class class class)co 7370   ∘_f cof 7632   supp csupp 8114   ↑_m cmap 8777   finSupp cfsupp 9278  0cc0 11040   + caddc 11043  -cneg 11379  ℤcz 12502  Word cword 14450  Basecbs 17150  +_gcplusg 17191  0_gc0g 17373   Σ_g cgsu 17374  Mndcmnd 18673  Grpcgrp 18880  inv_gcminusg 18881  ._gcmg 19014  SubGrpcsubg 19067  CMndccmn 19726  mulGrpcmgp 20092  Ringcrg 20185  RingSpancrgspn 20560  ℤ_ringczring 21418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117  ax-addf 11119

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-se 5588  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-isom 6511  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-of 7634  df-om 7821  df-1st 7945  df-2nd 7946  df-supp 8115  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-1o 8409  df-er 8647  df-map 8779  df-en 8898  df-dom 8899  df-sdom 8900  df-fin 8901  df-fsupp 9279  df-oi 9429  df-card 9865  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-nn 12160  df-2 12222  df-3 12223  df-4 12224  df-5 12225  df-6 12226  df-7 12227  df-8 12228  df-9 12229  df-n0 12416  df-z 12503  df-dec 12622  df-uz 12766  df-fz 13438  df-fzo 13585  df-seq 13939  df-hash 14268  df-word 14451  df-struct 17088  df-sets 17105  df-slot 17123  df-ndx 17135  df-base 17151  df-ress 17172  df-plusg 17204  df-mulr 17205  df-starv 17206  df-tset 17210  df-ple 17211  df-ds 17213  df-unif 17214  df-0g 17375  df-gsum 17376  df-mgm 18579  df-sgrp 18658  df-mnd 18674  df-submnd 18723  df-grp 18883  df-minusg 18884  df-mulg 19015  df-subg 19070  df-cntz 19263  df-cmn 19728  df-abl 19729  df-mgp 20093  df-rng 20105  df-ur 20134  df-ring 20187  df-cring 20188  df-subrng 20496  df-subrg 20520  df-cnfld 21327  df-zring 21419

This theorem is referenced by:  elrgspnlem2  33343