Theorem elrgspnlem2 33426

Description: Lemma for elrgspn 33429. (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 33425	. 2 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅))
10		eqeq2 2776	. . . . . . 7 ⊢ ((1r‘𝑅) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))
11		eqeq2 2776	. . . . . . 7 ⊢ ((0g‘𝑅) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))
12		simpr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → 𝑤 = ∅)
13	12	fveq2d 6873	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅))
14		eqid 2764	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))
15		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 = ∅) → 𝑣 = ∅)
16	15	iftrued 4490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 = ∅) → if(𝑣 = ∅, 1, 0) = 1)
17		wrd0 14554	. . . . . . . . . . . . 13 ⊢ ∅ ∈ Word 𝐴
18	17	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ∈ Word 𝐴)
19		1zzd 12604	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
20	14, 16, 18, 19	fvmptd2 6986	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
21	20	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) = 1)
22	13, 21	eqtrd 2799	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 1)
23	12	oveq2d 7414	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (𝑀 Σg ∅))
24		eqid 2764	. . . . . . . . . . . 12 ⊢ (1r‘𝑅) = (1r‘𝑅)
25	3, 24	ringidval 20235	. . . . . . . . . . 11 ⊢ (1r‘𝑅) = (0g‘𝑀)
26	25	gsum0 18720	. . . . . . . . . 10 ⊢ (𝑀 Σg ∅) = (1r‘𝑅)
27	23, 26	eqtrdi 2815	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (1r‘𝑅))
28	22, 27	oveq12d 7416	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1 · (1r‘𝑅)))
29	2, 24	ringidcl 20317	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐵)
30	1, 29	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵)
31	2, 4	mulg1 19125	. . . . . . . . . 10 ⊢ ((1r‘𝑅) ∈ 𝐵 → (1 · (1r‘𝑅)) = (1r‘𝑅))
32	30, 31	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (1 · (1r‘𝑅)) = (1r‘𝑅))
33	32	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (1 · (1r‘𝑅)) = (1r‘𝑅))
34	28, 33	eqtrd 2799	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅))
35		eqeq1 2768	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑤 → (𝑣 = ∅ ↔ 𝑤 = ∅))
36	35	notbid 320	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑤 → (¬ 𝑣 = ∅ ↔ ¬ 𝑤 = ∅))
37	36	biimparc 483	. . . . . . . . . . . 12 ⊢ ((¬ 𝑤 = ∅ ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
38	37	adantll 724	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅)
39	38	iffalsed 4493	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → if(𝑣 = ∅, 1, 0) = 0)
40		simplr 778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 𝑤 ∈ Word 𝐴)
41		0zd 12582	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 0 ∈ ℤ)
42	14, 39, 40, 41	fvmptd2 6986	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 0)
43	42	oveq1d 7413	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤)))
44	3	ringmgp 20291	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
45	1, 44	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ Mnd)
46		sswrd 14537	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵)
47	7, 46	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵)
48	47	sselda 3938	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
49	3, 2	mgpbas 20193	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑀)
50	49	gsumwcl 18875	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵)
51	45, 48, 50	syl2an2r 695	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
52		eqid 2764	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
53	2, 52, 4	mulg0 19118	. . . . . . . . . 10 ⊢ ((𝑀 Σg 𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
54	51, 53	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
55	54	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅))
56	43, 55	eqtrd 2799	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅))
57	10, 11, 34, 56	ifbothda 4521	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))
58	57	mpteq2dva 5195	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))
59	58	oveq2d 7414	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))))
60	1	ringcmnd 20336	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CMnd)
61	60	cmnmndd 19846	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Mnd)
62	2	fvexi 6883	. . . . . . . 8 ⊢ 𝐵 ∈ V
63	62	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ V)
64	63, 7	ssexd 5282	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ V)
65		wrdexg 14539	. . . . . 6 ⊢ (𝐴 ∈ V → Word 𝐴 ∈ V)
66	64, 65	syl 17	. . . . 5 ⊢ (𝜑 → Word 𝐴 ∈ V)
67		eqid 2764	. . . . 5 ⊢ (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))
68	30, 2	eleqtrdi 2874	. . . . 5 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
69	52, 61, 66, 18, 67, 68	gsummptif1n0 20008	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) = (1r‘𝑅))
70	59, 69	eqtrd 2799	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (1r‘𝑅))
71		eqid 2764	. . . . 5 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
72		fveq1 6868	. . . . . . . . . 10 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤))
73	72	oveq1d 7413	. . . . . . . . 9 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))
74	73	mpteq2dv 5196	. . . . . . . 8 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))
75	74	oveq2d 7414	. . . . . . 7 ⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
76	75	eqeq2d 2775	. . . . . 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 5105	. . . . . . . 8 ⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0))
78		zex 12579	. . . . . . . . . 10 ⊢ ℤ ∈ V
79	78	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℤ ∈ V)
80		1zzd 12604	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑣 = ∅) → 1 ∈ ℤ)
81		0zd 12582	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ ¬ 𝑣 = ∅) → 0 ∈ ℤ)
82	80, 81	ifclda 4518	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ Word 𝐴) → if(𝑣 = ∅, 1, 0) ∈ ℤ)
83	82	fmpttd 7098	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)):Word 𝐴⟶ℤ)
84	79, 66, 83	elmapdd 8824	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ (ℤ ↑m Word 𝐴))
85	66	mptexd 7210	. . . . . . . . 9 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V)
86	83	ffund 6698	. . . . . . . . 9 ⊢ (𝜑 → Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)))
87		0zd 12582	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
88		snfi 9026	. . . . . . . . . 10 ⊢ {∅} ∈ Fin
89	88	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {∅} ∈ Fin)
90		eldifsni 4752	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ (Word 𝐴 ∖ {∅}) → 𝑣 ≠ ∅)
91	90	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → 𝑣 ≠ ∅)
92	91	neneqd 2964	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → ¬ 𝑣 = ∅)
93	92	iffalsed 4493	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → if(𝑣 = ∅, 1, 0) = 0)
94	93, 66	suppss2 8182	. . . . . . . . 9 ⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆ {∅})
95		suppssfifsupp 9328	. . . . . . . . 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 1399	. . . . . . . 8 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp 0)
97	77, 84, 96	elrabd 3654	. . . . . . 7 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
98	97, 6	eleqtrrdi 2875	. . . . . 6 ⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ 𝐹)
99		eqidd 2765	. . . . . 6 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))
100	76, 98, 99	rspcedvdw 3586	. . . . 5 ⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
101		ovexd 7433	. . . . 5 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V)
102	71, 100, 101	elrnmptd 5941	. . . 4 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
103	102, 8	eleqtrrdi 2875	. . 3 ⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆)
104	70, 103	eqeltrrd 2865	. 2 ⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆)
105		simpllr 785	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
106		simpr 488	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
107	105, 106	oveq12d 7416	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
108		eqid 2764	. . . . . . . . . . . . . 14 ⊢ (.r‘𝑅) = (.r‘𝑅)
109	66	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ∈ V)
110	1	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ Ring)
111	1	ringgrpd 20294	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 ∈ Grp)
112	111	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
113	6	ssrab3 4037	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 ⊆ (ℤ ↑m Word 𝐴)
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word 𝐴))
115	114	sselda 3938	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word 𝐴))
116	79, 66	elmapd 8823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
117	116	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑔:Word 𝐴⟶ℤ))
118	115, 117	mpbid 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
119	118	ffvelcdmda 7067	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
120	51	adantlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
121	2, 4, 112, 119, 120	mulgcld 19140	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
122	121	adantlr 725	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
123	122	ralrimiva 3156	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
124		fveq2 6869	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑤 → (𝑔‘𝑢) = (𝑔‘𝑤))
125		oveq2 7406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑤 → (𝑀 Σg 𝑢) = (𝑀 Σg 𝑤))
126	124, 125	oveq12d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑤 → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
127	126	eleq1d 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
128	127	cbvralvw 3242	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑢 ∈ Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
129	123, 128	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑢 ∈ Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
130	129	r19.21bi 3256	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑢 ∈ Word 𝐴) → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵)
131	111	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp)
132		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0))
133	132, 6	elrab2 3656	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑖 finSupp 0))
134	133	simplbi 500	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word 𝐴))
135	134	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word 𝐴))
136	79, 66	elmapd 8823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
137	136	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word 𝐴) ↔ 𝑖:Word 𝐴⟶ℤ))
138	135, 137	mpbid 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
139	138	ffvelcdmda 7067	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ)
140	51	adantlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
141	2, 4, 131, 139, 140	mulgcld 19140	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
142	141	adantllr 729	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
143	142	ralrimiva 3156	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
144		fveq2 6869	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑖‘𝑣) = (𝑖‘𝑤))
145		oveq2 7406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑤))
146	144, 145	oveq12d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑤 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
147	146	eleq1d 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑤 → (((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵))
148	147	cbvralvw 3242	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑣 ∈ Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
149	143, 148	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑣 ∈ Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
150	149	r19.21bi 3256	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵)
151	126	cbvmptv 5206	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
152		fvexd 6884	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V)
153		0zd 12582	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ)
154	66	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ∈ V)
155		ssidd 3961	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴)
156		breq1 5105	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0))
157	156, 6	elrab2 3656	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word 𝐴) ∧ 𝑔 finSupp 0))
158	157	simprbi 501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0)
159	158	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0)
160	2, 52, 4	mulg0 19118	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅))
161	160	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅))
162	152, 153, 154, 155, 120, 118, 159, 161	fisuppov1 32887	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
163	162	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
164	151, 163	eqbrtrid 5137	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) finSupp (0g‘𝑅))
165	146	cbvmptv 5206	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
166	162	ralrimiva 3156	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
167		fveq1 6868	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤))
168	167	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))
169	168	mpteq2dv 5196	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
170	169	breq1d 5112	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅)))
171	170	cbvralvw 3242	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅) ↔ ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
172	166, 171	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
173	172	r19.21bi 3256	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
174	173	adantlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp (0g‘𝑅))
175	165, 174	eqbrtrid 5137	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) finSupp (0g‘𝑅))
176	2, 108, 52, 109, 109, 110, 130, 150, 164, 175	gsumdixp 20369	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))))(.r‘𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))))
177	151	oveq2i 7409	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))
178	165	oveq2i 7409	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))
179	177, 178	oveq12i 7410	. . . . . . . . . . . . . 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 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Ring)
182	122	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)
183	111	ad4antr 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Grp)
184	138	adantlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ)
185	184	ffvelcdmda 7067	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑓 ∈ Word 𝐴) → (𝑖‘𝑓) ∈ ℤ)
186	185	adantlr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑖‘𝑓) ∈ ℤ)
187	45	ad4antr 742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
188	47	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐵)
189	188	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵)
190	189	sselda 3938	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑓 ∈ Word 𝐵)
191	49	gsumwcl 18875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg 𝑓) ∈ 𝐵)
192	187, 190, 191	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑓) ∈ 𝐵)
193	2, 4, 183, 186, 192	mulgcld 19140	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)
194	2, 108, 181, 182, 193	ringcld 20312	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
195	194	anasss 470	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
196	195	ralrimivva 3207	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴∀𝑓 ∈ Word 𝐴(((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵)
197		eqid 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
198	197	fmpo 8051	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ Word 𝐴∀𝑓 ∈ Word 𝐴(((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵 ↔ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵)
199	196, 198	sylib 220	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵)
200		vex 3460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑤 ∈ V
201		vex 3460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑓 ∈ V
202	200, 201	op1std 7982	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (1st ‘𝑎) = 𝑤)
203	202	fveq2d 6873	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑔‘(1st ‘𝑎)) = (𝑔‘𝑤))
204	202	oveq2d 7414	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (1st ‘𝑎)) = (𝑀 Σg 𝑤))
205	203, 204	oveq12d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))
206	200, 201	op2ndd 7983	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (2nd ‘𝑎) = 𝑓)
207	206	fveq2d 6873	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑖‘(2nd ‘𝑎)) = (𝑖‘𝑓))
208	206	oveq2d 7414	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (𝑀 Σg (2nd ‘𝑎)) = (𝑀 Σg 𝑓))
209	207, 208	oveq12d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓)))
210	205, 209	oveq12d 7416	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ⟨𝑤, 𝑓⟩ → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
211	210	mpompt 7512	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
212	66, 66	xpexd 7736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (Word 𝐴 × Word 𝐴) ∈ V)
213	212	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (Word 𝐴 × Word 𝐴) ∈ V)
214	213	mptexd 7210	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) ∈ V)
215		fvexd 6884	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (0g‘𝑅) ∈ V)
216	110	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Ring)
217	111	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Grp)
218	118	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ)
219		xp1st 8004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1st ‘𝑎) ∈ Word 𝐴)
220	219	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴)
221	218, 220	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑔‘(1st ‘𝑎)) ∈ ℤ)
222	216, 44	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑀 ∈ Mnd)
223	188	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵)
224	223, 220	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐵)
225	49	gsumwcl 18875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ (1st ‘𝑎) ∈ Word 𝐵) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
226	222, 224, 225	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
227	2, 4, 217, 221, 226	mulgcld 19140	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) ∈ 𝐵)
228	184	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ)
229		xp2nd 8005	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴)
230	229	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴)
231	228, 230	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈ ℤ)
232	223, 230	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐵)
233	49	gsumwcl 18875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ Mnd ∧ (2nd ‘𝑎) ∈ Word 𝐵) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
234	222, 232, 233	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
235	2, 4, 217, 231, 234	mulgcld 19140	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) ∈ 𝐵)
236	2, 108, 216, 227, 235	ringcld 20312	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) ∈ 𝐵)
237	236	fmpttd 7098	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))):(Word 𝐴 × Word 𝐴)⟶𝐵)
238	237	ffund 6698	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Fun (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))))
239	159	fsuppimpd 9317	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin)
240	133	simprbi 501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0)
241	240	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0)
242	241	fsuppimpd 9317	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑖 supp 0) ∈ Fin)
243		xpfi 9266	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑔 supp 0) ∈ Fin ∧ (𝑖 supp 0) ∈ Fin) → ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin)
244	239, 242, 243	syl2an2r 695	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin)
245	118	ffnd 6694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
246	245	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 Fn Word 𝐴)
247	246	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑔 Fn Word 𝐴)
248	109	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ∈ V)
249		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 0 ∈ ℤ)
250		xp1st 8004	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (1st ‘𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
251	250	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0)))
252	247, 248, 249, 251	fvdifsupp 8153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑔‘(1st ‘𝑎)) = 0)
253	252	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) = (0 · (𝑀 Σg (1st ‘𝑎))))
254	45	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑀 ∈ Mnd)
255	188	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵)
256	251	eldifad 3918	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴)
257	255, 256	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐵)
258	254, 257, 225	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
259	2, 52, 4	mulg0 19118	. . . . . . . . . . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) = (0g‘𝑅))
262	261	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . 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 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Ring)
264	111	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Grp)
265	184	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ)
266		xp2nd 8005	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴)
267	266	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴)
268	265, 267	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈ ℤ)
269	255, 267	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐵)
270	254, 269, 233	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
271	2, 4, 264, 268, 270	mulgcld 19140	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) ∈ 𝐵)
272	2, 108, 52, 263, 271	ringlzd 20347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((0g‘𝑅)(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
273	262, 272	eqtrd 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
274	138	ffnd 6694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
275	274	adantlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴)
276	275	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑖 Fn Word 𝐴)
277	109	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ∈ V)
278		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 0 ∈ ℤ)
279		xp2nd 8005	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (2nd ‘𝑎) ∈ (Word 𝐴 ∖ (𝑖 supp 0)))
280	279	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd ‘𝑎) ∈ (Word 𝐴 ∖ (𝑖 supp 0)))
281	276, 277, 278, 280	fvdifsupp 8153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑖‘(2nd ‘𝑎)) = 0)
282	281	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) = (0 · (𝑀 Σg (2nd ‘𝑎))))
283	45	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑀 ∈ Mnd)
284	188	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ⊆ Word 𝐵)
285	280	eldifad 3918	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd ‘𝑎) ∈ Word 𝐴)
286	284, 285	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd ‘𝑎) ∈ Word 𝐵)
287	283, 286, 233	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (2nd ‘𝑎)) ∈ 𝐵)
288	2, 52, 4	mulg0 19118	. . . . . . . . . . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))) = (0g‘𝑅))
291	290	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . 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 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Ring)
293	111	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Grp)
294	118	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ)
295	294	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑔:Word 𝐴⟶ℤ)
296		xp1st 8004	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (1st ‘𝑎) ∈ Word 𝐴)
297	296	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st ‘𝑎) ∈ Word 𝐴)
298	295, 297	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑔‘(1st ‘𝑎)) ∈ ℤ)
299	284, 297	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st ‘𝑎) ∈ Word 𝐵)
300	283, 299, 225	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (1st ‘𝑎)) ∈ 𝐵)
301	2, 4, 293, 298, 300	mulgcld 19140	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎))) ∈ 𝐵)
302	2, 108, 52, 292, 301	ringrzd 20348	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅))
303	291, 302	eqtrd 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
304		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))))
305		difxp 6151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))) = (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))))
306	304, 305	eleqtrdi 2874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
307		elun 4108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) ↔ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
308	306, 307	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))))
309	273, 303, 308	mpjaodan 971	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎)))) = (0g‘𝑅))
310	309, 213	suppss2 8182	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) supp (0g‘𝑅)) ⊆ ((𝑔 supp 0) × (𝑖 supp 0)))
311	244, 310	ssfid 9215	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) supp (0g‘𝑅)) ∈ Fin)
312	214, 215, 238, 311	isfsuppd 9314	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st ‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd ‘𝑎))))) finSupp (0g‘𝑅))
313	211, 312	eqbrtrrid 5138	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) finSupp (0g‘𝑅))
314	60	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ CMnd)
315	7	ad2antrr 736	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝐴 ⊆ 𝐵)
316	2, 52, 199, 313, 314, 315	gsumwrd2dccat 33260	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
317	126	oveq1d 7413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))
318		fveq2 6869	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑓 → (𝑖‘𝑣) = (𝑖‘𝑓))
319		oveq2 7406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑓 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑓))
320	318, 319	oveq12d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑓 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓)))
321	320	oveq2d 7414	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑓 → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
322	317, 321	cbvmpov 7493	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))
323	322	oveq2i 7409	. . . . . . . . . . . . . . 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 14725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑣 ∈ Word 𝐴 ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
326	325	adantll 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = 𝑣)
327	326	oveq2d 7414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) = (𝑀 Σg 𝑣))
328	327	oveq2d 7414	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
329	328	mpteq2dva 5195	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣))))
330	329	oveq2d 7414	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
331		df-ov 7401	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)
332	188	sselda 3938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
333	332	ad4ant13 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵)
334	187, 333, 50	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵)
335	2, 4, 108	mulgass3 20404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑅 ∈ Ring ∧ ((𝑖‘𝑓) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ (𝑀 Σg 𝑓) ∈ 𝐵)) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
336	181, 186, 334, 192, 335	syl13anc 1393	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
337	336	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))))
338	119	ad4ant13 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ)
339	2, 4, 108	mulgass2 20361	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ Ring ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))))
340	181, 338, 334, 193, 339	syl13anc 1393	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))))
341	2, 108, 181, 334, 192	ringcld 20312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)
342	2, 4	mulgass 19155	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑓) ∈ ℤ ∧ ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))))
343	183, 338, 186, 341, 342	syl13anc 1393	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))))
344	337, 340, 343	3eqtr4d 2809	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
345	3, 108	mgpplusg 20192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (.r‘𝑅) = (+g‘𝑀)
346	49, 345	gsumccat 18877	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))
347	187, 333, 190, 346	syl3anc 1392	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))
348	347	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))
349	344, 348	eqtr4d 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
350	349	adantllr 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
351	350	adantllr 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
352	351	3impa 1123	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))
353	352	mpoeq3dva 7475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓)))))
354		fveq2 6869	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑣 prefix 𝑗) → (𝑔‘𝑤) = (𝑔‘(𝑣 prefix 𝑗)))
355		fveq2 6869	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) → (𝑖‘𝑓) = (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
356	354, 355	oveqan12d 7417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → ((𝑔‘𝑤) · (𝑖‘𝑓)) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
357		oveq12 7407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑤 ++ 𝑓) = ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
358	357	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (𝑀 Σg (𝑤 ++ 𝑓)) = (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
359	356, 358	oveq12d 7416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
360	359	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ (𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
361		pfxcl 14693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ Word 𝐴 → (𝑣 prefix 𝑗) ∈ Word 𝐴)
362	361	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 prefix 𝑗) ∈ Word 𝐴)
363		swrdcl 14661	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ Word 𝐴 → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
364	363	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩) ∈ Word 𝐴)
365		ovexd 7433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))) ∈ V)
366	353, 360, 362, 364, 365	ovmpod 7550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
367	331, 366	eqtr3id 2813	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))
368	367	mpteq2dva 5195	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))))
369	368	oveq2d 7414	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))))))
370		eqid 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))
371		fveq2 6869	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑣 → (♯‘𝑡) = (♯‘𝑣))
372	371	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑣 → (0...(♯‘𝑡)) = (0...(♯‘𝑣)))
373		fvoveq1 7421	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑣 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑣 prefix 𝑗)))
374		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑣 → 𝑡 = 𝑣)
375	371	opeq2d 4840	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑣 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑣)⟩)
376	374, 375	oveq12d 7416	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑣 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))
377	376	fveq2d 6873	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑣 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)))
378	373, 377	oveq12d 7416	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑣 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
379	378	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 = 𝑣 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
380	372, 379	sumeq12dv 15735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑣 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
381		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐴)
382		fzfid 13988	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (0...(♯‘𝑣)) ∈ Fin)
383	294	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑔:Word 𝐴⟶ℤ)
384	383, 362	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑔‘(𝑣 prefix 𝑗)) ∈ ℤ)
385	184	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑖:Word 𝐴⟶ℤ)
386	385, 364	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)) ∈ ℤ)
387	384, 386	zmulcld 12685	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℤ)
388	387	zcnd 12680	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
389	382, 388	fsumcl 15762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) ∈ ℂ)
390	370, 380, 381, 389	fvmptd3 7001	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))))
391	390	oveq1d 7413	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
392	111	ad3antrrr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑅 ∈ Grp)
393	45	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑀 ∈ Mnd)
394	315, 46	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐵)
395	394	sselda 3938	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐵)
396	49	gsumwcl 18875	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σg 𝑣) ∈ 𝐵)
397	393, 395, 396	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑀 Σg 𝑣) ∈ 𝐵)
398	2, 4, 392, 382, 397, 387	gsummulgc2 33248	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))
399	391, 398	eqtr4d 2802	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr ⟨𝑗, (♯‘𝑣)⟩))) · (𝑀 Σg 𝑣)))))
400	330, 369, 399	3eqtr4rd 2810	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))
401	400	mpteq2dva 5195	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩)))))
402	401	oveq2d 7414	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘⟨(𝑣 prefix 𝑗), (𝑣 substr ⟨𝑗, (♯‘𝑣)⟩)⟩))))))
403	316, 324, 402	3eqtr4d 2809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
404	176, 180, 403	3eqtr3d 2807	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))))
405		fveq1 6868	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤))
406	405	oveq1d 7413	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))
407	406	mpteq2dv 5196	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))
408	407	oveq2d 7414	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
409	408	cbvmptv 5206	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
410		fveq1 6868	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (ℎ‘𝑤) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
411	410	oveq1d 7413	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
412	411	mpteq2dv 5196	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤))))
413	412	oveq2d 7414	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))))
414	413	eqeq2d 2775	. . . . . . . . . . . . . . 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 5105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) → (𝑓 finSupp 0 ↔ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0))
416	78	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V)
417		fzfid 13988	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → (0...(♯‘𝑡)) ∈ Fin)
418	294	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑔:Word 𝐴⟶ℤ)
419		pfxcl 14693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ Word 𝐴 → (𝑡 prefix 𝑗) ∈ Word 𝐴)
420	419	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 prefix 𝑗) ∈ Word 𝐴)
421	418, 420	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑔‘(𝑡 prefix 𝑗)) ∈ ℤ)
422	184	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑖:Word 𝐴⟶ℤ)
423		swrdcl 14661	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 ∈ Word 𝐴 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
424	423	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) ∈ Word 𝐴)
425	422, 424	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) ∈ ℤ)
426	421, 425	zmulcld 12685	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
427	417, 426	fsumzcl 15764	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) ∈ ℤ)
428	427	fmpttd 7098	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))):Word 𝐴⟶ℤ)
429	416, 109, 428	elmapdd 8824	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ (ℤ ↑m Word 𝐴))
430		0zd 12582	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 ∈ ℤ)
431	428	ffund 6698	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Fun (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))))
432		ccatfn 14587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ++ Fn (V × V)
433		fnfun 6623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( ++ Fn (V × V) → Fun ++ )
434	432, 433	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ Fun ++
435		imafi 9261	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Fun ++ ∧ ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin) → ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ∈ Fin)
436	434, 244, 435	sylancr 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ∈ Fin)
437		fveq2 6869	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑤 → (♯‘𝑡) = (♯‘𝑤))
438	437	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑤 → (0...(♯‘𝑡)) = (0...(♯‘𝑤)))
439		fvoveq1 7421	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑤 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑤 prefix 𝑗)))
440		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑤 → 𝑡 = 𝑤)
441	437	opeq2d 4840	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 𝑤 → ⟨𝑗, (♯‘𝑡)⟩ = ⟨𝑗, (♯‘𝑤)⟩)
442	440, 441	oveq12d 7416	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 𝑤 → (𝑡 substr ⟨𝑗, (♯‘𝑡)⟩) = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))
443	442	fveq2d 6873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 = 𝑤 → (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)) = (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
444	439, 443	oveq12d 7416	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑤 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
445	444	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = 𝑤 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
446	438, 445	sumeq12dv 15735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 = 𝑤 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
447		oveq1 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑢 ++ 𝑣) = ((𝑤 prefix 𝑗) ++ 𝑣))
448	447	eqeq2d 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑤 = (𝑢 ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣)))
449		oveq2 7406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑣 = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) → ((𝑤 prefix 𝑗) ++ 𝑣) = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
450	449	eqeq2d 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑣 = (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) → (𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))))
451	246	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑔 Fn Word 𝐴)
452	109	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → Word 𝐴 ∈ V)
453		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 0 ∈ ℤ)
454		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))))
455	454	eldifad 3918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ Word 𝐴)
456	455	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑤 ∈ Word 𝐴)
457		pfxcl 14693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ Word 𝐴 → (𝑤 prefix 𝑗) ∈ Word 𝐴)
458	456, 457	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 prefix 𝑗) ∈ Word 𝐴)
459	458	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 prefix 𝑗) ∈ Word 𝐴)
460		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑔‘(𝑤 prefix 𝑗)) ≠ 0)
461	451, 452, 453, 459, 460	elsuppfnd 32886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 prefix 𝑗) ∈ (𝑔 supp 0))
462	275	ad4antr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑖 Fn Word 𝐴)
463		swrdcl 14661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑤 ∈ Word 𝐴 → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
464	456, 463	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
465	464	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ Word 𝐴)
466		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)
467	462, 452, 453, 465, 466	elsuppfnd 32886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩) ∈ (𝑖 supp 0))
468	456	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ Word 𝐴)
469		simpllr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑗 ∈ (0...(♯‘𝑤)))
470		pfxcctswrd 14725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑤 ∈ Word 𝐴 ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
471	468, 469, 470	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 𝑤)
472	471	eqcomd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)))
473	448, 450, 461, 467, 472	2rspcedvdw 3597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))
474		fnov 7529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ( ++ Fn (V × V) ↔ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣)))
475	432, 474	mpbi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣))
476	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⊤ → 𝑤 ∈ V)
477		ssv 3962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 supp 0) ⊆ V
478	477	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⊤ → (𝑔 supp 0) ⊆ V)
479		ssv 3962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 supp 0) ⊆ V
480	479	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⊤ → (𝑖 supp 0) ⊆ V)
481	475, 476, 478, 480	elimampo 7535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⊤ → (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣)))
482	481	mptru 1569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))
483	473, 482	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
484	483	anasss 470	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
485	454	ad3antrrr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))))
486	485	eldifbd 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
487	486	anasss 470	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0)) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
488	484, 487	pm2.65da 826	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0))
489		df-ne 2960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ↔ ¬ (𝑔‘(𝑤 prefix 𝑗)) = 0)
490		df-ne 2960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0 ↔ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0)
491	489, 490	anbi12i 637	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) ↔ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
492	491	notbii 322	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0) ↔ ¬ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
493		pm4.57 1004	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0) ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
494	492, 493	bitr2i 278	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0) ↔ ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ≠ 0))
495	488, 494	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0))
496	294	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑔:Word 𝐴⟶ℤ)
497	496, 458	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℤ)
498	497	zcnd 12680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℂ)
499	184	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑖:Word 𝐴⟶ℤ)
500	499, 464	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℤ)
501	500	zcnd 12680	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) ∈ ℂ)
502	498, 501	mul0ord 11837	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0 ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)) = 0)))
503	495, 502	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0)
504	503	sumeq2dv 15731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = Σ𝑗 ∈ (0...(♯‘𝑤))0)
505		fzssuz 13572	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0...(♯‘𝑤)) ⊆ (ℤ≥‘0)
506		sumz 15751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((0...(♯‘𝑤)) ⊆ (ℤ≥‘0) ∨ (0...(♯‘𝑤)) ∈ Fin) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
507	506	orcs 886	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((0...(♯‘𝑤)) ⊆ (ℤ≥‘0) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
508	505, 507	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0)
509	504, 508	eqtrd 2799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr ⟨𝑗, (♯‘𝑤)⟩))) = 0)
510	446, 509	sylan9eqr 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑡 = 𝑤) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))) = 0)
511		0zd 12582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 0 ∈ ℤ)
512	370, 510, 455, 511	fvmptd2 6986	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) = 0)
513	428, 512	suppss 8176	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ⊆ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))
514	436, 513	ssfid 9215	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) supp 0) ∈ Fin)
515	429, 430, 431, 514	isfsuppd 9314	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) finSupp 0)
516	415, 429, 515	elrabd 3654	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ {𝑓 ∈ (ℤ ↑m Word 𝐴) ∣ 𝑓 finSupp 0})
517	516, 6	eleqtrrdi 2875	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩)))) ∈ 𝐹)
518		fveq2 6869	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = 𝑤 → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤))
519	518, 145	oveq12d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑤 → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
520	519	cbvmptv 5206	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑤) · (𝑀 Σg 𝑤)))
521	520	oveq2i 7409	. . . . . . . . . . . . . . . 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 3586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))))
524		ovexd 7433	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ V)
525	409, 523, 524	elrnmptd 5941	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
526	525, 8	eleqtrrdi 2875	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr ⟨𝑗, (♯‘𝑡)⟩))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ 𝑆)
527	404, 526	eqeltrd 2864	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
528	527	adantllr 729	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
529	528	adantllr 729	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
530	529	adantlr 725	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
531	530	adantr 484	. . . . . . 7 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆)
532	107, 531	eqeltrd 2864	. . . . . 6 ⊢ (((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
533	8	eleq2i 2856	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
534	169	oveq2d 7414	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
535	534	cbvmptv 5206	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
536	535	elrnmpt 5936	. . . . . . . . . 10 ⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))))
537	536	elv 3461	. . . . . . . . 9 ⊢ (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
538	533, 537	sylbb 221	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑆 → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
539	538	adantl 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
540	539	ad2antrr 736	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))
541	532, 540	r19.29a 3172	. . . . 5 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
542	8	eleq2i 2856	. . . . . . 7 ⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
543	71	elrnmpt 5936	. . . . . . . 8 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))))
544	543	elv 3461	. . . . . . 7 ⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
545	542, 544	sylbb 221	. . . . . 6 ⊢ (𝑥 ∈ 𝑆 → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
546	545	ad2antlr 737	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))
547	541, 546	r19.29a 3172	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
548	547	anasss 470	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
549	548	ralrimivva 3207	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)
550	2, 24, 108	issubrg2 20644	. . 3 ⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)))
551	550	biimpar 481	. 2 ⊢ ((𝑅 ∈ Ring ∧ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)) → 𝑆 ∈ (SubRing‘𝑅))
552	1, 9, 104, 549, 551	syl13anc 1393	1 ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∧ w3a 1099   = wceq 1562  ⊤wtru 1563   ∈ wcel 2144   ≠ wne 2959  ∀wral 3078  ∃wrex 3088  {crab 3416  Vcvv 3456   ∖ cdif 3903   ∪ cun 3904   ⊆ wss 3906  ∅c0 4287  ifcif 4482  {csn 4584  ⟨cop 4590   class class class wbr 5102   ↦ cmpt 5183   × cxp 5647  ran crn 5650   “ cima 5652  Fun wfun 6517   Fn wfn 6518  ⟶wf 6519  ‘cfv 6523  (class class class)co 7398   ∈ cmpo 7400  1^st c1st 7970  2^nd c2nd 7971   supp csupp 8142   ↑_m cmap 8810  Fincfn 8929   finSupp cfsupp 9309  ℂcc 11073  0cc0 11075  1c1 11076   · cmul 11080  ℤcz 12570  ℤ_≥cuz 12841  ...cfz 13514  ♯chash 14345  Word cword 14528   ++ cconcat 14585   substr csubstr 14656   prefix cpfx 14686  Σcsu 15715  Basecbs 17247  ._rcmulr 17289  0_gc0g 17470   Σ_g cgsu 17471  Mndcmnd 18770  Grpcgrp 18977  ._gcmg 19111  SubGrpcsubg 19164  CMndccmn 19822  mulGrpcmgp 20188  1_rcur 20233  Ringcrg 20285  SubRingcsubrg 20621  RingSpancrgspn 20662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-inf2 9598  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153  ax-addf 11154

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-se 5603  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-isom 6532  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-of 7662  df-om 7849  df-1st 7972  df-2nd 7973  df-supp 8143  df-tpos 8208  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-1o 8439  df-2o 8440  df-er 8680  df-map 8812  df-en 8930  df-dom 8931  df-sdom 8932  df-fin 8933  df-fsupp 9310  df-sup 9390  df-oi 9460  df-card 9899  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847  df-nn 12213  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12484  df-z 12571  df-dec 12691  df-uz 12842  df-rp 12996  df-fz 13515  df-fzo 13662  df-seq 14017  df-exp 14077  df-hash 14346  df-word 14529  df-concat 14586  df-substr 14657  df-pfx 14687  df-cj 15128  df-re 15129  df-im 15130  df-sqrt 15264  df-abs 15265  df-clim 15517  df-sum 15716  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17248  df-ress 17269  df-plusg 17301  df-mulr 17302  df-starv 17303  df-tset 17307  df-ple 17308  df-ds 17310  df-unif 17311  df-0g 17472  df-gsum 17473  df-mre 17616  df-mrc 17617  df-acs 17619  df-mgm 18676  df-sgrp 18755  df-mnd 18771  df-mhm 18819  df-submnd 18820  df-grp 18980  df-minusg 18981  df-mulg 19112  df-subg 19167  df-ghm 19256  df-cntz 19359  df-cmn 19824  df-abl 19825  df-mgp 20189  df-rng 20201  df-ur 20234  df-ring 20287  df-cring 20288  df-oppr 20388  df-subrng 20598  df-subrg 20622  df-cnfld 21427  df-zring 21501

This theorem is referenced by:  elrgspnlem4  33428