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 ) >. ) >. ) ) ) ) ) )