This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- B = ( Base ` M )
gsumwrd2dccat.2 
|- Z = ( 0g ` M )
gsumwrd2dccat.3 
|- ( ph -> F : ( Word A X. Word A ) --> B )
gsumwrd2dccat.4 
|- ( ph -> F finSupp Z )
gsumwrd2dccat.5 
|- ( ph -> M e. CMnd )
gsumwrd2dccat.6 
|- ( ph -> A C_ B )
Assertion gsumwrd2dccat 
|- ( ph -> ( M gsum F ) = ( M gsum ( w e. Word A |-> ( M gsum ( j e. ( 0 ... ( # ` w ) ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumwrd2dccat.1 
 |-  B = ( Base ` M )
2 gsumwrd2dccat.2 
 |-  Z = ( 0g ` M )
3 gsumwrd2dccat.3 
 |-  ( ph -> F : ( Word A X. Word A ) --> B )
4 gsumwrd2dccat.4 
 |-  ( ph -> F finSupp Z )
5 gsumwrd2dccat.5 
 |-  ( ph -> M e. CMnd )
6 gsumwrd2dccat.6 
 |-  ( ph -> A C_ B )
7 1 fvexi 
 |-  B e. _V
8 7 a1i 
 |-  ( ph -> B e. _V )
9 8 6 ssexd 
 |-  ( ph -> A e. _V )
10 wrdexg 
 |-  ( A e. _V -> Word A e. _V )
11 9 10 syl 
 |-  ( ph -> Word A e. _V )
12 11 11 xpexd 
 |-  ( ph -> ( Word A X. Word A ) e. _V )
13 eqid 
 |-  U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) = U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) )
14 eqid 
 |-  ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) = ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. )
15 eqid 
 |-  ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) = ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. )
16 13 14 15 9 gsumwrd2dccatlem 
 |-  ( ph -> ( ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) : ( Word A X. Word A ) -1-1-onto-> U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) /\ `' ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) = ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) )
17 16 simpld 
 |-  ( ph -> ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) : ( Word A X. Word A ) -1-1-onto-> U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) )
18 f1ocnv 
 |-  ( ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) : ( Word A X. Word A ) -1-1-onto-> U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) -> `' ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) : U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) -1-1-onto-> ( Word A X. Word A ) )
19 17 18 syl 
 |-  ( ph -> `' ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) : U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) -1-1-onto-> ( Word A X. Word A ) )
20 16 simprd 
 |-  ( ph -> `' ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) = ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) )
21 20 f1oeq1d 
 |-  ( ph -> ( `' ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) : U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) -1-1-onto-> ( Word A X. Word A ) <-> ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) : U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) -1-1-onto-> ( Word A X. Word A ) ) )
22 19 21 mpbid 
 |-  ( ph -> ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) : U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) -1-1-onto-> ( Word A X. Word A ) )
23 1 2 5 12 3 4 22 gsumf1o 
 |-  ( ph -> ( M gsum F ) = ( M gsum ( F o. ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ) )
24 relxp 
 |-  Rel ( { x } X. ( 0 ... ( # ` x ) ) )
