Metamath Proof Explorer


Theorem 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 𝑍 = ( 0g𝑀 )
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 𝑍 = ( 0g𝑀 )
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 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) = ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ )
15 eqid ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) = ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ )
16 13 14 15 9 gsumwrd2dccatlem ( 𝜑 → ( ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) : ( Word 𝐴 × Word 𝐴 ) –1-1-onto 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ∧ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) = ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) )
17 16 simpld ( 𝜑 → ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) : ( Word 𝐴 × Word 𝐴 ) –1-1-onto 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) )
18 f1ocnv ( ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) : ( Word 𝐴 × Word 𝐴 ) –1-1-onto 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) → ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) : 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) )
19 17 18 syl ( 𝜑 ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) : 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) )
20 16 simprd ( 𝜑 ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) = ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) )
21 20 f1oeq1d ( 𝜑 → ( ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) : 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) ↔ ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) : 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) ) )
22 19 21 mpbid ( 𝜑 → ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) : 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) )
23 1 2 5 12 3 4 22 gsumf1o ( 𝜑 → ( 𝑀 Σg 𝐹 ) = ( 𝑀 Σg ( 𝐹 ∘ ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ) )
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 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 1st𝑏 ) ∈ dom 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
30 28 29 sylan ( ( 𝜑𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 1st𝑏 ) ∈ dom 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) )
31 lencl ( 𝑥 ∈ Word 𝐴 → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
32 31 adantl ( ( 𝜑𝑥 ∈ Word 𝐴 ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
33 nn0uz 0 = ( ℤ ‘ 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 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 1st𝑏 ) ∈ Word 𝐴 )
40 pfxcl ( ( 1st𝑏 ) ∈ Word 𝐴 → ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) ∈ Word 𝐴 )
41 39 40 syl ( ( 𝜑𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) ∈ Word 𝐴 )
42 swrdcl ( ( 1st𝑏 ) ∈ Word 𝐴 → ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ∈ Word 𝐴 )
43 39 42 syl ( ( 𝜑𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ∈ Word 𝐴 )
44 41 43 opelxpd ( ( 𝜑𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ∈ ( 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 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) = ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ )
51 50 a1i ( 𝜑 → ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) = ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) )
52 3 feqmptd ( 𝜑𝐹 = ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ( 𝐹𝑎 ) ) )
53 fveq2 ( 𝑎 = ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ → ( 𝐹𝑎 ) = ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) )
54 44 51 52 53 fmptco ( 𝜑 → ( 𝐹 ∘ ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) = ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) )
55 54 oveq2d ( 𝜑 → ( 𝑀 Σg ( 𝐹 ∘ ( 𝑏 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ) = ( 𝑀 Σg ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ) )
56 nfv 𝑤 𝜑
57 3 44 cofmpt ( 𝜑 → ( 𝐹 ∘ ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) = ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) )
58 20 51 eqtr2d ( 𝜑 → ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) = ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) )
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 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) : 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) ↔ ( 𝑎 ∈ ( Word 𝐴 × Word 𝐴 ) ↦ ⟨ ( ( 1st𝑎 ) ++ ( 2nd𝑎 ) ) , ( ♯ ‘ ( 1st𝑎 ) ) ⟩ ) : 𝑤 ∈ Word 𝐴 ( { 𝑤 } × ( 0 ... ( ♯ ‘ 𝑤 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) ) )
63 19 62 mpbird ( 𝜑 → ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) : 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) )
64 f1of1 ( ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) : 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) –1-1-onto→ ( Word 𝐴 × Word 𝐴 ) → ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) : 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) –1-1→ ( Word 𝐴 × Word 𝐴 ) )
65 63 64 syl ( 𝜑 → ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) : 𝑥 ∈ 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 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) finSupp 𝑍 )
70 57 69 eqbrtrrd ( 𝜑 → ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) finSupp 𝑍 )
71 3 adantr ( ( 𝜑𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → 𝐹 : ( Word 𝐴 × Word 𝐴 ) ⟶ 𝐵 )
72 71 44 ffvelcdmd ( ( 𝜑𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ∈ 𝐵 )
73 72 fmpttd ( 𝜑 → ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) : 𝑥 ∈ 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 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ) = ( 𝑀 Σg ( 𝑤 ∈ dom 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σg ( 𝑗 ∈ ( 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) ) ) )
82 23 55 81 3eqtrd ( 𝜑 → ( 𝑀 Σg 𝐹 ) = ( 𝑀 Σg ( 𝑤 ∈ dom 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σg ( 𝑗 ∈ ( 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) ) ) )
83 eqid ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) = ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) )
84 vex 𝑤 ∈ V
85 vex 𝑗 ∈ V
86 84 85 op1std ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( 1st𝑏 ) = 𝑤 )
87 84 85 op2ndd ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( 2nd𝑏 ) = 𝑗 )
88 86 87 oveq12d ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) = ( 𝑤 prefix 𝑗 ) )
89 86 fveq2d ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( ♯ ‘ ( 1st𝑏 ) ) = ( ♯ ‘ 𝑤 ) )
90 87 89 opeq12d ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ = ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ )
91 86 90 oveq12d ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) = ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) )
92 88 91 opeq12d ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ = ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ )
93 92 fveq2d ( 𝑏 = ⟨ 𝑤 , 𝑗 ⟩ → ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) = ( 𝐹 ‘ ⟨ ( 𝑤 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 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) = ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) )
109 108 mpteq2dva ( ( 𝜑𝑤 ∈ dom 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 𝑗 ∈ ( 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) = ( 𝑗 ∈ ( 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) )
110 109 oveq2d ( ( 𝜑𝑤 ∈ dom 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) → ( 𝑀 Σg ( 𝑗 ∈ ( 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) = ( 𝑀 Σg ( 𝑗 ∈ ( 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) )
111 110 mpteq2dva ( 𝜑 → ( 𝑤 ∈ dom 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σg ( 𝑗 ∈ ( 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) ) = ( 𝑤 ∈ dom 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σg ( 𝑗 ∈ ( 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( 𝐹 ‘ ⟨ ( 𝑤 prefix 𝑗 ) , ( 𝑤 substr ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) )
112 111 oveq2d ( 𝜑 → ( 𝑀 Σg ( 𝑤 ∈ dom 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝑀 Σg ( 𝑗 ∈ ( 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) “ { 𝑤 } ) ↦ ( ( 𝑏 𝑥 ∈ Word 𝐴 ( { 𝑥 } × ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ↦ ( 𝐹 ‘ ⟨ ( ( 1st𝑏 ) prefix ( 2nd𝑏 ) ) , ( ( 1st𝑏 ) substr ⟨ ( 2nd𝑏 ) , ( ♯ ‘ ( 1st𝑏 ) ) ⟩ ) ⟩ ) ) ‘ ⟨ 𝑤 , 𝑗 ⟩ ) ) ) ) ) = ( 𝑀 Σ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 ⟨ 𝑗 , ( ♯ ‘ 𝑤 ) ⟩ ) ⟩ ) ) ) ) ) )