Theorem elrgspnlem1 33155

Description: Lemma for elrgspn 33159. (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 20187	. 2 ⊢ (𝜑 → 𝑅 ∈ Grp)
3		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
4		elrgspn.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑅)
5		eqid 2734	. . . . . . . . . 10 ⊢ (0g‘𝑅) = (0g‘𝑅)
6	1	ringcmnd 20229	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ CMnd)
7	6	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑅 ∈ CMnd)
8	4	fvexi 6886	. . . . . . . . . . . . . 14 ⊢ 𝐵 ∈ V
9	8	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ V)
10		elrgspn.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
11	9, 10	ssexd 5291	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ V)
12		wrdexg 14529	. . . . . . . . . . . 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 4055	. . . . . . . . . . . . . . . 16 ⊢ 𝐹 ⊆ (ℤ ↑m Word 𝐴)
19	18	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word 𝐴))
20	19	sselda 3956	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word 𝐴))
21		zex 12589	. . . . . . . . . . . . . . . . 17 ⊢ ℤ ∈ V
22	21	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ℤ ∈ V)
23	22, 13	elmapd 8848	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
24	23	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
25	20, 24	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
26	25	ffvelcdmda 7070	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
27		elrgspn.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (mulGrp‘𝑅)
28	27	ringmgp 20184	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
29	1, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ Mnd)
30		sswrd 14527	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
31	10, 30	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
32	31	sselda 3956	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
33	27, 4	mgpbas 20090	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝑀)
34	33	gsumwcl 18802	. . . . . . . . . . . . . 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 19064	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
38	37	fmpttd 7101	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵)
39		fvexd 6887	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V)
40		0zd 12592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ)
41		ssidd 3980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴)
42		breq1 5119	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
43	42, 17	elrab2 3672	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
44	43	simprbi 496	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
45	44	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
46	4, 5, 15	mulg0 19042	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅))
47	46	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅))
48	39, 40, 14, 41, 36, 25, 45, 47	fisuppov1 32593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
49	4, 5, 7, 14, 38, 48	gsumcl 19881	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
50	49	ad4ant13 751	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
51	3, 50	eqeltrd 2833	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 ∈ 𝐵)
52		elrgspnlem1.1	. . . . . . . . . 10 ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
53	52	eleq2i 2825	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
54		eqid 2734	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
55	54	elrnmpt 5935	. . . . . . . . . 10 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
56	55	elv 3462	. . . . . . . . 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 2843	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑅))
61	60	ex 412	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ (Base‘𝑅)))
62	61	ssrdv 3962	. . 3 ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑅))
63	62, 4	sseqtrrdi 3998	. 2 ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
64		breq1 5119	. . . . . . . 8 ⊢ (𝑓 = (Word 𝐴 × {0}) → (𝑓 finSupp 0 ↔ (Word 𝐴 × {0}) finSupp 0))
65		0z 12591	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
66	65	fconst6 6764	. . . . . . . . . 10 ⊢ (Word 𝐴 × {0}):Word 𝐴⟶ℤ
67	66	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (Word 𝐴 × {0}):Word 𝐴⟶ℤ)
68	22, 13, 67	elmapdd 8849	. . . . . . . 8 ⊢ (𝜑 → (Word 𝐴 × {0}) ∈ (ℤ ↑m Word 𝐴))
69		c0ex 11221	. . . . . . . . . 10 ⊢ 0 ∈ V
70	69	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ V)
71	13, 70	fczfsuppd 9392	. . . . . . . 8 ⊢ (𝜑 → (Word 𝐴 × {0}) finSupp 0)
72	64, 68, 71	elrabd 3671	. . . . . . 7 ⊢ (𝜑 → (Word 𝐴 × {0}) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
73	72, 17	eleqtrrdi 2844	. . . . . 6 ⊢ (𝜑 → (Word 𝐴 × {0}) ∈ 𝐹)
74		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → 𝑔 = (Word 𝐴 × {0}))
75	74	fveq1d 6874	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = ((Word 𝐴 × {0})‘𝑤))
76	69	fconst 6760	. . . . . . . . . . . . . . 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 7150	. . . . . . . . . . . . . 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 2769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = 0)
82	81	oveq1d 7414	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
83	35	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
84	4, 5, 15	mulg0 19042	. . . . . . . . . . . 12 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
85	83, 84	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
86	82, 85	eqtrd 2769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
87	86	mpteq2dva 5211	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))
88	87	oveq2d 7415	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))))
89	6	cmnmndd 19770	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Mnd)
90	5	gsumz 18799	. . . . . . . . . 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 2769	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (0g‘𝑅))
94	93	eqeq2d 2745	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → ((0g‘𝑅) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (0g‘𝑅) = (0g‘𝑅)))
95		eqidd 2735	. . . . . 6 ⊢ (𝜑 → (0g‘𝑅) = (0g‘𝑅))
96	73, 94, 95	rspcedvd 3601	. . . . 5 ⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (0g‘𝑅) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
97		fvexd 6887	. . . . 5 ⊢ (𝜑 → (0g‘𝑅) ∈ V)
98	54, 96, 97	elrnmptd 5940	. . . 4 ⊢ (𝜑 → (0g‘𝑅) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
99	98, 52	eleqtrrdi 2844	. . 3 ⊢ (𝜑 → (0g‘𝑅) ∈ 𝑆)
100	99	ne0d 4315	. 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 7417	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
104		eqid 2734	. . . . . . . . . . . . . 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 5119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0))
110	109, 17	elrab2 3672	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑖 finSupp 0))
111	110	simplbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word 𝐴))
112	111	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word 𝐴))
113	22, 13	elmapd 8848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
114	113	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
115	112, 114	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
116	115	ffvelcdmda 7070	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ)
117	35	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
118	4, 15, 108, 116, 117	mulgcld 19064	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
119	118	adantllr 719	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
120		eqidd 2735	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
121		eqidd 2735	. . . . . . . . . . . . . 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 6871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤))
125	124	oveq1d 7414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
126	125	mpteq2dv 5212	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
127	126	breq1d 5126	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅)))
128	127	cbvralvw 3218	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
129	123, 128	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
130	129	r19.21bi 3232	. . . . . . . . . . . . . . 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 19890	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
133	25	ffnd 6703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
134	133	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
135	115	ffnd 6703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
136	135	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
137		inidm 4200	. . . . . . . . . . . . . . . . . 18 ⊢ (Word 𝐴 ∩ Word 𝐴) = Word 𝐴
138		eqidd 2735	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = (𝑔‘𝑤))
139		eqidd 2735	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) = (𝑖‘𝑤))
140	134, 136, 106, 106, 137, 138, 139	ofval 7676	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔 ∘f + 𝑖)‘𝑤) = ((𝑔‘𝑤) + (𝑖‘𝑤)))
141	140	oveq1d 7414	. . . . . . . . . . . . . . . 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 19074	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
147	142, 143, 144, 145, 146	syl13anc 1373	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
148	141, 147	eqtr2d 2770	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))
149	148	mpteq2dva 5211	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))
150	149	oveq2d 7415	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
151	132, 150	eqtr3d 2771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
152		fveq1 6871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤))
153	152	oveq1d 7414	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))
154	153	mpteq2dv 5212	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))
155	154	oveq2d 7415	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
156	155	cbvmptv 5222	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
157		fveq1 6871	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → (ℎ‘𝑤) = ((𝑔 ∘f + 𝑖)‘𝑤))
158	157	oveq1d 7414	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))
159	158	mpteq2dv 5212	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))
160	159	oveq2d 7415	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
161	160	eqeq2d 2745	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))))
162		breq1 5119	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑔 ∘f + 𝑖) → (𝑓 finSupp 0 ↔ (𝑔 ∘f + 𝑖) finSupp 0))
163	21	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V)
164		zaddcl 12624	. . . . . . . . . . . . . . . . . . . 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 7683	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖):Word 𝐴⟶ℤ)
169	163, 106, 168	elmapdd 8849	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ (ℤ ↑m Word 𝐴))
170		zringring 21395	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℤring ∈ Ring
171		ringmnd 20188	. . . . . . . . . . . . . . . . . . . . 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 21404	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 = (0g‘ℤring)
178	176, 177	breqtrdi 5157	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 finSupp (0g‘ℤring))
179	110	simprbi 496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0)
180	179	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0)
181	180, 177	breqtrdi 5157	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp (0g‘ℤring))
182		zringbas 21399	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℤ = (Base‘ℤring)
183	182	mndpfsupp 18730	. . . . . . . . . . . . . . . . . . 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 1387	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f (+g‘ℤring)𝑖) finSupp (0g‘ℤring))
185		zringplusg 21400	. . . . . . . . . . . . . . . . . . . . 21 ⊢ + = (+g‘ℤring)
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → + = (+g‘ℤring))
187	186	ofeqd 7667	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∘f + = ∘f (+g‘ℤring))
188	187	oveqd 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) = (𝑔 ∘f (+g‘ℤring)𝑖))
189	177	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 = (0g‘ℤring))
190	184, 188, 189	3brtr4d 5148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) finSupp 0)
191	162, 169, 190	elrabd 3671	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
192	191, 17	eleqtrrdi 2844	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ 𝐹)
193		eqidd 2735	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))
194	161, 192, 193	rspcedvdw 3602	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
195		ovexd 7434	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V)
196	156, 194, 195	elrnmptd 5940	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
197	196, 52	eleqtrrdi 2844	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
198	151, 197	eqeltrd 2833	. . . . . . . . . . 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 2833	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆)
203	52	eleq2i 2825	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
204	126	oveq2d 7415	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
205	204	cbvmptv 5222	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
206	205	elrnmpt 5935	. . . . . . . . . . 11 ⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
207	206	elv 3462	. . . . . . . . . 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 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 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑅 ∈ Grp)
216	26	znegcld 12691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) ∈ ℤ)
217	4, 15, 16, 216, 36	mulgcld 19064	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
218	217	fmpttd 7101	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵)
219	25	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑔:Word 𝐴⟶ℤ)
220		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴)
221	219, 220	fvco3d 6975	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤)))
222		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℤ ↦ -𝑧) = (𝑧 ∈ ℤ ↦ -𝑧)
223		negeq 11466	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑔‘𝑤) → -𝑧 = -(𝑔‘𝑤))
224	222, 223, 26, 216	fvmptd3 7005	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤)) = -(𝑔‘𝑤))
225	221, 224	eqtrd 2769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = -(𝑔‘𝑤))
226	225	oveq1d 7414	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤)) = (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))
227	226	mpteq2dva 5211	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
228		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
229	228	znegcld 12691	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → -𝑧 ∈ ℤ)
230	229	fmpttd 7101	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ)
231	230	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ)
232	231, 25	fcod 6727	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔):Word 𝐴⟶ℤ)
233	21	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ℤ ∈ V)
234		negeq 11466	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 0 → -𝑧 = -0)
235		neg0 11521	. . . . . . . . . . . . . . 15 ⊢ -0 = 0
236	234, 235	eqtrdi 2785	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 0 → -𝑧 = 0)
237		0zd 12592	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ ℤ)
238	222, 236, 237, 237	fvmptd3 7005	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0)
239	238	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0)
240	40, 25, 231, 14, 233, 45, 239	fsuppco2 9409	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔) finSupp 0)
241	39, 40, 14, 41, 36, 232, 240, 47	fisuppov1 32593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
242	227, 241	eqbrtrrd 5140	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
243	4, 5, 7, 14, 218, 242	gsumcl 19881	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
244	243	ad4ant13 751	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵)
245	3	oveq1d 7414	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
246		eqidd 2735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
247		eqidd 2735	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
248	4, 5, 104, 7, 14, 37, 217, 246, 247, 48, 242	gsummptfsadd 19890	. . . . . . . . 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 12690	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℂ)
251	250	negidd 11576	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) + -(𝑔‘𝑤)) = 0)
252	251	oveq1d 7414	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
253	4, 15, 104	mulgdir 19074	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ -(𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
254	16, 26, 216, 36, 253	syl13anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))
255	36, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
256	252, 254, 255	3eqtr3d 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (0g‘𝑅))
257	256	mpteq2dva 5211	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))
258	257	oveq2d 7415	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))))
259	91	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅))
260	258, 259	eqtrd 2769	. . . . . . . . 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 2775	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (0g‘𝑅))
263		eqid 2734	. . . . . . . . 9 ⊢ (invg‘𝑅) = (invg‘𝑅)
264	4, 104, 5, 263	grpinvid1 18959	. . . . . . . 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 1374	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ((invg‘𝑅)‘𝑥) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
267		fveq1 6871	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (ℎ‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤))
268	267	oveq1d 7414	. . . . . . . . . . . . 13 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))
269	268	mpteq2dv 5212	. . . . . . . . . . . 12 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))
270	269	oveq2d 7415	. . . . . . . . . . 11 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))))
271	270	eqeq2d 2745	. . . . . . . . . 10 ⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))))
272		breq1 5119	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0))
273	25	ffvelcdmda 7070	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑔‘𝑣) ∈ ℤ)
274	273	znegcld 12691	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → -(𝑔‘𝑣) ∈ ℤ)
275	274	fmpttd 7101	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)):Word 𝐴⟶ℤ)
276	233, 14, 275	elmapdd 8849	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ (ℤ ↑m Word 𝐴))
277	275	ffund 6706	. . . . . . . . . . . . 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 12592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 0 ∈ ℤ)
281		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
282	278, 279, 280, 281	fvdifsupp 8164	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → (𝑔‘𝑣) = 0)
283	282	negeqd 11468	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = -0)
284	283, 235	eqtrdi 2785	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = 0)
285	284, 14	suppss2 8193	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) supp 0) ⊆ (𝑔 supp 0))
286	276, 40, 277, 45, 285	fsuppsssuppgd 9388	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0)
287	272, 276, 286	elrabd 3671	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
288	287, 17	eleqtrrdi 2844	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ 𝐹)
289		eqid 2734	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))
290		fveq2 6872	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑤 → (𝑔‘𝑣) = (𝑔‘𝑤))
291	290	negeqd 11468	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑤 → -(𝑔‘𝑣) = -(𝑔‘𝑤))
292	289, 291, 220, 216	fvmptd3 7005	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) = -(𝑔‘𝑤))
293	292	eqcomd 2740	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤))
294	293	oveq1d 7414	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))
295	294	mpteq2dva 5211	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))
296	295	oveq2d 7415	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))))
297	271, 288, 296	rspcedvdw 3602	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
298	156, 297, 243	elrnmptd 5940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
299	298, 52	eleqtrrdi 2844	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
300	299	ad4ant13 751	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
301	266, 300	eqeltrd 2833	. . . . 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 19109	. . 3 ⊢ (𝑅 ∈ Grp → (𝑆 ∈ (SubGrp‘𝑅) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))))
306	305	biimpar 477	. 2 ⊢ ((𝑅 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))) → 𝑆 ∈ (SubGrp‘𝑅))
307	2, 63, 100, 304, 306	syl13anc 1373	1 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2931  ∀wral 3050  ∃wrex 3059  {crab 3413  Vcvv 3457   ∖ cdif 3921   ⊆ wss 3924  ∅c0 4306  {csn 4599   class class class wbr 5116   ↦ cmpt 5198   × cxp 5649  ran crn 5652   ∘ ccom 5655   Fn wfn 6522  ⟶wf 6523  ‘cfv 6527  (class class class)co 7399   ∘_f cof 7663   supp csupp 8153   ↑_m cmap 8834   finSupp cfsupp 9367  0cc0 11121   + caddc 11124  -cneg 11459  ℤcz 12580  Word cword 14519  Basecbs 17213  +_gcplusg 17256  0_gc0g 17438   Σ_g cgsu 17439  Mndcmnd 18697  Grpcgrp 18901  inv_gcminusg 18902  ._gcmg 19035  SubGrpcsubg 19088  CMndccmn 19746  mulGrpcmgp 20085  Ringcrg 20178  RingSpancrgspn 20555  ℤ_ringczring 21392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5246  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723  ax-cnex 11177  ax-resscn 11178  ax-1cn 11179  ax-icn 11180  ax-addcl 11181  ax-addrcl 11182  ax-mulcl 11183  ax-mulrcl 11184  ax-mulcom 11185  ax-addass 11186  ax-mulass 11187  ax-distr 11188  ax-i2m1 11189  ax-1ne0 11190  ax-1rid 11191  ax-rnegex 11192  ax-rrecex 11193  ax-cnre 11194  ax-pre-lttri 11195  ax-pre-lttrn 11196  ax-pre-ltadd 11197  ax-pre-mulgt0 11198  ax-addf 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3357  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-tp 4604  df-op 4606  df-uni 4881  df-int 4920  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-tr 5227  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6287  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-isom 6536  df-riota 7356  df-ov 7402  df-oprab 7403  df-mpo 7404  df-of 7665  df-om 7856  df-1st 7982  df-2nd 7983  df-supp 8154  df-frecs 8274  df-wrecs 8305  df-recs 8379  df-rdg 8418  df-1o 8474  df-er 8713  df-map 8836  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-fsupp 9368  df-oi 9516  df-card 9945  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11460  df-neg 11461  df-nn 12233  df-2 12295  df-3 12296  df-4 12297  df-5 12298  df-6 12299  df-7 12300  df-8 12301  df-9 12302  df-n0 12494  df-z 12581  df-dec 12701  df-uz 12845  df-fz 13514  df-fzo 13661  df-seq 14009  df-hash 14337  df-word 14520  df-struct 17151  df-sets 17168  df-slot 17186  df-ndx 17198  df-base 17214  df-ress 17237  df-plusg 17269  df-mulr 17270  df-starv 17271  df-tset 17275  df-ple 17276  df-ds 17278  df-unif 17279  df-0g 17440  df-gsum 17441  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-submnd 18747  df-grp 18904  df-minusg 18905  df-mulg 19036  df-subg 19091  df-cntz 19285  df-cmn 19748  df-abl 19749  df-mgp 20086  df-rng 20098  df-ur 20127  df-ring 20180  df-cring 20181  df-subrng 20491  df-subrg 20515  df-cnfld 21301  df-zring 21393

This theorem is referenced by:  elrgspnlem2  33156