25 24 a1i 
 |-  ( ( ph /\ x e. Word A ) -> Rel ( { x } X. ( 0 ... ( # ` x ) ) ) )
26 25 ralrimiva 
 |-  ( ph -> A. x e. Word A Rel ( { x } X. ( 0 ... ( # ` x ) ) ) )
27 reliun 
 |-  ( Rel U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) <-> A. x e. Word A Rel ( { x } X. ( 0 ... ( # ` x ) ) ) )
28 26 27 sylibr 
 |-  ( ph -> Rel U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) )
29 1stdm 
 |-  ( ( Rel U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) /\ b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( 1st ` b ) e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) )
30 28 29 sylan 
 |-  ( ( ph /\ b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( 1st ` b ) e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) )
31 lencl 
 |-  ( x e. Word A -> ( # ` x ) e. NN0 )
32 31 adantl 
 |-  ( ( ph /\ x e. Word A ) -> ( # ` x ) e. NN0 )
33 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
34 32 33 eleqtrdi 
 |-  ( ( ph /\ x e. Word A ) -> ( # ` x ) e. ( ZZ>= ` 0 ) )
35 fzn0 
 |-  ( ( 0 ... ( # ` x ) ) =/= (/) <-> ( # ` x ) e. ( ZZ>= ` 0 ) )
36 34 35 sylibr 
 |-  ( ( ph /\ x e. Word A ) -> ( 0 ... ( # ` x ) ) =/= (/) )
37 36 dmdju 
 |-  ( ph -> dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) = Word A )
38 37 adantr 
 |-  ( ( ph /\ b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) = Word A )
39 30 38 eleqtrd 
 |-  ( ( ph /\ b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( 1st ` b ) e. Word A )
40 pfxcl 
 |-  ( ( 1st ` b ) e. Word A -> ( ( 1st ` b ) prefix ( 2nd ` b ) ) e. Word A )
41 39 40 syl 
 |-  ( ( ph /\ b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( ( 1st ` b ) prefix ( 2nd ` b ) ) e. Word A )
42 swrdcl 
 |-  ( ( 1st ` b ) e. Word A -> ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) e. Word A )
43 39 42 syl 
 |-  ( ( ph /\ b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) e. Word A )
44 41 43 opelxpd 
 |-  ( ( ph /\ b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. e. ( Word A X. Word A ) )
45 sneq 
 |-  ( w = x -> { w } = { x } )
46 fveq2 
 |-  ( w = x -> ( # ` w ) = ( # ` x ) )
47 46 oveq2d 
 |-  ( w = x -> ( 0 ... ( # ` w ) ) = ( 0 ... ( # ` x ) ) )
48 45 47 xpeq12d 
 |-  ( w = x -> ( { w } X. ( 0 ... ( # ` w ) ) ) = ( { x } X. ( 0 ... ( # ` x ) ) ) )
49 48 cbviunv 
 |-  U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) = U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) )
50 49 mpteq1i 
 |-  ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) = ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. )
51 50 a1i 
 |-  ( ph -> ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) = ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) )
52 3 feqmptd 
 |-  ( ph -> F = ( a e. ( Word A X. Word A ) |-> ( F ` a ) ) )
53 fveq2 
 |-  ( a = <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. -> ( F ` a ) = ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) )
54 44 51 52 53 fmptco 
 |-  ( ph -> ( F o. ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) = ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) )
55 54 oveq2d 
 |-  ( ph -> ( M gsum ( F o. ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ) = ( M gsum ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ) )
56 nfv 
 |-  F/ w ph
57 3 44 cofmpt 
 |-  ( ph -> ( F o. ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) = ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) )
58 20 51 eqtr2d 
 |-  ( ph -> ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) = `' ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) )
59 49 eqcomi 
 |-  U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) = U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) )
60 59 a1i 
 |-  ( ph -> U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) = U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) )
61 eqidd 
 |-  ( ph -> ( Word A X. Word A ) = ( Word A X. Word A ) )
62 58 60 61 f1oeq123d 
 |-  ( ph -> ( ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) : U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) -1-1-onto-> ( Word A X. Word A ) <-> `' ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) : U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) -1-1-onto-> ( Word A X. Word A ) ) )
63 19 62 mpbird 
 |-  ( ph -> ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) : U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) -1-1-onto-> ( Word A X. Word A ) )
64 f1of1 
 |-  ( ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) : U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) -1-1-onto-> ( Word A X. Word A ) -> ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) : U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) -1-1-> ( Word A X. Word A ) )
65 63 64 syl 
 |-  ( ph -> ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) : U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) -1-1-> ( Word A X. Word A ) )
66 2 fvexi 
 |-  Z e. _V
67 66 a1i 
 |-  ( ph -> Z e. _V )
68 3 12 fexd 
 |-  ( ph -> F e. _V )
69 4 65 67 68 fsuppco 
 |-  ( ph -> ( F o. ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) finSupp Z )
70 57 69 eqbrtrrd 
 |-  ( ph -> ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) finSupp Z )
71 3 adantr 
 |-  ( ( ph /\ b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> F : ( Word A X. Word A ) --> B )
72 71 44 ffvelcdmd 
 |-  ( ( ph /\ b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) e. B )
73 72 fmpttd 
 |-  ( ph -> ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) : U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) --> B )
74 vsnex 
 |-  { x } e. _V
75 ovex 
 |-  ( 0 ... ( # ` x ) ) e. _V
76 74 75 xpex 
 |-  ( { x } X. ( 0 ... ( # ` x ) ) ) e. _V
77 76 a1i 
 |-  ( ( ph /\ x e. Word A ) -> ( { x } X. ( 0 ... ( # ` x ) ) ) e. _V )
78 77 ralrimiva 
 |-  ( ph -> A. x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) e. _V )
79 iunexg 
 |-  ( ( Word A e. _V /\ A. x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) e. _V ) -> U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) e. _V )
80 11 78 79 syl2anc 
 |-  ( ph -> U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) e. _V )
81 56 1 2 28 70 5 73 80 gsumfs2d 
 |-  ( ph -> ( M gsum ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ) = ( M gsum ( w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ` <. w , j >. ) ) ) ) ) )
82 23 55 81 3eqtrd 
 |-  ( ph -> ( M gsum F ) = ( M gsum ( w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ` <. w , j >. ) ) ) ) ) )
83 eqid 
 |-  ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) = ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) )
84 vex 
 |-  w e. _V
85 vex 
 |-  j e. _V
86 84 85 op1std 
 |-  ( b = <. w , j >. -> ( 1st ` b ) = w )
87 84 85 op2ndd 
 |-  ( b = <. w , j >. -> ( 2nd ` b ) = j )
88 86 87 oveq12d 
 |-  ( b = <. w , j >. -> ( ( 1st ` b ) prefix ( 2nd ` b ) ) = ( w prefix j ) )
89 86 fveq2d 
 |-  ( b = <. w , j >. -> ( # ` ( 1st ` b ) ) = ( # ` w ) )
90 87 89 opeq12d 
 |-  ( b = <. w , j >. -> <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. = <. j , ( # ` w ) >. )
91 86 90 oveq12d 
 |-  ( b = <. w , j >. -> ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) = ( w substr <. j , ( # ` w ) >. ) )
92 88 91 opeq12d 
 |-  ( b = <. w , j >. -> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. = <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. )
93 92 fveq2d 
 |-  ( b = <. w , j >. -> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) = ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) )
94 37 eleq2d 
 |-  ( ph -> ( w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) <-> w e. Word A ) )
95 94 biimpa 
 |-  ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> w e. Word A )
96 95 adantr 
 |-  ( ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) /\ j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) ) -> w e. Word A )
97 ovexd 
 |-  ( ( ph /\ x e. Word A ) -> ( 0 ... ( # ` x ) ) e. _V )
98 nfcv 
 |-  F/_ x ( 0 ... ( # ` w ) )
99 fveq2 
 |-  ( x = w -> ( # ` x ) = ( # ` w ) )
100 99 oveq2d 
 |-  ( x = w -> ( 0 ... ( # ` x ) ) = ( 0 ... ( # ` w ) ) )
101 11 97 98 100 iunsnima2 
 |-  ( ( ph /\ w e. Word A ) -> ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) = ( 0 ... ( # ` w ) ) )
102 95 101 syldan 
 |-  ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) = ( 0 ... ( # ` w ) ) )
103 102 eleq2d 
 |-  ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) <-> j e. ( 0 ... ( # ` w ) ) ) )
104 103 biimpa 
 |-  ( ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) /\ j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) ) -> j e. ( 0 ... ( # ` w ) ) )
105 100 opeliunxp2 
 |-  ( <. w , j >. e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) <-> ( w e. Word A /\ j e. ( 0 ... ( # ` w ) ) ) )
106 96 104 105 sylanbrc 
 |-  ( ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) /\ j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) ) -> <. w , j >. e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) )
107 fvexd 
 |-  ( ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) /\ j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) ) -> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) e. _V )
108 83 93 106 107 fvmptd3 
 |-  ( ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) /\ j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) ) -> ( ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ` <. w , j >. ) = ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) )
109 108 mpteq2dva 
 |-  ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ` <. w , j >. ) ) = ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) )
110 109 oveq2d 
 |-  ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ` <. w , j >. ) ) ) = ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) )
111 110 mpteq2dva 
 |-  ( ph -> ( w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ` <. w , j >. ) ) ) ) = ( w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) ) )
112 111 oveq2d 
 |-  ( ph -> ( M gsum ( w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( ( b e. U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( F ` <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) ` <. w , j >. ) ) ) ) ) = ( M gsum ( w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) ) ) )
113 102 mpteq1d 
 |-  ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) = ( j e. ( 0 ... ( # ` w ) ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) )
114 113 oveq2d 
 |-  ( ( ph /\ w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) ) -> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) = ( M gsum ( j e. ( 0 ... ( # ` w ) ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) )
115 37 114 mpteq12dva 
 |-  ( ph -> ( w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) ) = ( w e. Word A |-> ( M gsum ( j e. ( 0 ... ( # ` w ) ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) ) )
116 115 oveq2d 
 |-  ( ph -> ( M gsum ( w e. dom U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) |-> ( M gsum ( j e. ( U_ x e. Word A ( { x } X. ( 0 ... ( # ` x ) ) ) " { w } ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) ) ) = ( M gsum ( w e. Word A |-> ( M gsum ( j e. ( 0 ... ( # ` w ) ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) ) ) )
117 82 112 116 3eqtrd 
 |-  ( ph -> ( M gsum F ) = ( M gsum ( w e. Word A |-> ( M gsum ( j e. ( 0 ... ( # ` w ) ) |-> ( F ` <. ( w prefix j ) , ( w substr <. j , ( # ` w ) >. ) >. ) ) ) ) ) )