Theorem elrgspnlem2 33506

Description: Lemma for elrgspn 33509. (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 33505	. 2 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))
10		eqeq2 2781	. . . . . . 7 ⊢ ((1r‘𝑅) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))
11		eqeq2 2781	. . . . . . 7 ⊢ ((0g‘𝑅) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))
12		simpr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → 𝑤 = ∅)
13	12	fveq2d 6888	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅))
14		eqid 2769	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))
15		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 = ∅) → 𝑣 = ∅)
16	15	iftrued 4500	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 = ∅) → if(𝑣 = ∅, 1, 0) = 1)
17		wrd0 14578	. . . . . . . . . . . . 13 ⊢ ∅ ∈ Word 𝐴
18	17	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ∈ Word 𝐴)
19		1zzd 12627	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
20	14, 16, 18, 19	fvmptd2 7001	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
21	20	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
22	13, 21	eqtrd 2804	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 1)
23	12	oveq2d 7429	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (𝑀 Σg ∅))
24		eqid 2769	. . . . . . . . . . . 12 ⊢ (1r‘𝑅) = (1r‘𝑅)
25	3, 24	ringidval 20267	. . . . . . . . . . 11 ⊢ (1r‘𝑅) = (0g‘𝑀)
26	25	gsum0 18744	. . . . . . . . . 10 ⊢ (𝑀 Σg ∅) = (1r‘𝑅)
27	23, 26	eqtrdi 2820	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (1r‘𝑅))
28	22, 27	oveq12d 7431	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1 · (1r‘𝑅)))
29	2, 24	ringidcl 20350	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐵)
30	1, 29	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵)
31	2, 4	mulg1 19149	. . . . . . . . . 10 ⊢ ((1r‘𝑅) ∈ 𝐵 → (1 · (1r‘𝑅)) = (1r‘𝑅))
32	30, 31	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (1 · (1r‘𝑅)) = (1r‘𝑅))
33	32	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (1 · (1r‘𝑅)) = (1r‘𝑅))
34	28, 33	eqtrd 2804	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅))
35		eqeq1 2773	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑤 → (𝑣 = ∅ ↔ 𝑤 = ∅))
36	35	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑤 → (¬ 𝑣 = ∅ ↔ ¬ 𝑤 = ∅))
37	36	biimparc 484	. . . . . . . . . . . 12 ⊢ ((¬ 𝑤 = ∅ ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
38	37	adantll 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
39	38	iffalsed 4503	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → if(𝑣 = ∅, 1, 0) = 0)
40		simplr 780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 𝑤 ∈ Word 𝐴)
41		0zd 12605	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 0 ∈ ℤ)
42	14, 39, 40, 41	fvmptd2 7001	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 0)
43	42	oveq1d 7428	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
44	3	ringmgp 20323	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
45	1, 44	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ Mnd)
46		sswrd 14561	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
47	7, 46	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
48	47	sselda 3945	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
49	3, 2	mgpbas 20223	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑀)
50	49	gsumwcl 18900	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
51	45, 48, 50	syl2an2r 697	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
52		eqid 2769	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
53	2, 52, 4	mulg0 19142	. . . . . . . . . 10 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
54	51, 53	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
55	54	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
56	43, 55	eqtrd 2804	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
57	10, 11, 34, 56	ifbothda 4531	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))
58	57	mpteq2dva 5208	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))
59	58	oveq2d 7429	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))))
60	1	ringcmnd 20369	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
61	60	cmnmndd 19876	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Mnd)
62	2	fvexi 6898	. . . . . . . 8 ⊢ 𝐵 ∈ V
63	62	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
64	63, 7	ssexd 5297	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ V)
65		wrdexg 14563	. . . . . 6 ⊢ (𝐴 ∈ V → Word 𝐴 ∈ V)
66	64, 65	syl 18	. . . . 5 ⊢ (𝜑 → Word 𝐴 ∈ V)
67		eqid 2769	. . . . 5 ⊢ (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))
68	30, 2	eleqtrdi 2879	. . . . 5 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
69	52, 61, 66, 18, 67, 68	gsummptif1n0 20038	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) = (1r‘𝑅))
70	59, 69	eqtrd 2804	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (1r‘𝑅))
71		eqid 2769	. . . . 5 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
72		fveq1 6883	. . . . . . . . . 10 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤))
73	72	oveq1d 7428	. . . . . . . . 9 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))
74	73	mpteq2dv 5209	. . . . . . . 8 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))
75	74	oveq2d 7429	. . . . . . 7 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
76	75	eqeq2d 2780	. . . . . 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 5116	. . . . . . . 8 ⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0))
78		zex 12602	. . . . . . . . . 10 ⊢ ℤ ∈ V
79	78	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℤ ∈ V)
80		1zzd 12627	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑣 = ∅) → 1 ∈ ℤ)
81		0zd 12605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ ¬ 𝑣 = ∅) → 0 ∈ ℤ)
82	80, 81	ifclda 4528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ Word 𝐴) → if(𝑣 = ∅, 1, 0) ∈ ℤ)
83	82	fmpttd 7113	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)):Word 𝐴⟶ℤ)
84	79, 66, 83	elmapdd 8840	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ (ℤ ↑m Word 𝐴))
85	66	mptexd 7225	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V)
86	83	ffund 6713	. . . . . . . . 9 ⊢ (𝜑 → Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)))
87		0zd 12605	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
88		snfi 9042	. . . . . . . . . 10 ⊢ {∅} ∈ Fin
89	88	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {∅} ∈ Fin)
90		eldifsni 4762	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (Word 𝐴 ∖ {∅}) → 𝑣 ≠ ∅)
91	90	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → 𝑣 ≠ ∅)
92	91	neneqd 2969	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → ¬ 𝑣 = ∅)
93	92	iffalsed 4503	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → if(𝑣 = ∅, 1, 0) = 0)
94	93, 66	suppss2 8198	. . . . . . . . 9 ⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆ {∅})
95		suppssfifsupp 9342	. . . . . . . . 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 1403	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0)
97	77, 84, 96	elrabd 3661	. . . . . . 7 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
98	97, 6	eleqtrrdi 2880	. . . . . 6 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ 𝐹)
99		eqidd 2770	. . . . . 6 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
100	76, 98, 99	rspcedvdw 3593	. . . . 5 ⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
101		ovexd 7448	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V)
102	71, 100, 101	elrnmptd 5956	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
103	102, 8	eleqtrrdi 2880	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
104	70, 103	eqeltrrd 2870	. 2 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆)
105		simpllr 787	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
106		simpr 489	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
107	105, 106	oveq12d 7431	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
108		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (.r‘𝑅) = (.r‘𝑅)
109	66	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ∈ V)
110	1	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ Ring)
111	1	ringgrpd 20326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 ∈ Grp)
112	111	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
113	6	ssrab3 4044	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 ⊆ (ℤ ↑m Word 𝐴)
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word 𝐴))
115	114	sselda 3945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word 𝐴))
116	79, 66	elmapd 8839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
117	116	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
118	115, 117	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
119	118	ffvelcdmda 7082	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
120	51	adantlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
121	2, 4, 112, 119, 120	mulgcld 19164	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
122	121	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
123	122	ralrimiva 3163	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
124		fveq2 6884	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑤 → (𝑔‘𝑢) = (𝑔‘𝑤))
125		oveq2 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑤 → (𝑀 Σg 𝑢) = (𝑀 Σg 𝑤))
126	124, 125	oveq12d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑤 → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
127	126	eleq1d 2854	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
128	127	cbvralvw 3249	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑢 ∈ Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
129	123, 128	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑢 ∈ Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
130	129	r19.21bi 3263	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑢 ∈ Word 𝐴) → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
131	111	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
132		breq1 5116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0))
133	132, 6	elrab2 3663	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑖 finSupp 0))
134	133	simplbi 501	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word 𝐴))
135	134	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word 𝐴))
136	79, 66	elmapd 8839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
137	136	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
138	135, 137	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
139	138	ffvelcdmda 7082	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ)
140	51	adantlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
141	2, 4, 131, 139, 140	mulgcld 19164	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
142	141	adantllr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
143	142	ralrimiva 3163	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
144		fveq2 6884	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑖‘𝑣) = (𝑖‘𝑤))
145		oveq2 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑤))
146	144, 145	oveq12d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑤 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
147	146	eleq1d 2854	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑤 → (((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
148	147	cbvralvw 3249	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑣 ∈ Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
149	143, 148	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑣 ∈ Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
150	149	r19.21bi 3263	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
151	126	cbvmptv 5219	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
152		fvexd 6899	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V)
153		0zd 12605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ)
154	66	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ∈ V)
155		ssidd 3968	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴)
156		breq1 5116	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
157	156, 6	elrab2 3663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
158	157	simprbi 502	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
159	158	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
160	2, 52, 4	mulg0 19142	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅))
161	160	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅))
162	152, 153, 154, 155, 120, 118, 159, 161	fisuppov1 32971	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
163	162	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
164	151, 163	eqbrtrid 5150	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) finSupp (0g‘𝑅))
165	146	cbvmptv 5219	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
166	162	ralrimiva 3163	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
167		fveq1 6883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤))
168	167	oveq1d 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
169	168	mpteq2dv 5209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
170	169	breq1d 5123	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅)))
171	170	cbvralvw 3249	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
172	166, 171	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
173	172	r19.21bi 3263	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
174	173	adantlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
175	165, 174	eqbrtrid 5150	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) finSupp (0g‘𝑅))
176	2, 108, 52, 109, 109, 110, 130, 150, 164, 175	gsumdixp 20402	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))))(.r‘𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))))
177	151	oveq2i 7424	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
178	165	oveq2i 7424	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
179	177, 178	oveq12i 7425	. . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Ring)
182	122	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
183	111	ad4antr 744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Grp)
184	138	adantlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
185	184	ffvelcdmda 7082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑓 ∈ Word 𝐴) → (𝑖‘𝑓) ∈ ℤ)
186	185	adantlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑖‘𝑓) ∈ ℤ)
187	45	ad4antr 744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
188	47	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐵)
189	188	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵)
190	189	sselda 3945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑓 ∈ Word 𝐵)
191	49	gsumwcl 18900	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg 𝑓) ∈ 𝐵)
192	187, 190, 191	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑓) ∈ 𝐵)
193	2, 4, 183, 186, 192	mulgcld 19164	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)
194	2, 108, 181, 182, 193	ringcld 20344	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
195	194	anasss 471	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
196	195	ralrimivva 3214	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴∀𝑓 ∈ Word 𝐴(((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
197		eqid 2769	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
198	197	fmpo 8067	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ Word 𝐴∀𝑓 ∈ Word 𝐴(((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵 ↔ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵)
199	196, 198	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵)
200		vex 3467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑤 ∈ V
201		vex 3467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑓 ∈ V
202	200, 201	op1std 7998	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (1st ‘𝑎) = 𝑤)
203	202	fveq2d 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑔‘(1st ‘𝑎)) = (𝑔‘𝑤))
204	202	oveq2d 7429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (1st ‘𝑎)) = (𝑀 Σg 𝑤))
205	203, 204	oveq12d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
206	200, 201	op2ndd 7999	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (2nd ‘𝑎) = 𝑓)
207	206	fveq2d 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑖‘(2nd ‘𝑎)) = (𝑖‘𝑓))
208	206	oveq2d 7429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (2nd ‘𝑎)) = (𝑀 Σg 𝑓))
209	207, 208	oveq12d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓)))
210	205, 209	oveq12d 7431	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
211	210	mpompt 7527	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
212	66, 66	xpexd 7752	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Word 𝐴 × Word 𝐴) ∈ V)
213	212	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (Word 𝐴 × Word 𝐴) ∈ V)
214	213	mptexd 7225	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) ∈ V)
215		fvexd 6899	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (0g‘𝑅) ∈ V)
216	110	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Ring)
217	111	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Grp)
218	118	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ)
219		xp1st 8020	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1st ‘𝑎) ∈ Word 𝐴)
220	219	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴)
221	218, 220	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑔‘(1st ‘𝑎)) ∈ ℤ)
222	216, 44	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑀 ∈ Mnd)
223	188	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵)
224	223, 220	sseldd 3946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐵)
225	49	gsumwcl 18900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ (1st ‘𝑎) ∈ Word 𝐵) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
226	222, 224, 225	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
227	2, 4, 217, 221, 226	mulgcld 19164	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) ∈ 𝐵)
228	184	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ)
229		xp2nd 8021	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴)
230	229	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴)
231	228, 230	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈ ℤ)
232	223, 230	sseldd 3946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐵)
233	49	gsumwcl 18900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ (2nd ‘𝑎) ∈ Word 𝐵) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
234	222, 232, 233	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
235	2, 4, 217, 231, 234	mulgcld 19164	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) ∈ 𝐵)
236	2, 108, 216, 227, 235	ringcld 20344	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) ∈ 𝐵)
237	236	fmpttd 7113	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))):(Word 𝐴 × Word 𝐴)⟶𝐵)
238	237	ffund 6713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Fun (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))))
239	159	fsuppimpd 9331	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin)
240	133	simprbi 502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0)
241	240	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0)
242	241	fsuppimpd 9331	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑖 supp 0) ∈ Fin)
243		xpfi 9281	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 supp 0) ∈ Fin ∧ (𝑖 supp 0) ∈ Fin) → ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin)
244	239, 242, 243	syl2an2r 697	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin)
245	118	ffnd 6709	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
246	245	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
247	246	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑔 Fn Word 𝐴)
248	109	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ∈ V)
249		0zd 12605	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 0 ∈ ℤ)
250		xp1st 8020	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (1st ‘𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
251	250	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
252	247, 248, 249, 251	fvdifsupp 8169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑔‘(1st ‘𝑎)) = 0)
253	252	oveq1d 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) = (0 · (𝑀 Σg (1st ‘𝑎))))
254	45	ad4antr 744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑀 ∈ Mnd)
255	188	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵)
256	251	eldifad 3925	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴)
257	255, 256	sseldd 3946	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐵)
258	254, 257, 225	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
259	2, 52, 4	mulg0 19142	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 Σg (1st ‘𝑎)) ∈ 𝐵 → (0 · (𝑀 Σg (1st ‘𝑎))) = (0g‘𝑅))
260	258, 259	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (0 · (𝑀 Σg (1st ‘𝑎))) = (0g‘𝑅))
261	253, 260	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) = (0g‘𝑅))
262	261	oveq1d 7428	. . . . . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Ring)
264	111	ad4antr 744	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Grp)
265	184	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ)
266		xp2nd 8021	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴)
267	266	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴)
268	265, 267	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈ ℤ)
269	255, 267	sseldd 3946	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐵)
270	254, 269, 233	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
271	2, 4, 264, 268, 270	mulgcld 19164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) ∈ 𝐵)
272	2, 108, 52, 263, 271	ringlzd 20380	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((0g‘𝑅)(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
273	262, 272	eqtrd 2804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
274	138	ffnd 6709	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
275	274	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
276	275	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑖 Fn Word 𝐴)
277	109	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ∈ V)
278		0zd 12605	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 0 ∈ ℤ)
279		xp2nd 8021	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (2nd ‘𝑎) ∈ (Word 𝐴 ∖ (𝑖 supp 0)))
280	279	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd ‘𝑎) ∈ (Word 𝐴 ∖ (𝑖 supp 0)))
281	276, 277, 278, 280	fvdifsupp 8169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑖‘(2nd ‘𝑎)) = 0)
282	281	oveq1d 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) = (0 · (𝑀 Σg (2nd ‘𝑎))))
283	45	ad4antr 744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑀 ∈ Mnd)
284	188	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ⊆ Word 𝐵)
285	280	eldifad 3925	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd ‘𝑎) ∈ Word 𝐴)
286	284, 285	sseldd 3946	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd ‘𝑎) ∈ Word 𝐵)
287	283, 286, 233	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
288	2, 52, 4	mulg0 19142	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵 → (0 · (𝑀 Σg (2nd ‘𝑎))) = (0g‘𝑅))
289	287, 288	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (0 · (𝑀 Σg (2nd ‘𝑎))) = (0g‘𝑅))
290	282, 289	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) = (0g‘𝑅))
291	290	oveq2d 7429	. . . . . . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Ring)
293	111	ad4antr 744	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Grp)
294	118	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
295	294	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑔:Word 𝐴⟶ℤ)
296		xp1st 8020	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (1st ‘𝑎) ∈ Word 𝐴)
297	296	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st ‘𝑎) ∈ Word 𝐴)
298	295, 297	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑔‘(1st ‘𝑎)) ∈ ℤ)
299	284, 297	sseldd 3946	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st ‘𝑎) ∈ Word 𝐵)
300	283, 299, 225	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
301	2, 4, 293, 298, 300	mulgcld 19164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) ∈ 𝐵)
302	2, 108, 52, 292, 301	ringrzd 20381	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
303	291, 302	eqtrd 2804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
304		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))))
305		difxp 6164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))) = (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))))
306	304, 305	eleqtrdi 2879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
307		elun 4115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) ↔ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
308	306, 307	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
309	273, 303, 308	mpjaodan 973	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
310	309, 213	suppss2 8198	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) supp (0g‘𝑅)) ⊆ ((𝑔 supp 0) × (𝑖 supp 0)))
311	244, 310	ssfid 9231	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) supp (0g‘𝑅)) ∈ Fin)
312	214, 215, 238, 311	isfsuppd 9328	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) finSupp (0g‘𝑅))
313	211, 312	eqbrtrrid 5151	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) finSupp (0g‘𝑅))
314	60	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ CMnd)
315	7	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝐴 ⊆ 𝐵)
316	2, 52, 199, 313, 314, 315	gsumwrd2dccat 33341	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
317	126	oveq1d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))
318		fveq2 6884	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑓 → (𝑖‘𝑣) = (𝑖‘𝑓))
319		oveq2 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑓 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑓))
320	318, 319	oveq12d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑓 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓)))
321	320	oveq2d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑓 → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
322	317, 321	cbvmpov 7508	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
323	322	oveq2i 7424	. . . . . . . . . . . . . . 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 14749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ Word 𝐴 ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
326	325	adantll 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
327	326	oveq2d 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) = (𝑀 Σg 𝑣))
328	327	oveq2d 7429	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
329	328	mpteq2dva 5208	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣))))
330	329	oveq2d 7429	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
331		df-ov 7416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)
332	188	sselda 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
333	332	ad4ant13 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
334	187, 333, 50	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
335	2, 4, 108	mulgass3 20437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ Ring ∧ ((𝑖‘𝑓) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ (𝑀 Σg 𝑓) ∈ 𝐵)) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
336	181, 186, 334, 192, 335	syl13anc 1397	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
337	336	oveq2d 7429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))))
338	119	ad4ant13 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
339	2, 4, 108	mulgass2 20394	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ Ring ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))))
340	181, 338, 334, 193, 339	syl13anc 1397	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))))
341	2, 108, 181, 334, 192	ringcld 20344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)
342	2, 4	mulgass 19179	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑓) ∈ ℤ ∧ ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))))
343	183, 338, 186, 341, 342	syl13anc 1397	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))))
344	337, 340, 343	3eqtr4d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
345	3, 108	mgpplusg 20222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (.r‘𝑅) = (+g‘𝑀)
346	49, 345	gsumccat 18902	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))
347	187, 333, 190, 346	syl3anc 1396	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))
348	347	oveq2d 7429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
349	344, 348	eqtr4d 2807	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
350	349	adantllr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
351	350	adantllr 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
352	351	3impa 1125	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
353	352	mpoeq3dva 7490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓)))))
354		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑣 prefix 𝑗) → (𝑔‘𝑤) = (𝑔‘(𝑣 prefix 𝑗)))
355		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) → (𝑖‘𝑓) = (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
356	354, 355	oveqan12d 7432	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → ((𝑔‘𝑤) · (𝑖‘𝑓)) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
357		oveq12 7422	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑤 ++ 𝑓) = ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
358	357	oveq2d 7429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑀 Σg (𝑤 ++ 𝑓)) = (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
359	356, 358	oveq12d 7431	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
360	359	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ (𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
361		pfxcl 14717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ Word 𝐴 → (𝑣 prefix 𝑗) ∈ Word 𝐴)
362	361	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 prefix 𝑗) ∈ Word 𝐴)
363		swrdcl 14685	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ Word 𝐴 → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
364	363	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
365		ovexd 7448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) ∈ V)
366	353, 360, 362, 364, 365	ovmpod 7565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
367	331, 366	eqtr3id 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
368	367	mpteq2dva 5208	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))))
369	368	oveq2d 7429	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))))
370		eqid 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))
371		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑣 → (♯‘𝑡) = (♯‘𝑣))
372	371	oveq2d 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑣 → (0...(♯‘𝑡)) = (0...(♯‘𝑣)))
373		fvoveq1 7436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑣 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑣 prefix 𝑗)))
374		id 23	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑣 → 𝑡 = 𝑣)
375	371	opeq2d 4849	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑣 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑣)⟩)
376	374, 375	oveq12d 7431	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑣 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))
377	376	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑣 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
378	373, 377	oveq12d 7431	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑣 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
379	378	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 = 𝑣 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
380	372, 379	sumeq12dv 15759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑣 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
381		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐴)
382		fzfid 14011	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (0...(♯‘𝑣)) ∈ Fin)
383	294	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑔:Word 𝐴⟶ℤ)
384	383, 362	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑔‘(𝑣 prefix 𝑗)) ∈ ℤ)
385	184	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑖:Word 𝐴⟶ℤ)
386	385, 364	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) ∈ ℤ)
387	384, 386	zmulcld 12708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℤ)
388	387	zcnd 12703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
389	382, 388	fsumcl 15786	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
390	370, 380, 381, 389	fvmptd3 7016	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
391	390	oveq1d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
392	111	ad3antrrr 742	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑅 ∈ Grp)
393	45	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
394	315, 46	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐵)
395	394	sselda 3945	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐵)
396	49	gsumwcl 18900	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σg 𝑣) ∈ 𝐵)
397	393, 395, 396	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑀 Σg 𝑣) ∈ 𝐵)
398	2, 4, 392, 382, 397, 387	gsummulgc2 33329	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
399	391, 398	eqtr4d 2807	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
400	330, 369, 399	3eqtr4rd 2815	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))
401	400	mpteq2dva 5208	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)))))
402	401	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
403	316, 324, 402	3eqtr4d 2814	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
404	176, 180, 403	3eqtr3d 2812	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
405		fveq1 6883	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤))
406	405	oveq1d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))
407	406	mpteq2dv 5209	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))
408	407	oveq2d 7429	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
409	408	cbvmptv 5219	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
410		fveq1 6883	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (ℎ‘𝑤) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
411	410	oveq1d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
412	411	mpteq2dv 5209	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤))))
413	412	oveq2d 7429	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))))
414	413	eqeq2d 2780	. . . . . . . . . . . . . . 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 5116	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑓 finSupp 0 ↔ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0))
416	78	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V)
417		fzfid 14011	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → (0...(♯‘𝑡)) ∈ Fin)
418	294	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑔:Word 𝐴⟶ℤ)
419		pfxcl 14717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ Word 𝐴 → (𝑡 prefix 𝑗) ∈ Word 𝐴)
420	419	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 prefix 𝑗) ∈ Word 𝐴)
421	418, 420	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑔‘(𝑡 prefix 𝑗)) ∈ ℤ)
422	184	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑖:Word 𝐴⟶ℤ)
423		swrdcl 14685	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ Word 𝐴 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
424	423	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
425	422, 424	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) ∈ ℤ)
426	421, 425	zmulcld 12708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
427	417, 426	fsumzcl 15788	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
428	427	fmpttd 7113	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))):Word 𝐴⟶ℤ)
429	416, 109, 428	elmapdd 8840	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ (ℤ ↑m Word 𝐴))
430		0zd 12605	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 ∈ ℤ)
431	428	ffund 6713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Fun (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))))
432		ccatfn 14611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ++ Fn (V × V)
433		fnfun 6638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( ++ Fn (V × V) → Fun ++ )
434	432, 433	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ Fun ++
435		imafi 9277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Fun ++ ∧ ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin) → ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ∈ Fin)
436	434, 244, 435	sylancr 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ∈ Fin)
437		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑤 → (♯‘𝑡) = (♯‘𝑤))
438	437	oveq2d 7429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑤 → (0...(♯‘𝑡)) = (0...(♯‘𝑤)))
439		fvoveq1 7436	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑤 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑤 prefix 𝑗)))
440		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑤 → 𝑡 = 𝑤)
441	437	opeq2d 4849	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑤 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑤)⟩)
442	440, 441	oveq12d 7431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑤 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))
443	442	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑤 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
444	439, 443	oveq12d 7431	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑤 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
445	444	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = 𝑤 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
446	438, 445	sumeq12dv 15759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑤 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
447		oveq1 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑢 ++ 𝑣) = ((𝑤 prefix 𝑗) ++ 𝑣))
448	447	eqeq2d 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑤 = (𝑢 ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣)))
449		oveq2 7421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) → ((𝑤 prefix 𝑗) ++ 𝑣) = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
450	449	eqeq2d 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑣 = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) → (𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
451	246	ad4antr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑔 Fn Word 𝐴)
452	109	ad4antr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → Word 𝐴 ∈ V)
453		0zd 12605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 0 ∈ ℤ)
454		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))))
455	454	eldifad 3925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ Word 𝐴)
456	455	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑤 ∈ Word 𝐴)
457		pfxcl 14717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ Word 𝐴 → (𝑤 prefix 𝑗) ∈ Word 𝐴)
458	456, 457	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 prefix 𝑗) ∈ Word 𝐴)
459	458	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 prefix 𝑗) ∈ Word 𝐴)
460		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑔‘(𝑤 prefix 𝑗)) ≠ 0)
461	451, 452, 453, 459, 460	elsuppfnd 32970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 prefix 𝑗) ∈ (𝑔 supp 0))
462	275	ad4antr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑖 Fn Word 𝐴)
463		swrdcl 14685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ Word 𝐴 → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
464	456, 463	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
465	464	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
466		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)
467	462, 452, 453, 465, 466	elsuppfnd 32970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ (𝑖 supp 0))
468	456	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ Word 𝐴)
469		simpllr 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑗 ∈ (0...(♯‘𝑤)))
470		pfxcctswrd 14749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑤 ∈ Word 𝐴 ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
471	468, 469, 470	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
472	471	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
473	448, 450, 461, 467, 472	2rspcedvdw 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))
474		fnov 7544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ( ++ Fn (V × V) ↔ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣)))
475	432, 474	mpbi 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣))
476	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⊤ → 𝑤 ∈ V)
477		ssv 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 supp 0) ⊆ V
478	477	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⊤ → (𝑔 supp 0) ⊆ V)
479		ssv 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 supp 0) ⊆ V
480	479	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⊤ → (𝑖 supp 0) ⊆ V)
481	475, 476, 478, 480	elimampo 7550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⊤ → (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣)))
482	481	mptru 1574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))
483	473, 482	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
484	483	anasss 471	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
485	454	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))))
486	485	eldifbd 3926	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
487	486	anasss 471	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
488	484, 487	pm2.65da 828	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0))
489		df-ne 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ↔ ¬ (𝑔‘(𝑤 prefix 𝑗)) = 0)
490		df-ne 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0 ↔ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0)
491	489, 490	anbi12i 639	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) ↔ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
492	491	notbii 323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) ↔ ¬ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
493		pm4.57 1006	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0) ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
494	492, 493	bitr2i 279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0) ↔ ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0))
495	488, 494	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
496	294	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑔:Word 𝐴⟶ℤ)
497	496, 458	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℤ)
498	497	zcnd 12703	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℂ)
499	184	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑖:Word 𝐴⟶ℤ)
500	499, 464	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℤ)
501	500	zcnd 12703	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℂ)
502	498, 501	mul0ord 11864	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0 ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0)))
503	495, 502	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0)
504	503	sumeq2dv 15755	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))0)
505		fzssuz 13595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0...(♯‘𝑤)) ⊆ (ℤ≥‘0)
506		sumz 15775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((0...(♯‘𝑤)) ⊆ (ℤ≥‘0) ∨ (0...(♯‘𝑤)) ∈ Fin) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
507	506	orcs 888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((0...(♯‘𝑤)) ⊆ (ℤ≥‘0) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
508	505, 507	mp1i 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
509	504, 508	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0)
510	446, 509	sylan9eqr 2826	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑡 = 𝑤) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = 0)
511		0zd 12605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 0 ∈ ℤ)
512	370, 510, 455, 511	fvmptd2 7001	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) = 0)
513	428, 512	suppss 8192	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ⊆ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
514	436, 513	ssfid 9231	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ∈ Fin)
515	429, 430, 431, 514	isfsuppd 9328	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0)
516	415, 429, 515	elrabd 3661	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
517	516, 6	eleqtrrdi 2880	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ 𝐹)
518		fveq2 6884	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
519	518, 145	oveq12d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑤 → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
520	519	cbvmptv 5219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
521	520	oveq2i 7424	. . . . . . . . . . . . . . . 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 3593	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
524		ovexd 7448	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ V)
525	409, 523, 524	elrnmptd 5956	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
526	525, 8	eleqtrrdi 2880	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ 𝑆)
527	404, 526	eqeltrd 2869	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
528	527	adantllr 731	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
529	528	adantllr 731	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
530	529	adantlr 727	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
531	530	adantr 485	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
532	107, 531	eqeltrd 2869	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
533	8	eleq2i 2861	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
534	169	oveq2d 7429	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
535	534	cbvmptv 5219	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
536	535	elrnmpt 5951	. . . . . . . . . 10 ⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
537	536	elv 3468	. . . . . . . . 9 ⊢ (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
538	533, 537	sylbb 222	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑆 → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
539	538	adantl 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
540	539	ad2antrr 738	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
541	532, 540	r19.29a 3179	. . . . 5 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
542	8	eleq2i 2861	. . . . . . 7 ⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
543	71	elrnmpt 5951	. . . . . . . 8 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
544	543	elv 3468	. . . . . . 7 ⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
545	542, 544	sylbb 222	. . . . . 6 ⊢ (𝑥 ∈ 𝑆 → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
546	545	ad2antlr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
547	541, 546	r19.29a 3179	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
548	547	anasss 471	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
549	548	ralrimivva 3214	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
550	2, 24, 108	issubrg2 20679	. . 3 ⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)))
551	550	biimpar 482	. 2 ⊢ ((𝑅 ∈ Ring ∧ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)) → 𝑆 ∈ (SubRing‘𝑅))
552	1, 9, 104, 549, 551	syl13anc 1397	1 ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1567  ⊤wtru 1568   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095  {crab 3423  Vcvv 3463   ∖ cdif 3910   ∪ cun 3911   ⊆ wss 3913  ∅c0 4294  ifcif 4492  {csn 4594  ⟨cop 4600   class class class wbr 5113   ↦ cmpt 5196   × cxp 5662  ran crn 5665   “ cima 5667  Fun wfun 6533   Fn wfn 6534  ⟶wf 6535  ‘cfv 6539  (class class class)co 7413   ∈ cmpo 7415  1^st c1st 7986  2^nd c2nd 7987   supp csupp 8158   ↑_m cmap 8826  Fincfn 8945   finSupp cfsupp 9323  ℂcc 11100  0cc0 11102  1c1 11103   · cmul 11107  ℤcz 12593  ℤ_≥cuz 12864  ...cfz 13537  ♯chash 14368  Word cword 14552   ++ cconcat 14609   substr csubstr 14680   prefix cpfx 14710  Σcsu 15739  Basecbs 17271  ._rcmulr 17313  0_gc0g 17494   Σ_g cgsu 17495  Mndcmnd 18794  Grpcgrp 19002  ._gcmg 19135  SubGrpcsubg 19188  CMndccmn 19852  mulGrpcmgp 20218  1_rcur 20265  Ringcrg 20317  SubRingcsubrg 20656  RingSpancrgspn 20697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5273  ax-pow 5339  ax-pr 5407  ax-un 7735  ax-inf2 9612  ax-cnex 11158  ax-resscn 11159  ax-1cn 11160  ax-icn 11161  ax-addcl 11162  ax-addrcl 11163  ax-mulcl 11164  ax-mulrcl 11165  ax-mulcom 11166  ax-addass 11167  ax-mulass 11168  ax-distr 11169  ax-i2m1 11170  ax-1ne0 11171  ax-1rid 11172  ax-rnegex 11173  ax-rrecex 11174  ax-cnre 11175  ax-pre-lttri 11176  ax-pre-lttrn 11177  ax-pre-ltadd 11178  ax-pre-mulgt0 11179  ax-pre-sup 11180  ax-addf 11181

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-iin 4963  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-isom 6548  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7677  df-om 7865  df-1st 7988  df-2nd 7989  df-supp 8159  df-tpos 8224  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-er 8696  df-map 8828  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9324  df-sup 9404  df-oi 9474  df-card 9927  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11445  df-neg 11446  df-div 11874  df-nn 12236  df-2 12305  df-3 12306  df-4 12307  df-5 12308  df-6 12309  df-7 12310  df-8 12311  df-9 12312  df-n0 12507  df-z 12594  df-dec 12714  df-uz 12865  df-rp 13019  df-fz 13538  df-fzo 13685  df-seq 14040  df-exp 14100  df-hash 14369  df-word 14553  df-concat 14610  df-substr 14681  df-pfx 14711  df-cj 15152  df-re 15153  df-im 15154  df-sqrt 15288  df-abs 15289  df-clim 15541  df-sum 15740  df-struct 17209  df-sets 17226  df-slot 17244  df-ndx 17256  df-base 17272  df-ress 17293  df-plusg 17325  df-mulr 17326  df-starv 17327  df-tset 17331  df-ple 17332  df-ds 17334  df-unif 17335  df-0g 17496  df-gsum 17497  df-mre 17640  df-mrc 17641  df-acs 17643  df-mgm 18700  df-sgrp 18779  df-mnd 18795  df-mhm 18843  df-submnd 18844  df-grp 19005  df-minusg 19006  df-mulg 19136  df-subg 19191  df-ghm 19286  df-cntz 19389  df-cmn 19854  df-abl 19855  df-mgp 20219  df-rng 20233  df-ur 20266  df-ring 20319  df-cring 20320  df-oppr 20421  df-subrng 20633  df-subrg 20657  df-cnfld 21494  df-zring 21568

This theorem is referenced by:  elrgspnlem4  33508