elrgspnlem2

	Ref	Expression
Hypotheses	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	elrgspnlem2	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )

Proof

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

Metamath Proof Explorer

Theorem elrgspnlem2

Proof