Theorem elrgspnlem2 33304

Description: Lemma for elrgspn 33307. (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
elrgspnlem2	⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))

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

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

Proof of Theorem elrgspnlem2

Dummy variables 𝑎 ℎ 𝑖 𝑗 𝑡 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elrgspn.r	. 2 ⊢ (𝜑 → 𝑅 ∈ Ring)
2		elrgspn.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
3		elrgspn.m	. . 3 ⊢ 𝑀 = (mulGrp‘𝑅)
4		elrgspn.x	. . 3 ⊢ · = (.g‘𝑅)
5		elrgspn.n	. . 3 ⊢ 𝑁 = (RingSpan‘𝑅)
6		elrgspn.f	. . 3 ⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0}
7		elrgspn.a	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
8		elrgspnlem1.1	. . 3 ⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
9	2, 3, 4, 5, 6, 1, 7, 8	elrgspnlem1 33303	. 2 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))
10		eqeq2 2748	. . . . . . 7 ⊢ ((1r‘𝑅) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))
11		eqeq2 2748	. . . . . . 7 ⊢ ((0g‘𝑅) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))
12		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → 𝑤 = ∅)
13	12	fveq2d 6844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅))
14		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))
15		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 = ∅) → 𝑣 = ∅)
16	15	iftrued 4474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 = ∅) → if(𝑣 = ∅, 1, 0) = 1)
17		wrd0 14501	. . . . . . . . . . . . 13 ⊢ ∅ ∈ Word 𝐴
18	17	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ∈ Word 𝐴)
19		1zzd 12558	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
20	14, 16, 18, 19	fvmptd2 6956	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
21	20	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
22	13, 21	eqtrd 2771	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 1)
23	12	oveq2d 7383	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (𝑀 Σg ∅))
24		eqid 2736	. . . . . . . . . . . 12 ⊢ (1r‘𝑅) = (1r‘𝑅)
25	3, 24	ringidval 20164	. . . . . . . . . . 11 ⊢ (1r‘𝑅) = (0g‘𝑀)
26	25	gsum0 18652	. . . . . . . . . 10 ⊢ (𝑀 Σg ∅) = (1r‘𝑅)
27	23, 26	eqtrdi 2787	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (1r‘𝑅))
28	22, 27	oveq12d 7385	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1 · (1r‘𝑅)))
29	2, 24	ringidcl 20246	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐵)
30	1, 29	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵)
31	2, 4	mulg1 19057	. . . . . . . . . 10 ⊢ ((1r‘𝑅) ∈ 𝐵 → (1 · (1r‘𝑅)) = (1r‘𝑅))
32	30, 31	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (1 · (1r‘𝑅)) = (1r‘𝑅))
33	32	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (1 · (1r‘𝑅)) = (1r‘𝑅))
34	28, 33	eqtrd 2771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅))
35		eqeq1 2740	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑤 → (𝑣 = ∅ ↔ 𝑤 = ∅))
36	35	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑤 → (¬ 𝑣 = ∅ ↔ ¬ 𝑤 = ∅))
37	36	biimparc 479	. . . . . . . . . . . 12 ⊢ ((¬ 𝑤 = ∅ ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
38	37	adantll 715	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
39	38	iffalsed 4477	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → if(𝑣 = ∅, 1, 0) = 0)
40		simplr 769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 𝑤 ∈ Word 𝐴)
41		0zd 12536	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 0 ∈ ℤ)
42	14, 39, 40, 41	fvmptd2 6956	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 0)
43	42	oveq1d 7382	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
44	3	ringmgp 20220	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
45	1, 44	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ Mnd)
46		sswrd 14484	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
47	7, 46	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
48	47	sselda 3921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
49	3, 2	mgpbas 20126	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑀)
50	49	gsumwcl 18807	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
51	45, 48, 50	syl2an2r 686	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
52		eqid 2736	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
53	2, 52, 4	mulg0 19050	. . . . . . . . . 10 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
54	51, 53	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
55	54	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
56	43, 55	eqtrd 2771	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
57	10, 11, 34, 56	ifbothda 4505	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))
58	57	mpteq2dva 5178	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))
59	58	oveq2d 7383	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))))
60	1	ringcmnd 20265	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
61	60	cmnmndd 19779	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Mnd)
62	2	fvexi 6854	. . . . . . . 8 ⊢ 𝐵 ∈ V
63	62	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
64	63, 7	ssexd 5265	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ V)
65		wrdexg 14486	. . . . . 6 ⊢ (𝐴 ∈ V → Word 𝐴 ∈ V)
66	64, 65	syl 17	. . . . 5 ⊢ (𝜑 → Word 𝐴 ∈ V)
67		eqid 2736	. . . . 5 ⊢ (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))
68	30, 2	eleqtrdi 2846	. . . . 5 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
69	52, 61, 66, 18, 67, 68	gsummptif1n0 19941	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) = (1r‘𝑅))
70	59, 69	eqtrd 2771	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (1r‘𝑅))
71		eqid 2736	. . . . 5 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
72		fveq1 6839	. . . . . . . . . 10 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤))
73	72	oveq1d 7382	. . . . . . . . 9 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))
74	73	mpteq2dv 5179	. . . . . . . 8 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))
75	74	oveq2d 7383	. . . . . . 7 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
76	75	eqeq2d 2747	. . . . . 6 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))))
77		breq1 5088	. . . . . . . 8 ⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0))
78		zex 12533	. . . . . . . . . 10 ⊢ ℤ ∈ V
79	78	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℤ ∈ V)
80		1zzd 12558	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑣 = ∅) → 1 ∈ ℤ)
81		0zd 12536	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ ¬ 𝑣 = ∅) → 0 ∈ ℤ)
82	80, 81	ifclda 4502	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ Word 𝐴) → if(𝑣 = ∅, 1, 0) ∈ ℤ)
83	82	fmpttd 7067	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)):Word 𝐴⟶ℤ)
84	79, 66, 83	elmapdd 8788	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ (ℤ ↑m Word 𝐴))
85	66	mptexd 7179	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V)
86	83	ffund 6672	. . . . . . . . 9 ⊢ (𝜑 → Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)))
87		0zd 12536	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
88		snfi 8990	. . . . . . . . . 10 ⊢ {∅} ∈ Fin
89	88	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {∅} ∈ Fin)
90		eldifsni 4735	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (Word 𝐴 ∖ {∅}) → 𝑣 ≠ ∅)
91	90	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → 𝑣 ≠ ∅)
92	91	neneqd 2937	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → ¬ 𝑣 = ∅)
93	92	iffalsed 4477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → if(𝑣 = ∅, 1, 0) = 0)
94	93, 66	suppss2 8150	. . . . . . . . 9 ⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆ {∅})
95		suppssfifsupp 9293	. . . . . . . . 9 ⊢ ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V ∧ Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∧ 0 ∈ ℤ) ∧ ({∅} ∈ Fin ∧ ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆ {∅})) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0)
96	85, 86, 87, 89, 94, 95	syl32anc 1381	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0)
97	77, 84, 96	elrabd 3636	. . . . . . 7 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
98	97, 6	eleqtrrdi 2847	. . . . . 6 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ 𝐹)
99		eqidd 2737	. . . . . 6 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
100	76, 98, 99	rspcedvdw 3567	. . . . 5 ⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
101		ovexd 7402	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V)
102	71, 100, 101	elrnmptd 5918	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
103	102, 8	eleqtrrdi 2847	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
104	70, 103	eqeltrrd 2837	. 2 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆)
105		simpllr 776	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
106		simpr 484	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
107	105, 106	oveq12d 7385	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
108		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (.r‘𝑅) = (.r‘𝑅)
109	66	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ∈ V)
110	1	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ Ring)
111	1	ringgrpd 20223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 ∈ Grp)
112	111	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
113	6	ssrab3 4022	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 ⊆ (ℤ ↑m Word 𝐴)
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word 𝐴))
115	114	sselda 3921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word 𝐴))
116	79, 66	elmapd 8787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
117	116	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
118	115, 117	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
119	118	ffvelcdmda 7036	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
120	51	adantlr 716	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
121	2, 4, 112, 119, 120	mulgcld 19072	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
122	121	adantlr 716	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
123	122	ralrimiva 3129	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
124		fveq2 6840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑤 → (𝑔‘𝑢) = (𝑔‘𝑤))
125		oveq2 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑤 → (𝑀 Σg 𝑢) = (𝑀 Σg 𝑤))
126	124, 125	oveq12d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑤 → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
127	126	eleq1d 2821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
128	127	cbvralvw 3215	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑢 ∈ Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
129	123, 128	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑢 ∈ Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
130	129	r19.21bi 3229	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑢 ∈ Word 𝐴) → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
131	111	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
132		breq1 5088	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0))
133	132, 6	elrab2 3637	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑖 finSupp 0))
134	133	simplbi 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word 𝐴))
135	134	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word 𝐴))
136	79, 66	elmapd 8787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
137	136	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
138	135, 137	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
139	138	ffvelcdmda 7036	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ)
140	51	adantlr 716	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
141	2, 4, 131, 139, 140	mulgcld 19072	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
142	141	adantllr 720	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
143	142	ralrimiva 3129	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
144		fveq2 6840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑖‘𝑣) = (𝑖‘𝑤))
145		oveq2 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑤))
146	144, 145	oveq12d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑤 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
147	146	eleq1d 2821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑤 → (((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
148	147	cbvralvw 3215	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑣 ∈ Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
149	143, 148	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑣 ∈ Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
150	149	r19.21bi 3229	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
151	126	cbvmptv 5189	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
152		fvexd 6855	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V)
153		0zd 12536	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ)
154	66	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ∈ V)
155		ssidd 3945	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴)
156		breq1 5088	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
157	156, 6	elrab2 3637	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
158	157	simprbi 497	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
159	158	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
160	2, 52, 4	mulg0 19050	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅))
161	160	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅))
162	152, 153, 154, 155, 120, 118, 159, 161	fisuppov1 32756	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
163	162	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
164	151, 163	eqbrtrid 5120	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) finSupp (0g‘𝑅))
165	146	cbvmptv 5189	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
166	162	ralrimiva 3129	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
167		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤))
168	167	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
169	168	mpteq2dv 5179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
170	169	breq1d 5095	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅)))
171	170	cbvralvw 3215	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
172	166, 171	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
173	172	r19.21bi 3229	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
174	173	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
175	165, 174	eqbrtrid 5120	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) finSupp (0g‘𝑅))
176	2, 108, 52, 109, 109, 110, 130, 150, 164, 175	gsumdixp 20298	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))))(.r‘𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))))
177	151	oveq2i 7378	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
178	165	oveq2i 7378	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
179	177, 178	oveq12i 7379	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))))(.r‘𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
180	179	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))))(.r‘𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
181	110	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Ring)
182	122	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
183	111	ad4antr 733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Grp)
184	138	adantlr 716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
185	184	ffvelcdmda 7036	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑓 ∈ Word 𝐴) → (𝑖‘𝑓) ∈ ℤ)
186	185	adantlr 716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑖‘𝑓) ∈ ℤ)
187	45	ad4antr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
188	47	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐵)
189	188	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵)
190	189	sselda 3921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑓 ∈ Word 𝐵)
191	49	gsumwcl 18807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg 𝑓) ∈ 𝐵)
192	187, 190, 191	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑓) ∈ 𝐵)
193	2, 4, 183, 186, 192	mulgcld 19072	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)
194	2, 108, 181, 182, 193	ringcld 20241	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
195	194	anasss 466	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
196	195	ralrimivva 3180	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴∀𝑓 ∈ Word 𝐴(((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
197		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
198	197	fmpo 8021	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ Word 𝐴∀𝑓 ∈ Word 𝐴(((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵 ↔ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵)
199	196, 198	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵)
200		vex 3433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑤 ∈ V
201		vex 3433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑓 ∈ V
202	200, 201	op1std 7952	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (1st ‘𝑎) = 𝑤)
203	202	fveq2d 6844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑔‘(1st ‘𝑎)) = (𝑔‘𝑤))
204	202	oveq2d 7383	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (1st ‘𝑎)) = (𝑀 Σg 𝑤))
205	203, 204	oveq12d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
206	200, 201	op2ndd 7953	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (2nd ‘𝑎) = 𝑓)
207	206	fveq2d 6844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑖‘(2nd ‘𝑎)) = (𝑖‘𝑓))
208	206	oveq2d 7383	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (2nd ‘𝑎)) = (𝑀 Σg 𝑓))
209	207, 208	oveq12d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓)))
210	205, 209	oveq12d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
211	210	mpompt 7481	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
212	66, 66	xpexd 7705	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Word 𝐴 × Word 𝐴) ∈ V)
213	212	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (Word 𝐴 × Word 𝐴) ∈ V)
214	213	mptexd 7179	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) ∈ V)
215		fvexd 6855	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (0g‘𝑅) ∈ V)
216	110	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Ring)
217	111	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Grp)
218	118	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ)
219		xp1st 7974	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1st ‘𝑎) ∈ Word 𝐴)
220	219	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴)
221	218, 220	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑔‘(1st ‘𝑎)) ∈ ℤ)
222	216, 44	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑀 ∈ Mnd)
223	188	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵)
224	223, 220	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐵)
225	49	gsumwcl 18807	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ (1st ‘𝑎) ∈ Word 𝐵) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
226	222, 224, 225	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
227	2, 4, 217, 221, 226	mulgcld 19072	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) ∈ 𝐵)
228	184	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ)
229		xp2nd 7975	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴)
230	229	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴)
231	228, 230	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈ ℤ)
232	223, 230	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐵)
233	49	gsumwcl 18807	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ (2nd ‘𝑎) ∈ Word 𝐵) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
234	222, 232, 233	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
235	2, 4, 217, 231, 234	mulgcld 19072	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) ∈ 𝐵)
236	2, 108, 216, 227, 235	ringcld 20241	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) ∈ 𝐵)
237	236	fmpttd 7067	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))):(Word 𝐴 × Word 𝐴)⟶𝐵)
238	237	ffund 6672	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Fun (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))))
239	159	fsuppimpd 9282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin)
240	133	simprbi 497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0)
241	240	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0)
242	241	fsuppimpd 9282	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑖 supp 0) ∈ Fin)
243		xpfi 9230	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 supp 0) ∈ Fin ∧ (𝑖 supp 0) ∈ Fin) → ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin)
244	239, 242, 243	syl2an2r 686	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin)
245	118	ffnd 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
246	245	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
247	246	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑔 Fn Word 𝐴)
248	109	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ∈ V)
249		0zd 12536	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 0 ∈ ℤ)
250		xp1st 7974	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (1st ‘𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
251	250	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
252	247, 248, 249, 251	fvdifsupp 8121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑔‘(1st ‘𝑎)) = 0)
253	252	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) = (0 · (𝑀 Σg (1st ‘𝑎))))
254	45	ad4antr 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑀 ∈ Mnd)
255	188	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵)
256	251	eldifad 3901	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴)
257	255, 256	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐵)
258	254, 257, 225	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
259	2, 52, 4	mulg0 19050	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 Σg (1st ‘𝑎)) ∈ 𝐵 → (0 · (𝑀 Σg (1st ‘𝑎))) = (0g‘𝑅))
260	258, 259	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (0 · (𝑀 Σg (1st ‘𝑎))) = (0g‘𝑅))
261	253, 260	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) = (0g‘𝑅))
262	261	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = ((0g‘𝑅)(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))))
263	110	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Ring)
264	111	ad4antr 733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Grp)
265	184	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ)
266		xp2nd 7975	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴)
267	266	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴)
268	265, 267	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈ ℤ)
269	255, 267	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐵)
270	254, 269, 233	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
271	2, 4, 264, 268, 270	mulgcld 19072	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) ∈ 𝐵)
272	2, 108, 52, 263, 271	ringlzd 20276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((0g‘𝑅)(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
273	262, 272	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
274	138	ffnd 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
275	274	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
276	275	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑖 Fn Word 𝐴)
277	109	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ∈ V)
278		0zd 12536	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 0 ∈ ℤ)
279		xp2nd 7975	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (2nd ‘𝑎) ∈ (Word 𝐴 ∖ (𝑖 supp 0)))
280	279	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd ‘𝑎) ∈ (Word 𝐴 ∖ (𝑖 supp 0)))
281	276, 277, 278, 280	fvdifsupp 8121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑖‘(2nd ‘𝑎)) = 0)
282	281	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) = (0 · (𝑀 Σg (2nd ‘𝑎))))
283	45	ad4antr 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑀 ∈ Mnd)
284	188	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ⊆ Word 𝐵)
285	280	eldifad 3901	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd ‘𝑎) ∈ Word 𝐴)
286	284, 285	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd ‘𝑎) ∈ Word 𝐵)
287	283, 286, 233	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
288	2, 52, 4	mulg0 19050	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵 → (0 · (𝑀 Σg (2nd ‘𝑎))) = (0g‘𝑅))
289	287, 288	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (0 · (𝑀 Σg (2nd ‘𝑎))) = (0g‘𝑅))
290	282, 289	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) = (0g‘𝑅))
291	290	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)(0g‘𝑅)))
292	110	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Ring)
293	111	ad4antr 733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Grp)
294	118	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
295	294	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑔:Word 𝐴⟶ℤ)
296		xp1st 7974	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (1st ‘𝑎) ∈ Word 𝐴)
297	296	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st ‘𝑎) ∈ Word 𝐴)
298	295, 297	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑔‘(1st ‘𝑎)) ∈ ℤ)
299	284, 297	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st ‘𝑎) ∈ Word 𝐵)
300	283, 299, 225	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
301	2, 4, 293, 298, 300	mulgcld 19072	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) ∈ 𝐵)
302	2, 108, 52, 292, 301	ringrzd 20277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
303	291, 302	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
304		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))))
305		difxp 6128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))) = (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))))
306	304, 305	eleqtrdi 2846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
307		elun 4093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) ↔ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
308	306, 307	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
309	273, 303, 308	mpjaodan 961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
310	309, 213	suppss2 8150	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) supp (0g‘𝑅)) ⊆ ((𝑔 supp 0) × (𝑖 supp 0)))
311	244, 310	ssfid 9179	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) supp (0g‘𝑅)) ∈ Fin)
312	214, 215, 238, 311	isfsuppd 9279	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) finSupp (0g‘𝑅))
313	211, 312	eqbrtrrid 5121	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) finSupp (0g‘𝑅))
314	60	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ CMnd)
315	7	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝐴 ⊆ 𝐵)
316	2, 52, 199, 313, 314, 315	gsumwrd2dccat 33139	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
317	126	oveq1d 7382	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))
318		fveq2 6840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑓 → (𝑖‘𝑣) = (𝑖‘𝑓))
319		oveq2 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑓 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑓))
320	318, 319	oveq12d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑓 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓)))
321	320	oveq2d 7383	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑓 → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
322	317, 321	cbvmpov 7462	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
323	322	oveq2i 7378	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))))
324	323	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))))
325		pfxcctswrd 14672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ Word 𝐴 ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
326	325	adantll 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
327	326	oveq2d 7383	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) = (𝑀 Σg 𝑣))
328	327	oveq2d 7383	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
329	328	mpteq2dva 5178	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣))))
330	329	oveq2d 7383	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
331		df-ov 7370	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)
332	188	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
333	332	ad4ant13 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
334	187, 333, 50	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
335	2, 4, 108	mulgass3 20333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ Ring ∧ ((𝑖‘𝑓) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ (𝑀 Σg 𝑓) ∈ 𝐵)) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
336	181, 186, 334, 192, 335	syl13anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
337	336	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))))
338	119	ad4ant13 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
339	2, 4, 108	mulgass2 20290	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ Ring ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))))
340	181, 338, 334, 193, 339	syl13anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))))
341	2, 108, 181, 334, 192	ringcld 20241	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)
342	2, 4	mulgass 19087	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑓) ∈ ℤ ∧ ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))))
343	183, 338, 186, 341, 342	syl13anc 1375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))))
344	337, 340, 343	3eqtr4d 2781	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
345	3, 108	mgpplusg 20125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (.r‘𝑅) = (+g‘𝑀)
346	49, 345	gsumccat 18809	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))
347	187, 333, 190, 346	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))
348	347	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
349	344, 348	eqtr4d 2774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
350	349	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
351	350	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
352	351	3impa 1110	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
353	352	mpoeq3dva 7444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓)))))
354		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑣 prefix 𝑗) → (𝑔‘𝑤) = (𝑔‘(𝑣 prefix 𝑗)))
355		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) → (𝑖‘𝑓) = (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
356	354, 355	oveqan12d 7386	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → ((𝑔‘𝑤) · (𝑖‘𝑓)) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
357		oveq12 7376	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑤 ++ 𝑓) = ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
358	357	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑀 Σg (𝑤 ++ 𝑓)) = (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
359	356, 358	oveq12d 7385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
360	359	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ (𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
361		pfxcl 14640	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ Word 𝐴 → (𝑣 prefix 𝑗) ∈ Word 𝐴)
362	361	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 prefix 𝑗) ∈ Word 𝐴)
363		swrdcl 14608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ Word 𝐴 → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
364	363	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
365		ovexd 7402	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) ∈ V)
366	353, 360, 362, 364, 365	ovmpod 7519	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
367	331, 366	eqtr3id 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
368	367	mpteq2dva 5178	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))))
369	368	oveq2d 7383	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))))
370		eqid 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))
371		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑣 → (♯‘𝑡) = (♯‘𝑣))
372	371	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑣 → (0...(♯‘𝑡)) = (0...(♯‘𝑣)))
373		fvoveq1 7390	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑣 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑣 prefix 𝑗)))
374		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑣 → 𝑡 = 𝑣)
375	371	opeq2d 4823	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑣 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑣)⟩)
376	374, 375	oveq12d 7385	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑣 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))
377	376	fveq2d 6844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑣 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
378	373, 377	oveq12d 7385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑣 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
379	378	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 = 𝑣 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
380	372, 379	sumeq12dv 15668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑣 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
381		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐴)
382		fzfid 13935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (0...(♯‘𝑣)) ∈ Fin)
383	294	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑔:Word 𝐴⟶ℤ)
384	383, 362	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑔‘(𝑣 prefix 𝑗)) ∈ ℤ)
385	184	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑖:Word 𝐴⟶ℤ)
386	385, 364	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) ∈ ℤ)
387	384, 386	zmulcld 12639	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℤ)
388	387	zcnd 12634	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
389	382, 388	fsumcl 15695	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
390	370, 380, 381, 389	fvmptd3 6971	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
391	390	oveq1d 7382	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
392	111	ad3antrrr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑅 ∈ Grp)
393	45	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
394	315, 46	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐵)
395	394	sselda 3921	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐵)
396	49	gsumwcl 18807	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σg 𝑣) ∈ 𝐵)
397	393, 395, 396	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑀 Σg 𝑣) ∈ 𝐵)
398	2, 4, 392, 382, 397, 387	gsummulgc2 33127	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
399	391, 398	eqtr4d 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
400	330, 369, 399	3eqtr4rd 2782	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))
401	400	mpteq2dva 5178	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)))))
402	401	oveq2d 7383	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
403	316, 324, 402	3eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
404	176, 180, 403	3eqtr3d 2779	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
405		fveq1 6839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤))
406	405	oveq1d 7382	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))
407	406	mpteq2dv 5179	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))
408	407	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
409	408	cbvmptv 5189	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
410		fveq1 6839	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (ℎ‘𝑤) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
411	410	oveq1d 7382	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
412	411	mpteq2dv 5179	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤))))
413	412	oveq2d 7383	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))))
414	413	eqeq2d 2747	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → ((𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤))))))
415		breq1 5088	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑓 finSupp 0 ↔ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0))
416	78	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V)
417		fzfid 13935	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → (0...(♯‘𝑡)) ∈ Fin)
418	294	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑔:Word 𝐴⟶ℤ)
419		pfxcl 14640	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ Word 𝐴 → (𝑡 prefix 𝑗) ∈ Word 𝐴)
420	419	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 prefix 𝑗) ∈ Word 𝐴)
421	418, 420	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑔‘(𝑡 prefix 𝑗)) ∈ ℤ)
422	184	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑖:Word 𝐴⟶ℤ)
423		swrdcl 14608	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ Word 𝐴 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
424	423	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
425	422, 424	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) ∈ ℤ)
426	421, 425	zmulcld 12639	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
427	417, 426	fsumzcl 15697	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
428	427	fmpttd 7067	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))):Word 𝐴⟶ℤ)
429	416, 109, 428	elmapdd 8788	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ (ℤ ↑m Word 𝐴))
430		0zd 12536	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 ∈ ℤ)
431	428	ffund 6672	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Fun (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))))
432		ccatfn 14534	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ++ Fn (V × V)
433		fnfun 6598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( ++ Fn (V × V) → Fun ++ )
434	432, 433	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ Fun ++
435		imafi 9225	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Fun ++ ∧ ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin) → ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ∈ Fin)
436	434, 244, 435	sylancr 588	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ∈ Fin)
437		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑤 → (♯‘𝑡) = (♯‘𝑤))
438	437	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑤 → (0...(♯‘𝑡)) = (0...(♯‘𝑤)))
439		fvoveq1 7390	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑤 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑤 prefix 𝑗)))
440		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑤 → 𝑡 = 𝑤)
441	437	opeq2d 4823	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑤 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑤)⟩)
442	440, 441	oveq12d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑤 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))
443	442	fveq2d 6844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑤 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
444	439, 443	oveq12d 7385	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑤 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
445	444	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = 𝑤 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
446	438, 445	sumeq12dv 15668	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑤 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
447		oveq1 7374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑢 ++ 𝑣) = ((𝑤 prefix 𝑗) ++ 𝑣))
448	447	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑤 = (𝑢 ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣)))
449		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) → ((𝑤 prefix 𝑗) ++ 𝑣) = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
450	449	eqeq2d 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑣 = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) → (𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
451	246	ad4antr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑔 Fn Word 𝐴)
452	109	ad4antr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → Word 𝐴 ∈ V)
453		0zd 12536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 0 ∈ ℤ)
454		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))))
455	454	eldifad 3901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ Word 𝐴)
456	455	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑤 ∈ Word 𝐴)
457		pfxcl 14640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ Word 𝐴 → (𝑤 prefix 𝑗) ∈ Word 𝐴)
458	456, 457	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 prefix 𝑗) ∈ Word 𝐴)
459	458	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 prefix 𝑗) ∈ Word 𝐴)
460		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑔‘(𝑤 prefix 𝑗)) ≠ 0)
461	451, 452, 453, 459, 460	elsuppfnd 32755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 prefix 𝑗) ∈ (𝑔 supp 0))
462	275	ad4antr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑖 Fn Word 𝐴)
463		swrdcl 14608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ Word 𝐴 → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
464	456, 463	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
465	464	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
466		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)
467	462, 452, 453, 465, 466	elsuppfnd 32755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ (𝑖 supp 0))
468	456	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ Word 𝐴)
469		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑗 ∈ (0...(♯‘𝑤)))
470		pfxcctswrd 14672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑤 ∈ Word 𝐴 ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
471	468, 469, 470	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
472	471	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
473	448, 450, 461, 467, 472	2rspcedvdw 3578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))
474		fnov 7498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ( ++ Fn (V × V) ↔ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣)))
475	432, 474	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣))
476	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⊤ → 𝑤 ∈ V)
477		ssv 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 supp 0) ⊆ V
478	477	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⊤ → (𝑔 supp 0) ⊆ V)
479		ssv 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 supp 0) ⊆ V
480	479	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⊤ → (𝑖 supp 0) ⊆ V)
481	475, 476, 478, 480	elimampo 7504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⊤ → (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣)))
482	481	mptru 1549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))
483	473, 482	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
484	483	anasss 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
485	454	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))))
486	485	eldifbd 3902	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
487	486	anasss 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
488	484, 487	pm2.65da 817	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0))
489		df-ne 2933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ↔ ¬ (𝑔‘(𝑤 prefix 𝑗)) = 0)
490		df-ne 2933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0 ↔ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0)
491	489, 490	anbi12i 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) ↔ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
492	491	notbii 320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) ↔ ¬ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
493		pm4.57 993	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0) ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
494	492, 493	bitr2i 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0) ↔ ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0))
495	488, 494	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
496	294	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑔:Word 𝐴⟶ℤ)
497	496, 458	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℤ)
498	497	zcnd 12634	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℂ)
499	184	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑖:Word 𝐴⟶ℤ)
500	499, 464	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℤ)
501	500	zcnd 12634	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℂ)
502	498, 501	mul0ord 11798	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0 ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0)))
503	495, 502	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0)
504	503	sumeq2dv 15664	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))0)
505		fzssuz 13519	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0...(♯‘𝑤)) ⊆ (ℤ≥‘0)
506		sumz 15684	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((0...(♯‘𝑤)) ⊆ (ℤ≥‘0) ∨ (0...(♯‘𝑤)) ∈ Fin) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
507	506	orcs 876	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((0...(♯‘𝑤)) ⊆ (ℤ≥‘0) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
508	505, 507	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
509	504, 508	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0)
510	446, 509	sylan9eqr 2793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑡 = 𝑤) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = 0)
511		0zd 12536	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 0 ∈ ℤ)
512	370, 510, 455, 511	fvmptd2 6956	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) = 0)
513	428, 512	suppss 8144	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ⊆ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
514	436, 513	ssfid 9179	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ∈ Fin)
515	429, 430, 431, 514	isfsuppd 9279	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0)
516	415, 429, 515	elrabd 3636	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
517	516, 6	eleqtrrdi 2847	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ 𝐹)
518		fveq2 6840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
519	518, 145	oveq12d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑤 → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
520	519	cbvmptv 5189	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
521	520	oveq2i 7378	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤))))
522	521	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))))
523	414, 517, 522	rspcedvdw 3567	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
524		ovexd 7402	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ V)
525	409, 523, 524	elrnmptd 5918	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
526	525, 8	eleqtrrdi 2847	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ 𝑆)
527	404, 526	eqeltrd 2836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
528	527	adantllr 720	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
529	528	adantllr 720	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
530	529	adantlr 716	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
531	530	adantr 480	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
532	107, 531	eqeltrd 2836	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
533	8	eleq2i 2828	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
534	169	oveq2d 7383	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
535	534	cbvmptv 5189	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
536	535	elrnmpt 5913	. . . . . . . . . 10 ⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
537	536	elv 3434	. . . . . . . . 9 ⊢ (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
538	533, 537	sylbb 219	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑆 → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
539	538	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
540	539	ad2antrr 727	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
541	532, 540	r19.29a 3145	. . . . 5 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
542	8	eleq2i 2828	. . . . . . 7 ⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
543	71	elrnmpt 5913	. . . . . . . 8 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
544	543	elv 3434	. . . . . . 7 ⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
545	542, 544	sylbb 219	. . . . . 6 ⊢ (𝑥 ∈ 𝑆 → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
546	545	ad2antlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
547	541, 546	r19.29a 3145	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
548	547	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
549	548	ralrimivva 3180	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
550	2, 24, 108	issubrg2 20569	. . 3 ⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)))
551	550	biimpar 477	. 2 ⊢ ((𝑅 ∈ Ring ∧ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)) → 𝑆 ∈ (SubRing‘𝑅))
552	1, 9, 104, 549, 551	syl13anc 1375	1 ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  {crab 3389  Vcvv 3429   ∖ cdif 3886   ∪ cun 3887   ⊆ wss 3889  ∅c0 4273  ifcif 4466  {csn 4567  ⟨cop 4573   class class class wbr 5085   ↦ cmpt 5166   × cxp 5629  ran crn 5632   “ cima 5634  Fun wfun 6492   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369  1^st c1st 7940  2^nd c2nd 7941   supp csupp 8110   ↑_m cmap 8773  Fincfn 8893   finSupp cfsupp 9274  ℂcc 11036  0cc0 11038  1c1 11039   · cmul 11043  ℤcz 12524  ℤ_≥cuz 12788  ...cfz 13461  ♯chash 14292  Word cword 14475   ++ cconcat 14532   substr csubstr 14603   prefix cpfx 14633  Σcsu 15648  Basecbs 17179  ._rcmulr 17221  0_gc0g 17402   Σ_g cgsu 17403  Mndcmnd 18702  Grpcgrp 18909  ._gcmg 19043  SubGrpcsubg 19096  CMndccmn 19755  mulGrpcmgp 20121  1_rcur 20162  Ringcrg 20214  SubRingcsubrg 20546  RingSpancrgspn 20587

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 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-inf2 9562  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-iin 4936  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  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 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-tpos 8176  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-er 8643  df-map 8775  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-sup 9355  df-oi 9425  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-z 12525  df-dec 12645  df-uz 12789  df-rp 12943  df-fz 13462  df-fzo 13609  df-seq 13964  df-exp 14024  df-hash 14293  df-word 14476  df-concat 14533  df-substr 14604  df-pfx 14634  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-clim 15450  df-sum 15649  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-starv 17235  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-0g 17404  df-gsum 17405  df-mre 17548  df-mrc 17549  df-acs 17551  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-mhm 18751  df-submnd 18752  df-grp 18912  df-minusg 18913  df-mulg 19044  df-subg 19099  df-ghm 19188  df-cntz 19292  df-cmn 19757  df-abl 19758  df-mgp 20122  df-rng 20134  df-ur 20163  df-ring 20216  df-cring 20217  df-oppr 20317  df-subrng 20523  df-subrg 20547  df-cnfld 21353  df-zring 21427

This theorem is referenced by:  elrgspnlem4  33306