gsumwrd2dccat

Description: Rewrite a sum ranging over pairs of words as a sum of sums over concatenated subwords. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	gsumwrd2dccat.1	⊢ 𝐵 = ( Base ‘ 𝑀 )
	gsumwrd2dccat.2	⊢ 𝑍 = ( 0_g ‘ 𝑀 )
	gsumwrd2dccat.3	⊢ ( 𝜑 → 𝐹 : ( Word 𝐴 × Word 𝐴 ) ⟶ 𝐵 )
	gsumwrd2dccat.4	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
	gsumwrd2dccat.5	⊢ ( 𝜑 → 𝑀 ∈ CMnd )
	gsumwrd2dccat.6	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion	gsumwrd2dccat	⊢ ( 𝜑 → ( 𝑀 Σ_g 𝐹 ) = ( 𝑀 Σ_g ( 𝑤 ∈ Word 𝐴 ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumwrd2dccat.1	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		gsumwrd2dccat.2	⊢ 𝑍 = ( 0_g ‘ 𝑀 )
3		gsumwrd2dccat.3	⊢ ( 𝜑 → 𝐹 : ( Word 𝐴 × Word 𝐴 ) ⟶ 𝐵 )
4		gsumwrd2dccat.4	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
5		gsumwrd2dccat.5	⊢ ( 𝜑 → 𝑀 ∈ CMnd )
6		gsumwrd2dccat.6	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
7	1	fvexi	⊢ 𝐵 ∈ V
8	7	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
9	8 6	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
10		wrdexg	⊢ ( 𝐴 ∈ V → Word 𝐴 ∈ V )
11	9 10	syl	⊢ ( 𝜑 → Word 𝐴 ∈ V )
12	11 11	xpexd	⊢ ( 𝜑 → ( Word 𝐴 × Word 𝐴 ) ∈ V )
13		eqid	⊢ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) = ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) )
14		eqid	⊢ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) = ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ )
15		eqid	⊢ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) = ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ )
16	13 14 15 9	gsumwrd2dccatlem	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ^◡ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) = ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) )
17	16	simpld	⊢ ( 𝜑 → ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
18		f1ocnv	⊢ ( ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) : ( Word 𝐴 × Word 𝐴 ) –1-1-onto→ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ^◡ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) : ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) )
19	17 18	syl	⊢ ( 𝜑 → ^◡ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) : ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) )
20	16	simprd	⊢ ( 𝜑 → ^◡ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) = ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) )
21	20	f1oeq1d	⊢ ( 𝜑 → ( ^◡ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) : ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) ↔ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) : ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) ) )
22	19 21	mpbid	⊢ ( 𝜑 → ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) : ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) )
23	1 2 5 12 3 4 22	gsumf1o	⊢ ( 𝜑 → ( 𝑀 Σ_g 𝐹 ) = ( 𝑀 Σ_g ( 𝐹 ∘ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ) )
24		relxp	⊢ Rel ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) )
25	24	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐴 ) → Rel ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
26	25	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ Word 𝐴 Rel ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
27		reliun	⊢ ( Rel ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ Word 𝐴 Rel ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
28	26 27	sylibr	⊢ ( 𝜑 → Rel ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
29		1stdm	⊢ ( ( Rel ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 1^st ‘ 𝑏 ) ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
30	28 29	sylan	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 1^st ‘ 𝑏 ) ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
31		lencl	⊢ ( 𝑥 ∈ Word 𝐴 → ( ♯ ‘ 𝑥 ) ∈ ℕ₀ )
32	31	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐴 ) → ( ♯ ‘ 𝑥 ) ∈ ℕ₀ )
33		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
34	32 33	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐴 ) → ( ♯ ‘ 𝑥 ) ∈ ( ℤ_≥ ‘ 0 ) )
35		fzn0	⊢ ( ( 0 ... ( ♯ ‘ 𝑥 ) ) ≠ ∅ ↔ ( ♯ ‘ 𝑥 ) ∈ ( ℤ_≥ ‘ 0 ) )
36	34 35	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐴 ) → ( 0 ... ( ♯ ‘ 𝑥 ) ) ≠ ∅ )
37	36	dmdju	⊢ ( 𝜑 → dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) = Word 𝐴 )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) = Word 𝐴 )
39	30 38	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 )
40		pfxcl	⊢ ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 → ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∈ Word 𝐴 )
41	39 40	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) ∈ Word 𝐴 )
42		swrdcl	⊢ ( ( 1^st ‘ 𝑏 ) ∈ Word 𝐴 → ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ∈ Word 𝐴 )
43	39 42	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ∈ Word 𝐴 )
44	41 43	opelxpd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ∈ ( Word 𝐴 × Word 𝐴 ) )
45		sneq	⊢ ( 𝑤 = 𝑥 → { 𝑤 } = { 𝑥 } )
46		fveq2	⊢ ( 𝑤 = 𝑥 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑥 ) )
47	46	oveq2d	⊢ ( 𝑤 = 𝑥 → ( 0 ... ( ♯ ‘ 𝑤 ) ) = ( 0 ... ( ♯ ‘ 𝑥 ) ) )
48	45 47	xpeq12d	⊢ ( 𝑤 = 𝑥 → ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) = ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
49	48	cbviunv	⊢ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) = ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) )
50	49	mpteq1i	⊢ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) = ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ )
51	50	a1i	⊢ ( 𝜑 → ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) = ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) )
52	3	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ( 𝐹 ‘ 𝑎 ) ) )
53		fveq2	⊢ ( 𝑎 = ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) )
54	44 51 52 53	fmptco	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) = ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) )
55	54	oveq2d	⊢ ( 𝜑 → ( 𝑀 Σ_g ( 𝐹 ∘ ( 𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ) = ( 𝑀 Σ_g ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ) )
56		nfv	⊢ Ⅎ 𝑤 𝜑
57	3 44	cofmpt	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) = ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) )
58	20 51	eqtr2d	⊢ ( 𝜑 → ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) = ^◡ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) )
59	49	eqcomi	⊢ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) = ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) )
60	59	a1i	⊢ ( 𝜑 → ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) = ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
61		eqidd	⊢ ( 𝜑 → ( Word 𝐴 × Word 𝐴 ) = ( Word 𝐴 × Word 𝐴 ) )
62	58 60 61	f1oeq123d	⊢ ( 𝜑 → ( ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) : ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) ↔ ^◡ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1^st ‘ 𝑎 ) ++ ( 2^nd ‘ 𝑎 ) ) , ( ♯ ‘ ( 1^st ‘ 𝑎 ) ) ⟩ ) : ∪ 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) ) )
63	19 62	mpbird	⊢ ( 𝜑 → ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) : ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) )
64		f1of1	⊢ ( ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) : ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) → ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) : ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) –1-1→ ( Word 𝐴 × Word 𝐴 ) )
65	63 64	syl	⊢ ( 𝜑 → ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) : ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) –1-1→ ( Word 𝐴 × Word 𝐴 ) )
66	2	fvexi	⊢ 𝑍 ∈ V
67	66	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
68	3 12	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
69	4 65 67 68	fsuppco	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) finSupp 𝑍 )
70	57 69	eqbrtrrd	⊢ ( 𝜑 → ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) finSupp 𝑍 )
71	3	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → 𝐹 : ( Word 𝐴 × Word 𝐴 ) ⟶ 𝐵 )
72	71 44	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ∈ 𝐵 )
73	72	fmpttd	⊢ ( 𝜑 → ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) : ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ⟶ 𝐵 )
74		vsnex	⊢ { 𝑥 } ∈ V
75		ovex	⊢ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∈ V
76	74 75	xpex	⊢ ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∈ V
77	76	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐴 ) → ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∈ V )
78	77	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∈ V )
79		iunexg	⊢ ( ( Word 𝐴 ∈ V ∧ ∀ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∈ V ) → ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∈ V )
80	11 78 79	syl2anc	⊢ ( 𝜑 → ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ∈ V )
81	56 1 2 28 70 5 73 80	gsumfs2d	⊢ ( 𝜑 → ( 𝑀 Σ_g ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ) = ( 𝑀 Σ_g ( 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) ) ) )
82	23 55 81	3eqtrd	⊢ ( 𝜑 → ( 𝑀 Σ_g 𝐹 ) = ( 𝑀 Σ_g ( 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) ) ) )
83		eqid	⊢ ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) = ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) )
84		vex	⊢ 𝑤 ∈ V
85		vex	⊢ 𝑗 ∈ V
86	84 85	op1std	⊢ ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( 1^st ‘ 𝑏 ) = 𝑤 )
87	84 85	op2ndd	⊢ ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( 2^nd ‘ 𝑏 ) = 𝑗 )
88	86 87	oveq12d	⊢ ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) = ( 𝑤 prefix 𝑗 ) )
89	86	fveq2d	⊢ ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) = ( ♯ ‘ 𝑤 ) )
90	87 89	opeq12d	⊢ ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ = ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ )
91	86 90	oveq12d	⊢ ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) = ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) )
92	88 91	opeq12d	⊢ ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ = ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ )
93	92	fveq2d	⊢ ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) = ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) )
94	37	eleq2d	⊢ ( 𝜑 → ( 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↔ 𝑤 ∈ Word 𝐴 ) )
95	94	biimpa	⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → 𝑤 ∈ Word 𝐴 )
96	95	adantr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ) → 𝑤 ∈ Word 𝐴 )
97		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ Word 𝐴 ) → ( 0 ... ( ♯ ‘ 𝑥 ) ) ∈ V )
98		nfcv	⊢ Ⅎ 𝑥 ( 0 ... ( ♯ ‘ 𝑤 ) )
99		fveq2	⊢ ( 𝑥 = 𝑤 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑤 ) )
100	99	oveq2d	⊢ ( 𝑥 = 𝑤 → ( 0 ... ( ♯ ‘ 𝑥 ) ) = ( 0 ... ( ♯ ‘ 𝑤 ) ) )
101	11 97 98 100	iunsnima2	⊢ ( ( 𝜑 ∧ 𝑤 ∈ Word 𝐴 ) → ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) = ( 0 ... ( ♯ ‘ 𝑤 ) ) )
102	95 101	syldan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) = ( 0 ... ( ♯ ‘ 𝑤 ) ) )
103	102	eleq2d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↔ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
104	103	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ) → 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) )
105	100	opeliunxp2	⊢ ( ⟨ 𝑤 , 𝑗 ⟩ ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↔ ( 𝑤 ∈ Word 𝐴 ∧ 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
106	96 104 105	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ) → ⟨ 𝑤 , 𝑗 ⟩ ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
107		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ) → ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ∈ V )
108	83 93 106 107	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) ∧ 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ) → ( ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) = ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) )
109	108	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) = ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) )
110	109	oveq2d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) = ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) )
111	110	mpteq2dva	⊢ ( 𝜑 → ( 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) ) = ( 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) )
112	111	oveq2d	⊢ ( 𝜑 → ( 𝑀 Σ_g ( 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 ∈ ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1^st ‘ 𝑏 ) prefix ( 2^nd ‘ 𝑏 ) ) , ( ( 1^st ‘ 𝑏 ) substr ⟨ ( 2^nd ‘ 𝑏 ) , ( ♯ ‘ ( 1^st ‘ 𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) ) ) = ( 𝑀 Σ_g ( 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) ) )
113	102	mpteq1d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) = ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) )
114	113	oveq2d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) = ( 𝑀 Σ_g ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) )
115	37 114	mpteq12dva	⊢ ( 𝜑 → ( 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) = ( 𝑤 ∈ Word 𝐴 ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) )
116	115	oveq2d	⊢ ( 𝜑 → ( 𝑀 Σ_g ( 𝑤 ∈ dom ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( ∪ 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) ) = ( 𝑀 Σ_g ( 𝑤 ∈ Word 𝐴 ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) ) )
117	82 112 116	3eqtrd	⊢ ( 𝜑 → ( 𝑀 Σ_g 𝐹 ) = ( 𝑀 Σ_g ( 𝑤 ∈ Word 𝐴 ↦ ( 𝑀 Σ_g ( 𝑗 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) ) )

Metamath Proof Explorer

Theorem gsumwrd2dccat

Proof