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

Metamath Proof Explorer

Theorem gsumwrd2dccat

Proof