Theorem elrgspnlem1 33209

Description: Lemma for elrgspn 33213. (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 20162	. 2 ⊢ (𝜑 → 𝑅 ∈ Grp)
3		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
4		elrgspn.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑅)
5		eqid 2729	. . . . . . . . . 10 ⊢ (0g‘𝑅) = (0g‘𝑅)
6	1	ringcmnd 20204	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ CMnd)
7	6	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑅 ∈ CMnd)
8	4	fvexi 6854	. . . . . . . . . . . . . 14 ⊢ 𝐵 ∈ V
9	8	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ V)
10		elrgspn.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
11	9, 10	ssexd 5274	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ V)
12		wrdexg 14465	. . . . . . . . . . . 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 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
17		elrgspn.f	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}
18	17	ssrab3 4041	. . . . . . . . . . . . . . . 16 ⊢ 𝐹 ⊆ (ℤ ↑m Word 𝐴)
19	18	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word 𝐴))
20	19	sselda 3943	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word 𝐴))
21		zex 12514	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ∈ V
22	21	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℤ ∈ V)
23	22, 13	elmapd 8790	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
24	23	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
25	20, 24	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
26	25	ffvelcdmda 7038	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
27		elrgspn.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (mulGrp‘𝑅)
28	27	ringmgp 20159	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
29	1, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ Mnd)
30		sswrd 14463	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
31	10, 30	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
32	31	sselda 3943	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
33	27, 4	mgpbas 20065	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝑀)
34	33	gsumwcl 18748	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
35	29, 32, 34	syl2an2r 685	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
36	35	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
37	4, 15, 16, 26, 36	mulgcld 19010	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
38	37	fmpttd 7069	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵)
39		fvexd 6855	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V)
40		0zd 12517	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ)
41		ssidd 3967	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴)
42		breq1 5105	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
43	42, 17	elrab2 3659	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
44	43	simprbi 496	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
45	44	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
46	4, 5, 15	mulg0 18988	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅))
47	46	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅))
48	39, 40, 14, 41, 36, 25, 45, 47	fisuppov1 32656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
49	4, 5, 7, 14, 38, 48	gsumcl 19829	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
50	49	ad4ant13 751	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
51	3, 50	eqeltrd 2828	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 ∈ 𝐵)
52		elrgspnlem1.1	. . . . . . . . . 10 ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
53	52	eleq2i 2820	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
54		eqid 2729	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
55	54	elrnmpt 5911	. . . . . . . . . 10 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
56	55	elv 3449	. . . . . . . . 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 3141	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵)
60	59, 4	eleqtrdi 2838	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑅))
61	60	ex 412	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ (Base‘𝑅)))
62	61	ssrdv 3949	. . 3 ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑅))
63	62, 4	sseqtrrdi 3985	. 2 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
64		breq1 5105	. . . . . . . 8 ⊢ (𝑓 = (Word 𝐴 × {0}) → (𝑓 finSupp 0 ↔ (Word 𝐴 × {0}) finSupp 0))
65		0z 12516	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
66	65	fconst6 6732	. . . . . . . . . 10 ⊢ (Word 𝐴 × {0}):Word 𝐴⟶ℤ
67	66	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (Word 𝐴 × {0}):Word 𝐴⟶ℤ)
68	22, 13, 67	elmapdd 8791	. . . . . . . 8 ⊢ (𝜑 → (Word 𝐴 × {0}) ∈ (ℤ ↑m Word 𝐴))
69		c0ex 11144	. . . . . . . . . 10 ⊢ 0 ∈ V
70	69	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ V)
71	13, 70	fczfsuppd 9313	. . . . . . . 8 ⊢ (𝜑 → (Word 𝐴 × {0}) finSupp 0)
72	64, 68, 71	elrabd 3658	. . . . . . 7 ⊢ (𝜑 → (Word 𝐴 × {0}) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
73	72, 17	eleqtrrdi 2839	. . . . . 6 ⊢ (𝜑 → (Word 𝐴 × {0}) ∈ 𝐹)
74		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → 𝑔 = (Word 𝐴 × {0}))
75	74	fveq1d 6842	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = ((Word 𝐴 × {0})‘𝑤))
76	69	fconst 6728	. . . . . . . . . . . . . . 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 7118	. . . . . . . . . . . . . 14 ⊢ (((Word 𝐴 × {0}):Word 𝐴⟶{0} ∧ 𝑤 ∈ Word 𝐴) → ((Word 𝐴 × {0})‘𝑤) = 0)
80	77, 78, 79	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((Word 𝐴 × {0})‘𝑤) = 0)
81	75, 80	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = 0)
82	81	oveq1d 7384	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
83	35	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
84	4, 5, 15	mulg0 18988	. . . . . . . . . . . 12 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
85	83, 84	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
86	82, 85	eqtrd 2764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
87	86	mpteq2dva 5195	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))
88	87	oveq2d 7385	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))))
89	6	cmnmndd 19718	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Mnd)
90	5	gsumz 18745	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Mnd ∧ Word 𝐴 ∈ V) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅))
91	89, 13, 90	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅))
92	91	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅))
93	88, 92	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (0g‘𝑅))
94	93	eqeq2d 2740	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → ((0g‘𝑅) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (0g‘𝑅) = (0g‘𝑅)))
95		eqidd 2730	. . . . . 6 ⊢ (𝜑 → (0g‘𝑅) = (0g‘𝑅))
96	73, 94, 95	rspcedvd 3587	. . . . 5 ⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (0g‘𝑅) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
97		fvexd 6855	. . . . 5 ⊢ (𝜑 → (0g‘𝑅) ∈ V)
98	54, 96, 97	elrnmptd 5916	. . . 4 ⊢ (𝜑 → (0g‘𝑅) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
99	98, 52	eleqtrrdi 2839	. . 3 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑆)
100	99	ne0d 4301	. 2 ⊢ (𝜑 → 𝑆 ≠ ∅)
101		simpllr 775	. . . . . . . . 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 7387	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
104		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (+g‘𝑅) = (+g‘𝑅)
105	7	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ CMnd)
106	14	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ∈ V)
107	37	adantlr 715	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
108	2	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
109		breq1 5105	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0))
110	109, 17	elrab2 3659	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑖 finSupp 0))
111	110	simplbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word 𝐴))
112	111	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word 𝐴))
113	22, 13	elmapd 8790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
114	113	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
115	112, 114	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
116	115	ffvelcdmda 7038	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ)
117	35	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
118	4, 15, 108, 116, 117	mulgcld 19010	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
119	118	adantllr 719	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
120		eqidd 2730	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
121		eqidd 2730	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
122	48	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
123	48	ralrimiva 3125	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
124		fveq1 6839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤))
125	124	oveq1d 7384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
126	125	mpteq2dv 5196	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
127	126	breq1d 5112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅)))
128	127	cbvralvw 3213	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
129	123, 128	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
130	129	r19.21bi 3227	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
131	130	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
132	4, 5, 104, 105, 106, 107, 119, 120, 121, 122, 131	gsummptfsadd 19838	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
133	25	ffnd 6671	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
134	133	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
135	115	ffnd 6671	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
136	135	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
137		inidm 4186	. . . . . . . . . . . . . . . . . 18 ⊢ (Word 𝐴 ∩ Word 𝐴) = Word 𝐴
138		eqidd 2730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = (𝑔‘𝑤))
139		eqidd 2730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) = (𝑖‘𝑤))
140	134, 136, 106, 106, 137, 138, 139	ofval 7644	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔 ∘f + 𝑖)‘𝑤) = ((𝑔‘𝑤) + (𝑖‘𝑤)))
141	140	oveq1d 7384	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)))
142	16	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
143	26	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
144	116	adantllr 719	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ)
145	36	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
146	4, 15, 104	mulgdir 19020	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
147	142, 143, 144, 145, 146	syl13anc 1374	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
148	141, 147	eqtr2d 2765	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))
149	148	mpteq2dva 5195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))
150	149	oveq2d 7385	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
151	132, 150	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
152		fveq1 6839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤))
153	152	oveq1d 7384	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))
154	153	mpteq2dv 5196	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))
155	154	oveq2d 7385	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
156	155	cbvmptv 5206	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
157		fveq1 6839	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → (ℎ‘𝑤) = ((𝑔 ∘f + 𝑖)‘𝑤))
158	157	oveq1d 7384	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))
159	158	mpteq2dv 5196	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))
160	159	oveq2d 7385	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
161	160	eqeq2d 2740	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))))
162		breq1 5105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑔 ∘f + 𝑖) → (𝑓 finSupp 0 ↔ (𝑔 ∘f + 𝑖) finSupp 0))
163	21	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V)
164		zaddcl 12549	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 + 𝑦) ∈ ℤ)
165	164	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 + 𝑦) ∈ ℤ)
166	25	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
167	115	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
168	165, 166, 167, 106, 106, 137	off 7651	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖):Word 𝐴⟶ℤ)
169	163, 106, 168	elmapdd 8791	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ (ℤ ↑m Word 𝐴))
170		zringring 21391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℤring ∈ Ring
171		ringmnd 20163	. . . . . . . . . . . . . . . . . . . . 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 21400	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 = (0g‘ℤring)
178	176, 177	breqtrdi 5143	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 finSupp (0g‘ℤring))
179	110	simprbi 496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0)
180	179	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0)
181	180, 177	breqtrdi 5143	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp (0g‘ℤring))
182		zringbas 21395	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℤ = (Base‘ℤring)
183	182	mndpfsupp 18676	. . . . . . . . . . . . . . . . . . 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 1388	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f (+g‘ℤring)𝑖) finSupp (0g‘ℤring))
185		zringplusg 21396	. . . . . . . . . . . . . . . . . . . . 21 ⊢ + = (+g‘ℤring)
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → + = (+g‘ℤring))
187	186	ofeqd 7635	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∘f + = ∘f (+g‘ℤring))
188	187	oveqd 7386	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) = (𝑔 ∘f (+g‘ℤring)𝑖))
189	177	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 = (0g‘ℤring))
190	184, 188, 189	3brtr4d 5134	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) finSupp 0)
191	162, 169, 190	elrabd 3658	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
192	191, 17	eleqtrrdi 2839	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ 𝐹)
193		eqidd 2730	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
194	161, 192, 193	rspcedvdw 3588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
195		ovexd 7404	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V)
196	156, 194, 195	elrnmptd 5916	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
197	196, 52	eleqtrrdi 2839	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
198	151, 197	eqeltrd 2828	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
199	198	adantllr 719	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
200	199	adantllr 719	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
201	200	ad4ant13 751	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
202	103, 201	eqeltrd 2828	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆)
203	52	eleq2i 2820	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
204	126	oveq2d 7385	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
205	204	cbvmptv 5206	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
206	205	elrnmpt 5911	. . . . . . . . . . 11 ⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
207	206	elv 3449	. . . . . . . . . 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 726	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
211	202, 210	r19.29a 3141	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆)
212	58	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
213	211, 212	r19.29a 3141	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆)
214	213	ralrimiva 3125	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆)
215	2	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑅 ∈ Grp)
216	26	znegcld 12616	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) ∈ ℤ)
217	4, 15, 16, 216, 36	mulgcld 19010	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
218	217	fmpttd 7069	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵)
219	25	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑔:Word 𝐴⟶ℤ)
220		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
221	219, 220	fvco3d 6943	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤)))
222		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℤ ↦ -𝑧) = (𝑧 ∈ ℤ ↦ -𝑧)
223		negeq 11389	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑔‘𝑤) → -𝑧 = -(𝑔‘𝑤))
224	222, 223, 26, 216	fvmptd3 6973	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤)) = -(𝑔‘𝑤))
225	221, 224	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = -(𝑔‘𝑤))
226	225	oveq1d 7384	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤)) = (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))
227	226	mpteq2dva 5195	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
228		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
229	228	znegcld 12616	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → -𝑧 ∈ ℤ)
230	229	fmpttd 7069	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ)
231	230	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ)
232	231, 25	fcod 6695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔):Word 𝐴⟶ℤ)
233	21	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ℤ ∈ V)
234		negeq 11389	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 0 → -𝑧 = -0)
235		neg0 11444	. . . . . . . . . . . . . . 15 ⊢ -0 = 0
236	234, 235	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → -𝑧 = 0)
237		0zd 12517	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ ℤ)
238	222, 236, 237, 237	fvmptd3 6973	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0)
239	238	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0)
240	40, 25, 231, 14, 233, 45, 239	fsuppco2 9330	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔) finSupp 0)
241	39, 40, 14, 41, 36, 232, 240, 47	fisuppov1 32656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
242	227, 241	eqbrtrrd 5126	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
243	4, 5, 7, 14, 218, 242	gsumcl 19829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
244	243	ad4ant13 751	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
245	3	oveq1d 7384	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
246		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
247		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
248	4, 5, 104, 7, 14, 37, 217, 246, 247, 48, 242	gsummptfsadd 19838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
249	248	ad4ant13 751	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
250	26	zcnd 12615	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℂ)
251	250	negidd 11499	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) + -(𝑔‘𝑤)) = 0)
252	251	oveq1d 7384	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
253	4, 15, 104	mulgdir 19020	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ -(𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
254	16, 26, 216, 36, 253	syl13anc 1374	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
255	36, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
256	252, 254, 255	3eqtr3d 2772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (0g‘𝑅))
257	256	mpteq2dva 5195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))
258	257	oveq2d 7385	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))))
259	91	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅))
260	258, 259	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (0g‘𝑅))
261	260	ad4ant13 751	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (0g‘𝑅))
262	245, 249, 261	3eqtr2d 2770	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (0g‘𝑅))
263		eqid 2729	. . . . . . . . 9 ⊢ (invg‘𝑅) = (invg‘𝑅)
264	4, 104, 5, 263	grpinvid1 18905	. . . . . . . 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 1375	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ((invg‘𝑅)‘𝑥) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
267		fveq1 6839	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (ℎ‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤))
268	267	oveq1d 7384	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))
269	268	mpteq2dv 5196	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))
270	269	oveq2d 7385	. . . . . . . . . . 11 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))))
271	270	eqeq2d 2740	. . . . . . . . . 10 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))))
272		breq1 5105	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0))
273	25	ffvelcdmda 7038	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑔‘𝑣) ∈ ℤ)
274	273	znegcld 12616	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → -(𝑔‘𝑣) ∈ ℤ)
275	274	fmpttd 7069	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)):Word 𝐴⟶ℤ)
276	233, 14, 275	elmapdd 8791	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ (ℤ ↑m Word 𝐴))
277	275	ffund 6674	. . . . . . . . . . . . 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 12517	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 0 ∈ ℤ)
281		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
282	278, 279, 280, 281	fvdifsupp 8127	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → (𝑔‘𝑣) = 0)
283	282	negeqd 11391	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = -0)
284	283, 235	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = 0)
285	284, 14	suppss2 8156	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) supp 0) ⊆ (𝑔 supp 0))
286	276, 40, 277, 45, 285	fsuppsssuppgd 9309	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0)
287	272, 276, 286	elrabd 3658	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
288	287, 17	eleqtrrdi 2839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ 𝐹)
289		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))
290		fveq2 6840	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑤 → (𝑔‘𝑣) = (𝑔‘𝑤))
291	290	negeqd 11391	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑤 → -(𝑔‘𝑣) = -(𝑔‘𝑤))
292	289, 291, 220, 216	fvmptd3 6973	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) = -(𝑔‘𝑤))
293	292	eqcomd 2735	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤))
294	293	oveq1d 7384	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))
295	294	mpteq2dva 5195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))
296	295	oveq2d 7385	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))))
297	271, 288, 296	rspcedvdw 3588	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
298	156, 297, 243	elrnmptd 5916	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
299	298, 52	eleqtrrdi 2839	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
300	299	ad4ant13 751	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
301	266, 300	eqeltrd 2828	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ((invg‘𝑅)‘𝑥) ∈ 𝑆)
302	301, 58	r19.29a 3141	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((invg‘𝑅)‘𝑥) ∈ 𝑆)
303	214, 302	jca 511	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))
304	303	ralrimiva 3125	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))
305	4, 104, 263	issubg2 19055	. . 3 ⊢ (𝑅 ∈ Grp → (𝑆 ∈ (SubGrp‘𝑅) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))))
306	305	biimpar 477	. 2 ⊢ ((𝑅 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))) → 𝑆 ∈ (SubGrp‘𝑅))
307	2, 63, 100, 304, 306	syl13anc 1374	1 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3402  Vcvv 3444   ∖ cdif 3908   ⊆ wss 3911  ∅c0 4292  {csn 4585   class class class wbr 5102   ↦ cmpt 5183   × cxp 5629  ran crn 5632   ∘ ccom 5635   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369   ∘_f cof 7631   supp csupp 8116   ↑_m cmap 8776   finSupp cfsupp 9288  0cc0 11044   + caddc 11047  -cneg 11382  ℤcz 12505  Word cword 14454  Basecbs 17155  +_gcplusg 17196  0_gc0g 17378   Σ_g cgsu 17379  Mndcmnd 18643  Grpcgrp 18847  inv_gcminusg 18848  ._gcmg 18981  SubGrpcsubg 19034  CMndccmn 19694  mulGrpcmgp 20060  Ringcrg 20153  RingSpancrgspn 20530  ℤ_ringczring 21388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-addf 11123

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-om 7823  df-1st 7947  df-2nd 7948  df-supp 8117  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-er 8648  df-map 8778  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9289  df-oi 9439  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12419  df-z 12506  df-dec 12626  df-uz 12770  df-fz 13445  df-fzo 13592  df-seq 13943  df-hash 14272  df-word 14455  df-struct 17093  df-sets 17110  df-slot 17128  df-ndx 17140  df-base 17156  df-ress 17177  df-plusg 17209  df-mulr 17210  df-starv 17211  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-0g 17380  df-gsum 17381  df-mgm 18549  df-sgrp 18628  df-mnd 18644  df-submnd 18693  df-grp 18850  df-minusg 18851  df-mulg 18982  df-subg 19037  df-cntz 19231  df-cmn 19696  df-abl 19697  df-mgp 20061  df-rng 20073  df-ur 20102  df-ring 20155  df-cring 20156  df-subrng 20466  df-subrg 20490  df-cnfld 21297  df-zring 21389

This theorem is referenced by:  elrgspnlem2  33210