elrgspnlem2

	Ref	Expression
Hypotheses	elrgspn.b	$⊢ B = {Base}_{R}$
	elrgspn.m	$⊢ M = {mulGrp}_{R}$
	elrgspn.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	elrgspn.n	$⊢ N = RingSpan (R)$
	elrgspn.f	$⊢ F = \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
	elrgspn.r	$⊢ φ \to R \in Ring$
	elrgspn.a	$⊢ φ \to A \subseteq B$
	elrgspnlem1.1	$⊢ S = ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
Assertion	elrgspnlem2	$⊢ φ \to S \in SubRing (R)$

Proof

Step	Hyp	Ref	Expression
1		elrgspn.b	$⊢ B = {Base}_{R}$
2		elrgspn.m	$⊢ M = {mulGrp}_{R}$
3		elrgspn.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		elrgspn.n	$⊢ N = RingSpan (R)$
5		elrgspn.f	$⊢ F = \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
6		elrgspn.r	$⊢ φ \to R \in Ring$
7		elrgspn.a	$⊢ φ \to A \subseteq B$
8		elrgspnlem1.1	$⊢ S = ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
9	1 2 3 4 5 6 7 8	elrgspnlem1	$⊢ φ \to S \in SubGrp (R)$
10		eqeq2	$⊢ 1_{R} = if (w = \emptyset, 1_{R}, 0_{R}) \to ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 1_{R} \leftrightarrow (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = if (w = \emptyset, 1_{R}, 0_{R}))$
11		eqeq2	$⊢ 0_{R} = if (w = \emptyset, 1_{R}, 0_{R}) \to ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R} \leftrightarrow (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = if (w = \emptyset, 1_{R}, 0_{R}))$
12		simpr	$⊢ ((φ \land w \in Word A) \land w = \emptyset) \to w = \emptyset$
13	12	fveq2d	$⊢ ((φ \land w \in Word A) \land w = \emptyset) \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) = (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (\emptyset)$
14		eqid	$⊢ (v \in Word A ⟼ if (v = \emptyset, 1, 0)) = (v \in Word A ⟼ if (v = \emptyset, 1, 0))$
15		simpr	$⊢ (φ \land v = \emptyset) \to v = \emptyset$
16	15	iftrued	$⊢ (φ \land v = \emptyset) \to if (v = \emptyset, 1, 0) = 1$
17		wrd0	$⊢ \emptyset \in Word A$
18	17	a1i	$⊢ φ \to \emptyset \in Word A$
19		1zzd	$⊢ φ \to 1 \in ℤ$
20	14 16 18 19	fvmptd2	$⊢ φ \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (\emptyset) = 1$
21	20	ad2antrr	$⊢ ((φ \land w \in Word A) \land w = \emptyset) \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (\emptyset) = 1$
22	13 21	eqtrd	$⊢ ((φ \land w \in Word A) \land w = \emptyset) \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) = 1$
23	12	oveq2d	$⊢ ((φ \land w \in Word A) \land w = \emptyset) \to \sum_{M} w = \sum_{M} \emptyset$
24		eqid	$⊢ 1_{R} = 1_{R}$
25	2 24	ringidval	$⊢ 1_{R} = 0_{M}$
26	25	gsum0	$⊢ \sum_{M} \emptyset = 1_{R}$
27	23 26	eqtrdi	$⊢ ((φ \land w \in Word A) \land w = \emptyset) \to \sum_{M} w = 1_{R}$
28	22 27	oveq12d	$⊢ ((φ \land w \in Word A) \land w = \emptyset) \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 1 \underset{˙}{\cdot} 1_{R}$
29	1 24	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
30	6 29	syl	$⊢ φ \to 1_{R} \in B$
31	1 3	mulg1	$⊢ 1_{R} \in B \to 1 \underset{˙}{\cdot} 1_{R} = 1_{R}$
32	30 31	syl	$⊢ φ \to 1 \underset{˙}{\cdot} 1_{R} = 1_{R}$
33	32	ad2antrr	$⊢ ((φ \land w \in Word A) \land w = \emptyset) \to 1 \underset{˙}{\cdot} 1_{R} = 1_{R}$
34	28 33	eqtrd	$⊢ ((φ \land w \in Word A) \land w = \emptyset) \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 1_{R}$
35		eqeq1	$⊢ v = w \to (v = \emptyset \leftrightarrow w = \emptyset)$
36	35	notbid	$⊢ v = w \to (\neg v = \emptyset \leftrightarrow \neg w = \emptyset)$
37	36	biimparc	$⊢ (\neg w = \emptyset \land v = w) \to \neg v = \emptyset$
38	37	adantll	$⊢ (((φ \land w \in Word A) \land \neg w = \emptyset) \land v = w) \to \neg v = \emptyset$
39	38	iffalsed	$⊢ (((φ \land w \in Word A) \land \neg w = \emptyset) \land v = w) \to if (v = \emptyset, 1, 0) = 0$
40		simplr	$⊢ ((φ \land w \in Word A) \land \neg w = \emptyset) \to w \in Word A$
41		0zd	$⊢ ((φ \land w \in Word A) \land \neg w = \emptyset) \to 0 \in ℤ$
42	14 39 40 41	fvmptd2	$⊢ ((φ \land w \in Word A) \land \neg w = \emptyset) \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) = 0$
43	42	oveq1d	$⊢ ((φ \land w \in Word A) \land \neg w = \emptyset) \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0 \underset{˙}{\cdot} (\sum_{M}, w)$
44	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
45	6 44	syl	$⊢ φ \to M \in Mnd$
46		sswrd	$⊢ A \subseteq B \to Word A \subseteq Word B$
47	7 46	syl	$⊢ φ \to Word A \subseteq Word B$
48	47	sselda	$⊢ (φ \land w \in Word A) \to w \in Word B$
49	2 1	mgpbas	$⊢ B = {Base}_{M}$
50	49	gsumwcl	$⊢ (M \in Mnd \land w \in Word B) \to \sum_{M} w \in B$
51	45 48 50	syl2an2r	$⊢ (φ \land w \in Word A) \to \sum_{M} w \in B$
52		eqid	$⊢ 0_{R} = 0_{R}$
53	1 52 3	mulg0	$⊢ \sum_{M} w \in B \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
54	51 53	syl	$⊢ (φ \land w \in Word A) \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
55	54	adantr	$⊢ ((φ \land w \in Word A) \land \neg w = \emptyset) \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
56	43 55	eqtrd	$⊢ ((φ \land w \in Word A) \land \neg w = \emptyset) \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
57	10 11 34 56	ifbothda	$⊢ (φ \land w \in Word A) \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w) = if (w = \emptyset, 1_{R}, 0_{R})$
58	57	mpteq2dva	$⊢ φ \to (w \in Word A ⟼ (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ if (w = \emptyset, 1_{R}, 0_{R}))$
59	58	oveq2d	$⊢ φ \to \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} if (w = \emptyset, 1_{R}, 0_{R})$
60	6	ringcmnd	$⊢ φ \to R \in CMnd$
61	60	cmnmndd	$⊢ φ \to R \in Mnd$
62	1	fvexi	$⊢ B \in V$
63	62	a1i	$⊢ φ \to B \in V$
64	63 7	ssexd	$⊢ φ \to A \in V$
65		wrdexg	$⊢ A \in V \to Word A \in V$
66	64 65	syl	$⊢ φ \to Word A \in V$
67		eqid	$⊢ (w \in Word A ⟼ if (w = \emptyset, 1_{R}, 0_{R})) = (w \in Word A ⟼ if (w = \emptyset, 1_{R}, 0_{R}))$
68	30 1	eleqtrdi	$⊢ φ \to 1_{R} \in {Base}_{R}$
69	52 61 66 18 67 68	gsummptif1n0	$⊢ φ \to \underset{w \in Word A}{\sum_{R}} if (w = \emptyset, 1_{R}, 0_{R}) = 1_{R}$
70	59 69	eqtrd	$⊢ φ \to \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = 1_{R}$
71		eqid	$⊢ (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) = (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
72		fveq1	$⊢ g = (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \to g (w) = (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w)$
73	72	oveq1d	$⊢ g = (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) = (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)$
74	73	mpteq2dv	$⊢ g = (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ (v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
75	74	oveq2d	$⊢ g = (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
76	75	eqeq2d	$⊢ g = (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \to (\underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \leftrightarrow \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
77		breq1	$⊢ f = (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} ((v \in Word A ⟼ if (v = \emptyset, 1, 0))))$
78		zex	$⊢ ℤ \in V$
79	78	a1i	$⊢ φ \to ℤ \in V$
80		1zzd	$⊢ ((φ \land v \in Word A) \land v = \emptyset) \to 1 \in ℤ$
81		0zd	$⊢ ((φ \land v \in Word A) \land \neg v = \emptyset) \to 0 \in ℤ$
82	80 81	ifclda	$⊢ (φ \land v \in Word A) \to if (v = \emptyset, 1, 0) \in ℤ$
83	82	fmpttd	$⊢ φ \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) : Word A ⟶ ℤ$
84	79 66 83	elmapdd	$⊢ φ \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \in (ℤ^{Word A})$
85	66	mptexd	$⊢ φ \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \in V$
86	83	ffund	$⊢ φ \to Fun (v \in Word A ⟼ if (v = \emptyset, 1, 0))$
87		0zd	$⊢ φ \to 0 \in ℤ$
88		snfi	$⊢ \{\emptyset\} \in Fin$
89	88	a1i	$⊢ φ \to \{\emptyset\} \in Fin$
90		eldifsni	$⊢ v \in (Word A ∖ \{\emptyset\}) \to v \neq \emptyset$
91	90	adantl	$⊢ (φ \land v \in (Word A ∖ \{\emptyset\})) \to v \neq \emptyset$
92	91	neneqd	$⊢ (φ \land v \in (Word A ∖ \{\emptyset\})) \to \neg v = \emptyset$
93	92	iffalsed	$⊢ (φ \land v \in (Word A ∖ \{\emptyset\})) \to if (v = \emptyset, 1, 0) = 0$
94	93 66	suppss2	$⊢ φ \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) supp 0 \subseteq \{\emptyset\}$
95		suppssfifsupp	$⊢ (((v \in Word A ⟼ if (v = \emptyset, 1, 0)) \in V \land Fun (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \land 0 \in ℤ) \land (\{\emptyset\} \in Fin \land (v \in Word A ⟼ if (v = \emptyset, 1, 0)) supp 0 \subseteq \{\emptyset\})) \to {finSupp}_{0} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)))$
96	85 86 87 89 94 95	syl32anc	$⊢ φ \to {finSupp}_{0} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)))$
97	77 84 96	elrabd	$⊢ φ \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \in \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
98	97 5	eleqtrrdi	$⊢ φ \to (v \in Word A ⟼ if (v = \emptyset, 1, 0)) \in F$
99		eqidd	$⊢ φ \to \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
100	76 98 99	rspcedvdw	$⊢ φ \to \exists g \in F \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
101		ovexd	$⊢ φ \to \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in V$
102	71 100 101	elrnmptd	$⊢ φ \to \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
103	102 8	eleqtrrdi	$⊢ φ \to \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ if (v = \emptyset, 1, 0)) (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in S$
104	70 103	eqeltrrd	$⊢ φ \to 1_{R} \in S$
105		simpllr	$⊢ ((((((φ \land x \in S) \land y \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \land i \in F) \land y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
106		simpr	$⊢ ((((((φ \land x \in S) \land y \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \land i \in F) \land y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
107	105 106	oveq12d	$⊢ ((((((φ \land x \in S) \land y \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \land i \in F) \land y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to x \cdot_{R} y = (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \cdot_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
108		eqid	$⊢ \cdot_{R} = \cdot_{R}$
109	66	ad2antrr	$⊢ ((φ \land g \in F) \land i \in F) \to Word A \in V$
110	6	ad2antrr	$⊢ ((φ \land g \in F) \land i \in F) \to R \in Ring$
111	6	ringgrpd	$⊢ φ \to R \in Grp$
112	111	ad2antrr	$⊢ ((φ \land g \in F) \land w \in Word A) \to R \in Grp$
113	5	ssrab3	$⊢ F \subseteq ℤ^{Word A}$
114	113	a1i	$⊢ φ \to F \subseteq ℤ^{Word A}$
115	114	sselda	$⊢ (φ \land g \in F) \to g \in (ℤ^{Word A})$
116	79 66	elmapd	$⊢ φ \to (g \in (ℤ^{Word A}) \leftrightarrow g : Word A ⟶ ℤ)$
117	116	adantr	$⊢ (φ \land g \in F) \to (g \in (ℤ^{Word A}) \leftrightarrow g : Word A ⟶ ℤ)$
118	115 117	mpbid	$⊢ (φ \land g \in F) \to g : Word A ⟶ ℤ$
119	118	ffvelcdmda	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) \in ℤ$
120	51	adantlr	$⊢ ((φ \land g \in F) \land w \in Word A) \to \sum_{M} w \in B$
121	1 3 112 119 120	mulgcld	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
122	121	adantlr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
123	122	ralrimiva	$⊢ ((φ \land g \in F) \land i \in F) \to \forall w \in Word A g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
124		fveq2	$⊢ u = w \to g (u) = g (w)$
125		oveq2	$⊢ u = w \to \sum_{M} u = \sum_{M} w$
126	124 125	oveq12d	$⊢ u = w \to g (u) \underset{˙}{\cdot} (\sum_{M}, u) = g (w) \underset{˙}{\cdot} (\sum_{M}, w)$
127	126	eleq1d	$⊢ u = w \to (g (u) \underset{˙}{\cdot} (\sum_{M}, u) \in B \leftrightarrow g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B)$
128	127	cbvralvw	$⊢ \forall u \in Word A g (u) \underset{˙}{\cdot} (\sum_{M}, u) \in B \leftrightarrow \forall w \in Word A g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
129	123 128	sylibr	$⊢ ((φ \land g \in F) \land i \in F) \to \forall u \in Word A g (u) \underset{˙}{\cdot} (\sum_{M}, u) \in B$
130	129	r19.21bi	$⊢ (((φ \land g \in F) \land i \in F) \land u \in Word A) \to g (u) \underset{˙}{\cdot} (\sum_{M}, u) \in B$
131	111	ad2antrr	$⊢ ((φ \land i \in F) \land w \in Word A) \to R \in Grp$
132		breq1	$⊢ f = i \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} (i))$
133	132 5	elrab2	$⊢ i \in F \leftrightarrow (i \in (ℤ^{Word A}) \land {finSupp}_{0} (i))$
134	133	simplbi	$⊢ i \in F \to i \in (ℤ^{Word A})$
135	134	adantl	$⊢ (φ \land i \in F) \to i \in (ℤ^{Word A})$
136	79 66	elmapd	$⊢ φ \to (i \in (ℤ^{Word A}) \leftrightarrow i : Word A ⟶ ℤ)$
137	136	adantr	$⊢ (φ \land i \in F) \to (i \in (ℤ^{Word A}) \leftrightarrow i : Word A ⟶ ℤ)$
138	135 137	mpbid	$⊢ (φ \land i \in F) \to i : Word A ⟶ ℤ$
139	138	ffvelcdmda	$⊢ ((φ \land i \in F) \land w \in Word A) \to i (w) \in ℤ$
140	51	adantlr	$⊢ ((φ \land i \in F) \land w \in Word A) \to \sum_{M} w \in B$
141	1 3 131 139 140	mulgcld	$⊢ ((φ \land i \in F) \land w \in Word A) \to i (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
142	141	adantllr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to i (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
143	142	ralrimiva	$⊢ ((φ \land g \in F) \land i \in F) \to \forall w \in Word A i (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
144		fveq2	$⊢ v = w \to i (v) = i (w)$
145		oveq2	$⊢ v = w \to \sum_{M} v = \sum_{M} w$
146	144 145	oveq12d	$⊢ v = w \to i (v) \underset{˙}{\cdot} (\sum_{M}, v) = i (w) \underset{˙}{\cdot} (\sum_{M}, w)$
147	146	eleq1d	$⊢ v = w \to (i (v) \underset{˙}{\cdot} (\sum_{M}, v) \in B \leftrightarrow i (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B)$
148	147	cbvralvw	$⊢ \forall v \in Word A i (v) \underset{˙}{\cdot} (\sum_{M}, v) \in B \leftrightarrow \forall w \in Word A i (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
149	143 148	sylibr	$⊢ ((φ \land g \in F) \land i \in F) \to \forall v \in Word A i (v) \underset{˙}{\cdot} (\sum_{M}, v) \in B$
150	149	r19.21bi	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to i (v) \underset{˙}{\cdot} (\sum_{M}, v) \in B$
151	126	cbvmptv	$⊢ (u \in Word A ⟼ g (u) \underset{˙}{\cdot} (\sum_{M}, u)) = (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
152		fvexd	$⊢ (φ \land g \in F) \to 0_{R} \in V$
153		0zd	$⊢ (φ \land g \in F) \to 0 \in ℤ$
154	66	adantr	$⊢ (φ \land g \in F) \to Word A \in V$
155		ssidd	$⊢ (φ \land g \in F) \to Word A \subseteq Word A$
156		breq1	$⊢ f = g \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} (g))$
157	156 5	elrab2	$⊢ g \in F \leftrightarrow (g \in (ℤ^{Word A}) \land {finSupp}_{0} (g))$
158	157	simprbi	$⊢ g \in F \to {finSupp}_{0} (g)$
159	158	adantl	$⊢ (φ \land g \in F) \to {finSupp}_{0} (g)$
160	1 52 3	mulg0	$⊢ y \in B \to 0 \underset{˙}{\cdot} y = 0_{R}$
161	160	adantl	$⊢ ((φ \land g \in F) \land y \in B) \to 0 \underset{˙}{\cdot} y = 0_{R}$
162	152 153 154 155 120 118 159 161	fisuppov1	$⊢ (φ \land g \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
163	162	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
164	151 163	eqbrtrid	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{R}} ((u \in Word A ⟼ g (u) \underset{˙}{\cdot} (\sum_{M}, u)))$
165	146	cbvmptv	$⊢ (v \in Word A ⟼ i (v) \underset{˙}{\cdot} (\sum_{M}, v)) = (w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
166	162	ralrimiva	$⊢ φ \to \forall g \in F {finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
167		fveq1	$⊢ g = i \to g (w) = i (w)$
168	167	oveq1d	$⊢ g = i \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) = i (w) \underset{˙}{\cdot} (\sum_{M}, w)$
169	168	mpteq2dv	$⊢ g = i \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
170	169	breq1d	$⊢ g = i \to ({finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \leftrightarrow {finSupp}_{0_{R}} ((w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w))))$
171	170	cbvralvw	$⊢ \forall g \in F {finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \leftrightarrow \forall i \in F {finSupp}_{0_{R}} ((w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
172	166 171	sylib	$⊢ φ \to \forall i \in F {finSupp}_{0_{R}} ((w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
173	172	r19.21bi	$⊢ (φ \land i \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
174	173	adantlr	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
175	165 174	eqbrtrid	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{R}} ((v \in Word A ⟼ i (v) \underset{˙}{\cdot} (\sum_{M}, v)))$
176	1 108 52 109 109 110 130 150 164 175	gsumdixp	$⊢ ((φ \land g \in F) \land i \in F) \to (\underset{u \in Word A}{\sum_{R}}, (g (u) \underset{˙}{\cdot} (\sum_{M}, u))) \cdot_{R} (\underset{v \in Word A}{\sum_{R}}, (i (v) \underset{˙}{\cdot} (\sum_{M}, v))) = \sum_{R} (u \in Word A, v \in Word A ⟼ (g (u) \underset{˙}{\cdot} (\sum_{M}, u)) \cdot_{R} (i (v) \underset{˙}{\cdot} (\sum_{M}, v)))$
177	151	oveq2i	$⊢ \underset{u \in Word A}{\sum_{R}} (g (u) \underset{˙}{\cdot} (\sum_{M}, u)) = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
178	165	oveq2i	$⊢ \underset{v \in Word A}{\sum_{R}} (i (v) \underset{˙}{\cdot} (\sum_{M}, v)) = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
179	177 178	oveq12i	$⊢ (\underset{u \in Word A}{\sum_{R}}, (g (u) \underset{˙}{\cdot} (\sum_{M}, u))) \cdot_{R} (\underset{v \in Word A}{\sum_{R}}, (i (v) \underset{˙}{\cdot} (\sum_{M}, v))) = (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \cdot_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
180	179	a1i	$⊢ ((φ \land g \in F) \land i \in F) \to (\underset{u \in Word A}{\sum_{R}}, (g (u) \underset{˙}{\cdot} (\sum_{M}, u))) \cdot_{R} (\underset{v \in Word A}{\sum_{R}}, (i (v) \underset{˙}{\cdot} (\sum_{M}, v))) = (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \cdot_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
181	110	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to R \in Ring$
182	122	adantr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
183	111	ad4antr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to R \in Grp$
184	138	adantlr	$⊢ ((φ \land g \in F) \land i \in F) \to i : Word A ⟶ ℤ$
185	184	ffvelcdmda	$⊢ (((φ \land g \in F) \land i \in F) \land f \in Word A) \to i (f) \in ℤ$
186	185	adantlr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to i (f) \in ℤ$
187	45	ad4antr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to M \in Mnd$
188	47	adantr	$⊢ (φ \land g \in F) \to Word A \subseteq Word B$
189	188	ad2antrr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to Word A \subseteq Word B$
190	189	sselda	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to f \in Word B$
191	49	gsumwcl	$⊢ (M \in Mnd \land f \in Word B) \to \sum_{M} f \in B$
192	187 190 191	syl2anc	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to \sum_{M} f \in B$
193	1 3 183 186 192	mulgcld	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to i (f) \underset{˙}{\cdot} (\sum_{M}, f) \in B$
194	1 108 181 182 193	ringcld	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) \in B$
195	194	anasss	$⊢ (((φ \land g \in F) \land i \in F) \land (w \in Word A \land f \in Word A)) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) \in B$
196	195	ralrimivva	$⊢ ((φ \land g \in F) \land i \in F) \to \forall w \in Word A \forall f \in Word A (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) \in B$
197		eqid	$⊢ (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) = (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)))$
198	197	fmpo	$⊢ \forall w \in Word A \forall f \in Word A (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) \in B \leftrightarrow (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) : Word A \times Word A ⟶ B$
199	196 198	sylib	$⊢ ((φ \land g \in F) \land i \in F) \to (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) : Word A \times Word A ⟶ B$
200		vex	$⊢ w \in V$
201		vex	$⊢ f \in V$
202	200 201	op1std	$⊢ a = ⟨w, f⟩ \to 1^{st} (a) = w$
203	202	fveq2d	$⊢ a = ⟨w, f⟩ \to g (1^{st} (a)) = g (w)$
204	202	oveq2d	$⊢ a = ⟨w, f⟩ \to \sum_{M} 1^{st} (a) = \sum_{M} w$
205	203 204	oveq12d	$⊢ a = ⟨w, f⟩ \to g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a)) = g (w) \underset{˙}{\cdot} (\sum_{M}, w)$
206	200 201	op2ndd	$⊢ a = ⟨w, f⟩ \to 2^{nd} (a) = f$
207	206	fveq2d	$⊢ a = ⟨w, f⟩ \to i (2^{nd} (a)) = i (f)$
208	206	oveq2d	$⊢ a = ⟨w, f⟩ \to \sum_{M} 2^{nd} (a) = \sum_{M} f$
209	207 208	oveq12d	$⊢ a = ⟨w, f⟩ \to i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)) = i (f) \underset{˙}{\cdot} (\sum_{M}, f)$
210	205 209	oveq12d	$⊢ a = ⟨w, f⟩ \to (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))) = (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))$
211	210	mpompt	$⊢ (a \in (Word A \times Word A) ⟼ (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)))) = (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)))$
212	66 66	xpexd	$⊢ φ \to Word A \times Word A \in V$
213	212	ad2antrr	$⊢ ((φ \land g \in F) \land i \in F) \to Word A \times Word A \in V$
214	213	mptexd	$⊢ ((φ \land g \in F) \land i \in F) \to (a \in (Word A \times Word A) ⟼ (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)))) \in V$
215		fvexd	$⊢ ((φ \land g \in F) \land i \in F) \to 0_{R} \in V$
216	110	adantr	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to R \in Ring$
217	111	ad3antrrr	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to R \in Grp$
218	118	ad2antrr	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to g : Word A ⟶ ℤ$
219		xp1st	$⊢ a \in (Word A \times Word A) \to 1^{st} (a) \in Word A$
220	219	adantl	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to 1^{st} (a) \in Word A$
221	218 220	ffvelcdmd	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to g (1^{st} (a)) \in ℤ$
222	216 44	syl	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to M \in Mnd$
223	188	ad2antrr	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to Word A \subseteq Word B$
224	223 220	sseldd	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to 1^{st} (a) \in Word B$
225	49	gsumwcl	$⊢ (M \in Mnd \land 1^{st} (a) \in Word B) \to \sum_{M} 1^{st} (a) \in B$
226	222 224 225	syl2anc	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to \sum_{M} 1^{st} (a) \in B$
227	1 3 217 221 226	mulgcld	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a)) \in B$
228	184	adantr	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to i : Word A ⟶ ℤ$
229		xp2nd	$⊢ a \in (Word A \times Word A) \to 2^{nd} (a) \in Word A$
230	229	adantl	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to 2^{nd} (a) \in Word A$
231	228 230	ffvelcdmd	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to i (2^{nd} (a)) \in ℤ$
232	223 230	sseldd	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to 2^{nd} (a) \in Word B$
233	49	gsumwcl	$⊢ (M \in Mnd \land 2^{nd} (a) \in Word B) \to \sum_{M} 2^{nd} (a) \in B$
234	222 232 233	syl2anc	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to \sum_{M} 2^{nd} (a) \in B$
235	1 3 217 231 234	mulgcld	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)) \in B$
236	1 108 216 227 235	ringcld	$⊢ (((φ \land g \in F) \land i \in F) \land a \in (Word A \times Word A)) \to (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))) \in B$
237	236	fmpttd	$⊢ ((φ \land g \in F) \land i \in F) \to (a \in (Word A \times Word A) ⟼ (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)))) : Word A \times Word A ⟶ B$
238	237	ffund	$⊢ ((φ \land g \in F) \land i \in F) \to Fun (a \in (Word A \times Word A) ⟼ (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))))$
239	159	fsuppimpd	$⊢ (φ \land g \in F) \to g supp 0 \in Fin$
240	133	simprbi	$⊢ i \in F \to {finSupp}_{0} (i)$
241	240	adantl	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0} (i)$
242	241	fsuppimpd	$⊢ ((φ \land g \in F) \land i \in F) \to i supp 0 \in Fin$
243		xpfi	$⊢ (g supp 0 \in Fin \land i supp 0 \in Fin) \to {supp}_{0} (g) \times {supp}_{0} (i) \in Fin$
244	239 242 243	syl2an2r	$⊢ ((φ \land g \in F) \land i \in F) \to {supp}_{0} (g) \times {supp}_{0} (i) \in Fin$
245	118	ffnd	$⊢ (φ \land g \in F) \to g Fn Word A$
246	245	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to g Fn Word A$
247	246	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to g Fn Word A$
248	109	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to Word A \in V$
249		0zd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to 0 \in ℤ$
250		xp1st	$⊢ a \in ((Word A ∖ {supp}_{0} (g)) \times Word A) \to 1^{st} (a) \in (Word A ∖ {supp}_{0} (g))$
251	250	adantl	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to 1^{st} (a) \in (Word A ∖ {supp}_{0} (g))$
252	247 248 249 251	fvdifsupp	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to g (1^{st} (a)) = 0$
253	252	oveq1d	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a)) = 0 \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))$
254	45	ad4antr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to M \in Mnd$
255	188	ad3antrrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to Word A \subseteq Word B$
256	251	eldifad	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to 1^{st} (a) \in Word A$
257	255 256	sseldd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to 1^{st} (a) \in Word B$
258	254 257 225	syl2anc	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to \sum_{M} 1^{st} (a) \in B$
259	1 52 3	mulg0	$⊢ \sum_{M} 1^{st} (a) \in B \to 0 \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a)) = 0_{R}$
260	258 259	syl	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to 0 \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a)) = 0_{R}$
261	253 260	eqtrd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a)) = 0_{R}$
262	261	oveq1d	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))) = 0_{R} \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)))$
263	110	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to R \in Ring$
264	111	ad4antr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to R \in Grp$
265	184	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to i : Word A ⟶ ℤ$
266		xp2nd	$⊢ a \in ((Word A ∖ {supp}_{0} (g)) \times Word A) \to 2^{nd} (a) \in Word A$
267	266	adantl	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to 2^{nd} (a) \in Word A$
268	265 267	ffvelcdmd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to i (2^{nd} (a)) \in ℤ$
269	255 267	sseldd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to 2^{nd} (a) \in Word B$
270	254 269 233	syl2anc	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to \sum_{M} 2^{nd} (a) \in B$
271	1 3 264 268 270	mulgcld	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)) \in B$
272	1 108 52 263 271	ringlzd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to 0_{R} \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))) = 0_{R}$
273	262 272	eqtrd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in ((Word A ∖ {supp}_{0} (g)) \times Word A)) \to (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))) = 0_{R}$
274	138	ffnd	$⊢ (φ \land i \in F) \to i Fn Word A$
275	274	adantlr	$⊢ ((φ \land g \in F) \land i \in F) \to i Fn Word A$
276	275	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to i Fn Word A$
277	109	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to Word A \in V$
278		0zd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to 0 \in ℤ$
279		xp2nd	$⊢ a \in (Word A \times (Word A ∖ {supp}_{0} (i))) \to 2^{nd} (a) \in (Word A ∖ {supp}_{0} (i))$
280	279	adantl	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to 2^{nd} (a) \in (Word A ∖ {supp}_{0} (i))$
281	276 277 278 280	fvdifsupp	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to i (2^{nd} (a)) = 0$
282	281	oveq1d	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)) = 0 \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))$
283	45	ad4antr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to M \in Mnd$
284	188	ad3antrrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to Word A \subseteq Word B$
285	280	eldifad	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to 2^{nd} (a) \in Word A$
286	284 285	sseldd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to 2^{nd} (a) \in Word B$
287	283 286 233	syl2anc	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to \sum_{M} 2^{nd} (a) \in B$
288	1 52 3	mulg0	$⊢ \sum_{M} 2^{nd} (a) \in B \to 0 \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)) = 0_{R}$
289	287 288	syl	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to 0 \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)) = 0_{R}$
290	282 289	eqtrd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)) = 0_{R}$
291	290	oveq2d	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))) = (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} 0_{R}$
292	110	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to R \in Ring$
293	111	ad4antr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to R \in Grp$
294	118	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to g : Word A ⟶ ℤ$
295	294	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to g : Word A ⟶ ℤ$
296		xp1st	$⊢ a \in (Word A \times (Word A ∖ {supp}_{0} (i))) \to 1^{st} (a) \in Word A$
297	296	adantl	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to 1^{st} (a) \in Word A$
298	295 297	ffvelcdmd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to g (1^{st} (a)) \in ℤ$
299	284 297	sseldd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to 1^{st} (a) \in Word B$
300	283 299 225	syl2anc	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to \sum_{M} 1^{st} (a) \in B$
301	1 3 293 298 300	mulgcld	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a)) \in B$
302	1 108 52 292 301	ringrzd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} 0_{R} = 0_{R}$
303	291 302	eqtrd	$⊢ ((((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \land a \in (Word A \times (Word A ∖ {supp}_{0} (i)))) \to (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))) = 0_{R}$
304		simpr	$⊢ (((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \to a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))$
305		difxp	$⊢ (Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)) = ((Word A ∖ {supp}_{0} (g)) \times Word A) \cup (Word A \times (Word A ∖ {supp}_{0} (i)))$
306	304 305	eleqtrdi	$⊢ (((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \to a \in (((Word A ∖ {supp}_{0} (g)) \times Word A) \cup (Word A \times (Word A ∖ {supp}_{0} (i))))$
307		elun	$⊢ a \in (((Word A ∖ {supp}_{0} (g)) \times Word A) \cup (Word A \times (Word A ∖ {supp}_{0} (i)))) \leftrightarrow (a \in ((Word A ∖ {supp}_{0} (g)) \times Word A) \lor a \in (Word A \times (Word A ∖ {supp}_{0} (i))))$
308	306 307	sylib	$⊢ (((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \to (a \in ((Word A ∖ {supp}_{0} (g)) \times Word A) \lor a \in (Word A \times (Word A ∖ {supp}_{0} (i))))$
309	273 303 308	mpjaodan	$⊢ (((φ \land g \in F) \land i \in F) \land a \in ((Word A \times Word A) ∖ ({supp}_{0} (g) \times {supp}_{0} (i)))) \to (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a))) = 0_{R}$
310	309 213	suppss2	$⊢ ((φ \land g \in F) \land i \in F) \to (a \in (Word A \times Word A) ⟼ (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)))) supp 0_{R} \subseteq {supp}_{0} (g) \times {supp}_{0} (i)$
311	244 310	ssfid	$⊢ ((φ \land g \in F) \land i \in F) \to (a \in (Word A \times Word A) ⟼ (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)))) supp 0_{R} \in Fin$
312	214 215 238 311	isfsuppd	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{R}} ((a \in (Word A \times Word A) ⟼ (g (1^{st} (a)) \underset{˙}{\cdot} (\sum_{M}, 1^{st} (a))) \cdot_{R} (i (2^{nd} (a)) \underset{˙}{\cdot} (\sum_{M}, 2^{nd} (a)))))$
313	211 312	eqbrtrrid	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{R}} ((w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))))$
314	60	ad2antrr	$⊢ ((φ \land g \in F) \land i \in F) \to R \in CMnd$
315	7	ad2antrr	$⊢ ((φ \land g \in F) \land i \in F) \to A \subseteq B$
316	1 52 199 313 314 315	gsumwrd2dccat	$⊢ ((φ \land g \in F) \land i \in F) \to \sum_{R} (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) = \underset{v \in Word A}{\sum_{R}} ({\sum_{R}}_{j = 0}^{\|v\|}, (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (⟨v prefix j, v substr ⟨j, \|v\|⟩⟩))$
317	126	oveq1d	$⊢ u = w \to (g (u) \underset{˙}{\cdot} (\sum_{M}, u)) \cdot_{R} (i (v) \underset{˙}{\cdot} (\sum_{M}, v)) = (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (v) \underset{˙}{\cdot} (\sum_{M}, v))$
318		fveq2	$⊢ v = f \to i (v) = i (f)$
319		oveq2	$⊢ v = f \to \sum_{M} v = \sum_{M} f$
320	318 319	oveq12d	$⊢ v = f \to i (v) \underset{˙}{\cdot} (\sum_{M}, v) = i (f) \underset{˙}{\cdot} (\sum_{M}, f)$
321	320	oveq2d	$⊢ v = f \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (v) \underset{˙}{\cdot} (\sum_{M}, v)) = (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))$
322	317 321	cbvmpov	$⊢ (u \in Word A, v \in Word A ⟼ (g (u) \underset{˙}{\cdot} (\sum_{M}, u)) \cdot_{R} (i (v) \underset{˙}{\cdot} (\sum_{M}, v))) = (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)))$
323	322	oveq2i	$⊢ \sum_{R} (u \in Word A, v \in Word A ⟼ (g (u) \underset{˙}{\cdot} (\sum_{M}, u)) \cdot_{R} (i (v) \underset{˙}{\cdot} (\sum_{M}, v))) = \sum_{R} (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)))$
324	323	a1i	$⊢ ((φ \land g \in F) \land i \in F) \to \sum_{R} (u \in Word A, v \in Word A ⟼ (g (u) \underset{˙}{\cdot} (\sum_{M}, u)) \cdot_{R} (i (v) \underset{˙}{\cdot} (\sum_{M}, v))) = \sum_{R} (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)))$
325		pfxcctswrd	$⊢ (v \in Word A \land j \in (0 \dots \|v\|)) \to (v prefix j) ++ (v substr ⟨j, \|v\|⟩) = v$
326	325	adantll	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to (v prefix j) ++ (v substr ⟨j, \|v\|⟩) = v$
327	326	oveq2d	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to \sum_{M} ((v prefix j) ++ (v substr ⟨j, \|v\|⟩)) = \sum_{M} v$
328	327	oveq2d	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩))) = g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, v)$
329	328	mpteq2dva	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to (j \in (0 \dots \|v\|) ⟼ g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩)))) = (j \in (0 \dots \|v\|) ⟼ g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, v))$
330	329	oveq2d	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to {\sum_{R}}_{j = 0}^{\|v\|} (g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩)))) = {\sum_{R}}_{j = 0}^{\|v\|} (g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, v))$
331		df-ov	$⊢ (v prefix j) (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (v substr ⟨j, \|v\|⟩) = (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (⟨v prefix j, v substr ⟨j, \|v\|⟩⟩)$
332	188	sselda	$⊢ ((φ \land g \in F) \land w \in Word A) \to w \in Word B$
333	332	ad4ant13	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to w \in Word B$
334	187 333 50	syl2anc	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to \sum_{M} w \in B$
335	1 3 108	mulgass3	$⊢ (R \in Ring \land (i (f) \in ℤ \land \sum_{M} w \in B \land \sum_{M} f \in B)) \to (\sum_{M}, w) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) = i (f) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (\sum_{M}, f))$
336	181 186 334 192 335	syl13anc	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to (\sum_{M}, w) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) = i (f) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (\sum_{M}, f))$
337	336	oveq2d	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to g (w) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) = g (w) \underset{˙}{\cdot} (i (f) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (\sum_{M}, f)))$
338	119	ad4ant13	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to g (w) \in ℤ$
339	1 3 108	mulgass2	$⊢ (R \in Ring \land (g (w) \in ℤ \land \sum_{M} w \in B \land i (f) \underset{˙}{\cdot} (\sum_{M}, f) \in B)) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) = g (w) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)))$
340	181 338 334 193 339	syl13anc	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) = g (w) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)))$
341	1 108 181 334 192	ringcld	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to (\sum_{M}, w) \cdot_{R} (\sum_{M}, f) \in B$
342	1 3	mulgass	$⊢ (R \in Grp \land (g (w) \in ℤ \land i (f) \in ℤ \land (\sum_{M}, w) \cdot_{R} (\sum_{M}, f) \in B)) \to g (w) i (f) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (\sum_{M}, f)) = g (w) \underset{˙}{\cdot} (i (f) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (\sum_{M}, f)))$
343	183 338 186 341 342	syl13anc	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to g (w) i (f) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (\sum_{M}, f)) = g (w) \underset{˙}{\cdot} (i (f) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (\sum_{M}, f)))$
344	337 340 343	3eqtr4d	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) = g (w) i (f) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (\sum_{M}, f))$
345	2 108	mgpplusg	$⊢ \cdot_{R} = +_{M}$
346	49 345	gsumccat	$⊢ (M \in Mnd \land w \in Word B \land f \in Word B) \to \sum_{M} (w ++ f) = (\sum_{M}, w) \cdot_{R} (\sum_{M}, f)$
347	187 333 190 346	syl3anc	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to \sum_{M} (w ++ f) = (\sum_{M}, w) \cdot_{R} (\sum_{M}, f)$
348	347	oveq2d	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to g (w) i (f) \underset{˙}{\cdot} (\sum_{M}, (w ++ f)) = g (w) i (f) \underset{˙}{\cdot} ((\sum_{M}, w) \cdot_{R} (\sum_{M}, f))$
349	344 348	eqtr4d	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in Word A) \land f \in Word A) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) = g (w) i (f) \underset{˙}{\cdot} (\sum_{M}, (w ++ f))$
350	349	adantllr	$⊢ (((((φ \land g \in F) \land i \in F) \land v \in Word A) \land w \in Word A) \land f \in Word A) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) = g (w) i (f) \underset{˙}{\cdot} (\sum_{M}, (w ++ f))$
351	350	adantllr	$⊢ ((((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \land w \in Word A) \land f \in Word A) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) = g (w) i (f) \underset{˙}{\cdot} (\sum_{M}, (w ++ f))$
352	351	3impa	$⊢ (((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \land w \in Word A \land f \in Word A) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f)) = g (w) i (f) \underset{˙}{\cdot} (\sum_{M}, (w ++ f))$
353	352	mpoeq3dva	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) = (w \in Word A, f \in Word A ⟼ g (w) i (f) \underset{˙}{\cdot} (\sum_{M}, (w ++ f)))$
354		fveq2	$⊢ w = v prefix j \to g (w) = g (v prefix j)$
355		fveq2	$⊢ f = v substr ⟨j, \|v\|⟩ \to i (f) = i (v substr ⟨j, \|v\|⟩)$
356	354 355	oveqan12d	$⊢ (w = v prefix j \land f = v substr ⟨j, \|v\|⟩) \to g (w) i (f) = g (v prefix j) i (v substr ⟨j, \|v\|⟩)$
357		oveq12	$⊢ (w = v prefix j \land f = v substr ⟨j, \|v\|⟩) \to w ++ f = (v prefix j) ++ (v substr ⟨j, \|v\|⟩)$
358	357	oveq2d	$⊢ (w = v prefix j \land f = v substr ⟨j, \|v\|⟩) \to \sum_{M} (w ++ f) = \sum_{M} ((v prefix j) ++ (v substr ⟨j, \|v\|⟩))$
359	356 358	oveq12d	$⊢ (w = v prefix j \land f = v substr ⟨j, \|v\|⟩) \to g (w) i (f) \underset{˙}{\cdot} (\sum_{M}, (w ++ f)) = g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩)))$
360	359	adantl	$⊢ (((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \land (w = v prefix j \land f = v substr ⟨j, \|v\|⟩)) \to g (w) i (f) \underset{˙}{\cdot} (\sum_{M}, (w ++ f)) = g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩)))$
361		pfxcl	$⊢ v \in Word A \to v prefix j \in Word A$
362	361	ad2antlr	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to v prefix j \in Word A$
363		swrdcl	$⊢ v \in Word A \to v substr ⟨j, \|v\|⟩ \in Word A$
364	363	ad2antlr	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to v substr ⟨j, \|v\|⟩ \in Word A$
365		ovexd	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩))) \in V$
366	353 360 362 364 365	ovmpod	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to (v prefix j) (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (v substr ⟨j, \|v\|⟩) = g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩)))$
367	331 366	eqtr3id	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (⟨v prefix j, v substr ⟨j, \|v\|⟩⟩) = g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩)))$
368	367	mpteq2dva	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to (j \in (0 \dots \|v\|) ⟼ (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (⟨v prefix j, v substr ⟨j, \|v\|⟩⟩)) = (j \in (0 \dots \|v\|) ⟼ g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩))))$
369	368	oveq2d	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to {\sum_{R}}_{j = 0}^{\|v\|} (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (⟨v prefix j, v substr ⟨j, \|v\|⟩⟩) = {\sum_{R}}_{j = 0}^{\|v\|} (g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, ((v prefix j) ++ (v substr ⟨j, \|v\|⟩))))$
370		eqid	$⊢ (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩))$
371		fveq2	$⊢ t = v \to \|t\| = \|v\|$
372	371	oveq2d	$⊢ t = v \to (0 \dots \|t\|) = (0 \dots \|v\|)$
373		fvoveq1	$⊢ t = v \to g (t prefix j) = g (v prefix j)$
374		id	$⊢ t = v \to t = v$
375	371	opeq2d	$⊢ t = v \to ⟨j, \|t\|⟩ = ⟨j, \|v\|⟩$
376	374 375	oveq12d	$⊢ t = v \to t substr ⟨j, \|t\|⟩ = v substr ⟨j, \|v\|⟩$
377	376	fveq2d	$⊢ t = v \to i (t substr ⟨j, \|t\|⟩) = i (v substr ⟨j, \|v\|⟩)$
378	373 377	oveq12d	$⊢ t = v \to g (t prefix j) i (t substr ⟨j, \|t\|⟩) = g (v prefix j) i (v substr ⟨j, \|v\|⟩)$
379	378	adantr	$⊢ (t = v \land j \in (0 \dots \|t\|)) \to g (t prefix j) i (t substr ⟨j, \|t\|⟩) = g (v prefix j) i (v substr ⟨j, \|v\|⟩)$
380	372 379	sumeq12dv	$⊢ t = v \to \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩) = \sum_{j = 0}^{\|v\|} g (v prefix j) i (v substr ⟨j, \|v\|⟩)$
381		simpr	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to v \in Word A$
382		fzfid	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to (0 \dots \|v\|) \in Fin$
383	294	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to g : Word A ⟶ ℤ$
384	383 362	ffvelcdmd	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to g (v prefix j) \in ℤ$
385	184	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to i : Word A ⟶ ℤ$
386	385 364	ffvelcdmd	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to i (v substr ⟨j, \|v\|⟩) \in ℤ$
387	384 386	zmulcld	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to g (v prefix j) i (v substr ⟨j, \|v\|⟩) \in ℤ$
388	387	zcnd	$⊢ ((((φ \land g \in F) \land i \in F) \land v \in Word A) \land j \in (0 \dots \|v\|)) \to g (v prefix j) i (v substr ⟨j, \|v\|⟩) \in ℂ$
389	382 388	fsumcl	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to \sum_{j = 0}^{\|v\|} g (v prefix j) i (v substr ⟨j, \|v\|⟩) \in ℂ$
390	370 380 381 389	fvmptd3	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) = \sum_{j = 0}^{\|v\|} g (v prefix j) i (v substr ⟨j, \|v\|⟩)$
391	390	oveq1d	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v) = \sum_{j = 0}^{\|v\|} g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, v)$
392	111	ad3antrrr	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to R \in Grp$
393	45	ad3antrrr	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to M \in Mnd$
394	315 46	syl	$⊢ ((φ \land g \in F) \land i \in F) \to Word A \subseteq Word B$
395	394	sselda	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to v \in Word B$
396	49	gsumwcl	$⊢ (M \in Mnd \land v \in Word B) \to \sum_{M} v \in B$
397	393 395 396	syl2anc	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to \sum_{M} v \in B$
398	1 3 392 382 397 387	gsummulgc2	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to {\sum_{R}}_{j = 0}^{\|v\|} (g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, v)) = \sum_{j = 0}^{\|v\|} g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, v)$
399	391 398	eqtr4d	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v) = {\sum_{R}}_{j = 0}^{\|v\|} (g (v prefix j) i (v substr ⟨j, \|v\|⟩) \underset{˙}{\cdot} (\sum_{M}, v))$
400	330 369 399	3eqtr4rd	$⊢ (((φ \land g \in F) \land i \in F) \land v \in Word A) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v) = {\sum_{R}}_{j = 0}^{\|v\|} (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (⟨v prefix j, v substr ⟨j, \|v\|⟩⟩)$
401	400	mpteq2dva	$⊢ ((φ \land g \in F) \land i \in F) \to (v \in Word A ⟼ (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) = (v \in Word A ⟼ {\sum_{R}}_{j = 0}^{\|v\|} (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (⟨v prefix j, v substr ⟨j, \|v\|⟩⟩))$
402	401	oveq2d	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) = \underset{v \in Word A}{\sum_{R}} ({\sum_{R}}_{j = 0}^{\|v\|}, (w \in Word A, f \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \cdot_{R} (i (f) \underset{˙}{\cdot} (\sum_{M}, f))) (⟨v prefix j, v substr ⟨j, \|v\|⟩⟩))$
403	316 324 402	3eqtr4d	$⊢ ((φ \land g \in F) \land i \in F) \to \sum_{R} (u \in Word A, v \in Word A ⟼ (g (u) \underset{˙}{\cdot} (\sum_{M}, u)) \cdot_{R} (i (v) \underset{˙}{\cdot} (\sum_{M}, v))) = \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v))$
404	176 180 403	3eqtr3d	$⊢ ((φ \land g \in F) \land i \in F) \to (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \cdot_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) = \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v))$
405		fveq1	$⊢ g = h \to g (w) = h (w)$
406	405	oveq1d	$⊢ g = h \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) = h (w) \underset{˙}{\cdot} (\sum_{M}, w)$
407	406	mpteq2dv	$⊢ g = h \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ h (w) \underset{˙}{\cdot} (\sum_{M}, w))$
408	407	oveq2d	$⊢ g = h \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w))$
409	408	cbvmptv	$⊢ (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) = (h \in F ⟼ \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
410		fveq1	$⊢ h = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) \to h (w) = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w)$
411	410	oveq1d	$⊢ h = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) \to h (w) \underset{˙}{\cdot} (\sum_{M}, w) = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w) \underset{˙}{\cdot} (\sum_{M}, w)$
412	411	mpteq2dv	$⊢ h = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) \to (w \in Word A ⟼ h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
413	412	oveq2d	$⊢ h = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) \to \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
414	413	eqeq2d	$⊢ h = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) \to (\underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) = \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)) \leftrightarrow \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) = \underset{w \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
415		breq1	$⊢ f = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩))))$
416	78	a1i	$⊢ ((φ \land g \in F) \land i \in F) \to ℤ \in V$
417		fzfid	$⊢ (((φ \land g \in F) \land i \in F) \land t \in Word A) \to (0 \dots \|t\|) \in Fin$
418	294	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land t \in Word A) \land j \in (0 \dots \|t\|)) \to g : Word A ⟶ ℤ$
419		pfxcl	$⊢ t \in Word A \to t prefix j \in Word A$
420	419	ad2antlr	$⊢ ((((φ \land g \in F) \land i \in F) \land t \in Word A) \land j \in (0 \dots \|t\|)) \to t prefix j \in Word A$
421	418 420	ffvelcdmd	$⊢ ((((φ \land g \in F) \land i \in F) \land t \in Word A) \land j \in (0 \dots \|t\|)) \to g (t prefix j) \in ℤ$
422	184	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land t \in Word A) \land j \in (0 \dots \|t\|)) \to i : Word A ⟶ ℤ$
423		swrdcl	$⊢ t \in Word A \to t substr ⟨j, \|t\|⟩ \in Word A$
424	423	ad2antlr	$⊢ ((((φ \land g \in F) \land i \in F) \land t \in Word A) \land j \in (0 \dots \|t\|)) \to t substr ⟨j, \|t\|⟩ \in Word A$
425	422 424	ffvelcdmd	$⊢ ((((φ \land g \in F) \land i \in F) \land t \in Word A) \land j \in (0 \dots \|t\|)) \to i (t substr ⟨j, \|t\|⟩) \in ℤ$
426	421 425	zmulcld	$⊢ ((((φ \land g \in F) \land i \in F) \land t \in Word A) \land j \in (0 \dots \|t\|)) \to g (t prefix j) i (t substr ⟨j, \|t\|⟩) \in ℤ$
427	417 426	fsumzcl	$⊢ (((φ \land g \in F) \land i \in F) \land t \in Word A) \to \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩) \in ℤ$
428	427	fmpttd	$⊢ ((φ \land g \in F) \land i \in F) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) : Word A ⟶ ℤ$
429	416 109 428	elmapdd	$⊢ ((φ \land g \in F) \land i \in F) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) \in (ℤ^{Word A})$
430		0zd	$⊢ ((φ \land g \in F) \land i \in F) \to 0 \in ℤ$
431	428	ffund	$⊢ ((φ \land g \in F) \land i \in F) \to Fun (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩))$
432		ccatfn	$⊢ ++ Fn (V \times V)$
433		fnfun	$⊢ ++ Fn (V \times V) \to Fun ++$
434	432 433	ax-mp	$⊢ Fun ++$
435		imafi	$⊢ (Fun ++ \land {supp}_{0} (g) \times {supp}_{0} (i) \in Fin) \to ++ [{supp}_{0} (g) \times {supp}_{0} (i)] \in Fin$
436	434 244 435	sylancr	$⊢ ((φ \land g \in F) \land i \in F) \to ++ [{supp}_{0} (g) \times {supp}_{0} (i)] \in Fin$
437		fveq2	$⊢ t = w \to \|t\| = \|w\|$
438	437	oveq2d	$⊢ t = w \to (0 \dots \|t\|) = (0 \dots \|w\|)$
439		fvoveq1	$⊢ t = w \to g (t prefix j) = g (w prefix j)$
440		id	$⊢ t = w \to t = w$
441	437	opeq2d	$⊢ t = w \to ⟨j, \|t\|⟩ = ⟨j, \|w\|⟩$
442	440 441	oveq12d	$⊢ t = w \to t substr ⟨j, \|t\|⟩ = w substr ⟨j, \|w\|⟩$
443	442	fveq2d	$⊢ t = w \to i (t substr ⟨j, \|t\|⟩) = i (w substr ⟨j, \|w\|⟩)$
444	439 443	oveq12d	$⊢ t = w \to g (t prefix j) i (t substr ⟨j, \|t\|⟩) = g (w prefix j) i (w substr ⟨j, \|w\|⟩)$
445	444	adantr	$⊢ (t = w \land j \in (0 \dots \|t\|)) \to g (t prefix j) i (t substr ⟨j, \|t\|⟩) = g (w prefix j) i (w substr ⟨j, \|w\|⟩)$
446	438 445	sumeq12dv	$⊢ t = w \to \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩) = \sum_{j = 0}^{\|w\|} g (w prefix j) i (w substr ⟨j, \|w\|⟩)$
447		oveq1	$⊢ u = w prefix j \to u ++ v = (w prefix j) ++ v$
448	447	eqeq2d	$⊢ u = w prefix j \to (w = u ++ v \leftrightarrow w = (w prefix j) ++ v)$
449		oveq2	$⊢ v = w substr ⟨j, \|w\|⟩ \to (w prefix j) ++ v = (w prefix j) ++ (w substr ⟨j, \|w\|⟩)$
450	449	eqeq2d	$⊢ v = w substr ⟨j, \|w\|⟩ \to (w = (w prefix j) ++ v \leftrightarrow w = (w prefix j) ++ (w substr ⟨j, \|w\|⟩))$
451	246	ad4antr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to g Fn Word A$
452	109	ad4antr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to Word A \in V$
453		0zd	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to 0 \in ℤ$
454		simpr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \to w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])$
455	454	eldifad	$⊢ (((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \to w \in Word A$
456	455	adantr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to w \in Word A$
457		pfxcl	$⊢ w \in Word A \to w prefix j \in Word A$
458	456 457	syl	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to w prefix j \in Word A$
459	458	ad2antrr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to w prefix j \in Word A$
460		simplr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to g (w prefix j) \neq 0$
461	451 452 453 459 460	elsuppfnd	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to w prefix j \in {supp}_{0} (g)$
462	275	ad4antr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to i Fn Word A$
463		swrdcl	$⊢ w \in Word A \to w substr ⟨j, \|w\|⟩ \in Word A$
464	456 463	syl	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to w substr ⟨j, \|w\|⟩ \in Word A$
465	464	ad2antrr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to w substr ⟨j, \|w\|⟩ \in Word A$
466		simpr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to i (w substr ⟨j, \|w\|⟩) \neq 0$
467	462 452 453 465 466	elsuppfnd	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to w substr ⟨j, \|w\|⟩ \in {supp}_{0} (i)$
468	456	ad2antrr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to w \in Word A$
469		simpllr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to j \in (0 \dots \|w\|)$
470		pfxcctswrd	$⊢ (w \in Word A \land j \in (0 \dots \|w\|)) \to (w prefix j) ++ (w substr ⟨j, \|w\|⟩) = w$
471	468 469 470	syl2anc	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to (w prefix j) ++ (w substr ⟨j, \|w\|⟩) = w$
472	471	eqcomd	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to w = (w prefix j) ++ (w substr ⟨j, \|w\|⟩)$
473	448 450 461 467 472	2rspcedvdw	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to \exists u \in {supp}_{0} (g) \exists v \in {supp}_{0} (i) w = u ++ v$
474		fnov	$⊢ ++ Fn (V \times V) \leftrightarrow ++ = (u \in V, v \in V ⟼ u ++ v)$
475	432 474	mpbi	$⊢ ++ = (u \in V, v \in V ⟼ u ++ v)$
476	200	a1i	$⊢ ⊤ \to w \in V$
477		ssv	$⊢ g supp 0 \subseteq V$
478	477	a1i	$⊢ ⊤ \to g supp 0 \subseteq V$
479		ssv	$⊢ i supp 0 \subseteq V$
480	479	a1i	$⊢ ⊤ \to i supp 0 \subseteq V$
481	475 476 478 480	elimampo	$⊢ ⊤ \to (w \in ++ [{supp}_{0} (g) \times {supp}_{0} (i)] \leftrightarrow \exists u \in {supp}_{0} (g) \exists v \in {supp}_{0} (i) w = u ++ v)$
482	481	mptru	$⊢ w \in ++ [{supp}_{0} (g) \times {supp}_{0} (i)] \leftrightarrow \exists u \in {supp}_{0} (g) \exists v \in {supp}_{0} (i) w = u ++ v$
483	473 482	sylibr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to w \in ++ [{supp}_{0} (g) \times {supp}_{0} (i)]$
484	483	anasss	$⊢ (((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land (g (w prefix j) \neq 0 \land i (w substr ⟨j, \|w\|⟩) \neq 0)) \to w \in ++ [{supp}_{0} (g) \times {supp}_{0} (i)]$
485	454	ad3antrrr	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])$
486	485	eldifbd	$⊢ ((((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land g (w prefix j) \neq 0) \land i (w substr ⟨j, \|w\|⟩) \neq 0) \to \neg w \in ++ [{supp}_{0} (g) \times {supp}_{0} (i)]$
487	486	anasss	$⊢ (((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \land (g (w prefix j) \neq 0 \land i (w substr ⟨j, \|w\|⟩) \neq 0)) \to \neg w \in ++ [{supp}_{0} (g) \times {supp}_{0} (i)]$
488	484 487	pm2.65da	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to \neg (g (w prefix j) \neq 0 \land i (w substr ⟨j, \|w\|⟩) \neq 0)$
489		df-ne	$⊢ g (w prefix j) \neq 0 \leftrightarrow \neg g (w prefix j) = 0$
490		df-ne	$⊢ i (w substr ⟨j, \|w\|⟩) \neq 0 \leftrightarrow \neg i (w substr ⟨j, \|w\|⟩) = 0$
491	489 490	anbi12i	$⊢ (g (w prefix j) \neq 0 \land i (w substr ⟨j, \|w\|⟩) \neq 0) \leftrightarrow (\neg g (w prefix j) = 0 \land \neg i (w substr ⟨j, \|w\|⟩) = 0)$
492	491	notbii	$⊢ \neg (g (w prefix j) \neq 0 \land i (w substr ⟨j, \|w\|⟩) \neq 0) \leftrightarrow \neg (\neg g (w prefix j) = 0 \land \neg i (w substr ⟨j, \|w\|⟩) = 0)$
493		pm4.57	$⊢ \neg (\neg g (w prefix j) = 0 \land \neg i (w substr ⟨j, \|w\|⟩) = 0) \leftrightarrow (g (w prefix j) = 0 \lor i (w substr ⟨j, \|w\|⟩) = 0)$
494	492 493	bitr2i	$⊢ (g (w prefix j) = 0 \lor i (w substr ⟨j, \|w\|⟩) = 0) \leftrightarrow \neg (g (w prefix j) \neq 0 \land i (w substr ⟨j, \|w\|⟩) \neq 0)$
495	488 494	sylibr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to (g (w prefix j) = 0 \lor i (w substr ⟨j, \|w\|⟩) = 0)$
496	294	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to g : Word A ⟶ ℤ$
497	496 458	ffvelcdmd	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to g (w prefix j) \in ℤ$
498	497	zcnd	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to g (w prefix j) \in ℂ$
499	184	ad2antrr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to i : Word A ⟶ ℤ$
500	499 464	ffvelcdmd	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to i (w substr ⟨j, \|w\|⟩) \in ℤ$
501	500	zcnd	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to i (w substr ⟨j, \|w\|⟩) \in ℂ$
502	498 501	mul0ord	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to (g (w prefix j) i (w substr ⟨j, \|w\|⟩) = 0 \leftrightarrow (g (w prefix j) = 0 \lor i (w substr ⟨j, \|w\|⟩) = 0))$
503	495 502	mpbird	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land j \in (0 \dots \|w\|)) \to g (w prefix j) i (w substr ⟨j, \|w\|⟩) = 0$
504	503	sumeq2dv	$⊢ (((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \to \sum_{j = 0}^{\|w\|} g (w prefix j) i (w substr ⟨j, \|w\|⟩) = \sum_{j = 0}^{\|w\|} 0$
505		fzssuz	$⊢ (0 \dots \|w\|) \subseteq ℤ_{\geq 0}$
506		sumz	$⊢ ((0 \dots \|w\|) \subseteq ℤ_{\geq 0} \lor (0 \dots \|w\|) \in Fin) \to \sum_{j = 0}^{\|w\|} 0 = 0$
507	506	orcs	$⊢ (0 \dots \|w\|) \subseteq ℤ_{\geq 0} \to \sum_{j = 0}^{\|w\|} 0 = 0$
508	505 507	mp1i	$⊢ (((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \to \sum_{j = 0}^{\|w\|} 0 = 0$
509	504 508	eqtrd	$⊢ (((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \to \sum_{j = 0}^{\|w\|} g (w prefix j) i (w substr ⟨j, \|w\|⟩) = 0$
510	446 509	sylan9eqr	$⊢ ((((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \land t = w) \to \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩) = 0$
511		0zd	$⊢ (((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \to 0 \in ℤ$
512	370 510 455 511	fvmptd2	$⊢ (((φ \land g \in F) \land i \in F) \land w \in (Word A ∖ ++ [{supp}_{0} (g) \times {supp}_{0} (i)])) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w) = 0$
513	428 512	suppss	$⊢ ((φ \land g \in F) \land i \in F) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) supp 0 \subseteq ++ [{supp}_{0} (g) \times {supp}_{0} (i)]$
514	436 513	ssfid	$⊢ ((φ \land g \in F) \land i \in F) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) supp 0 \in Fin$
515	429 430 431 514	isfsuppd	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)))$
516	415 429 515	elrabd	$⊢ ((φ \land g \in F) \land i \in F) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) \in \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
517	516 5	eleqtrrdi	$⊢ ((φ \land g \in F) \land i \in F) \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) \in F$
518		fveq2	$⊢ v = w \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w)$
519	518 145	oveq12d	$⊢ v = w \to (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v) = (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w) \underset{˙}{\cdot} (\sum_{M}, w)$
520	519	cbvmptv	$⊢ (v \in Word A ⟼ (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) = (w \in Word A ⟼ (t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
521	520	oveq2i	$⊢ \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) = \underset{w \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
522	521	a1i	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) = \underset{w \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
523	414 517 522	rspcedvdw	$⊢ ((φ \land g \in F) \land i \in F) \to \exists h \in F \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) = \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w))$
524		ovexd	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) \in V$
525	409 523 524	elrnmptd	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
526	525 8	eleqtrrdi	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{v \in Word A}{\sum_{R}} ((t \in Word A ⟼ \sum_{j = 0}^{\|t\|} g (t prefix j) i (t substr ⟨j, \|t\|⟩)) (v) \underset{˙}{\cdot} (\sum_{M}, v)) \in S$
527	404 526	eqeltrd	$⊢ ((φ \land g \in F) \land i \in F) \to (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \cdot_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \in S$
528	527	adantllr	$⊢ (((φ \land x \in S) \land g \in F) \land i \in F) \to (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \cdot_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \in S$
529	528	adantllr	$⊢ ((((φ \land x \in S) \land y \in S) \land g \in F) \land i \in F) \to (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \cdot_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \in S$
530	529	adantlr	$⊢ (((((φ \land x \in S) \land y \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \land i \in F) \to (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \cdot_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \in S$
531	530	adantr	$⊢ ((((((φ \land x \in S) \land y \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \land i \in F) \land y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \cdot_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \in S$
532	107 531	eqeltrd	$⊢ ((((((φ \land x \in S) \land y \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \land i \in F) \land y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to x \cdot_{R} y \in S$
533	8	eleq2i	$⊢ y \in S \leftrightarrow y \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
534	169	oveq2d	$⊢ g = i \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
535	534	cbvmptv	$⊢ (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) = (i \in F ⟼ \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
536	535	elrnmpt	$⊢ y \in V \to (y \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \leftrightarrow \exists i \in F y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
537	536	elv	$⊢ y \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \leftrightarrow \exists i \in F y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
538	533 537	sylbb	$⊢ y \in S \to \exists i \in F y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
539	538	adantl	$⊢ ((φ \land x \in S) \land y \in S) \to \exists i \in F y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
540	539	ad2antrr	$⊢ ((((φ \land x \in S) \land y \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to \exists i \in F y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
541	532 540	r19.29a	$⊢ ((((φ \land x \in S) \land y \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to x \cdot_{R} y \in S$
542	8	eleq2i	$⊢ x \in S \leftrightarrow x \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
543	71	elrnmpt	$⊢ x \in V \to (x \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \leftrightarrow \exists g \in F x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
544	543	elv	$⊢ x \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \leftrightarrow \exists g \in F x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
545	542 544	sylbb	$⊢ x \in S \to \exists g \in F x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
546	545	ad2antlr	$⊢ ((φ \land x \in S) \land y \in S) \to \exists g \in F x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
547	541 546	r19.29a	$⊢ ((φ \land x \in S) \land y \in S) \to x \cdot_{R} y \in S$
548	547	anasss	$⊢ (φ \land (x \in S \land y \in S)) \to x \cdot_{R} y \in S$
549	548	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in S x \cdot_{R} y \in S$
550	1 24 108	issubrg2	$⊢ R \in Ring \to (S \in SubRing (R) \leftrightarrow (S \in SubGrp (R) \land 1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S))$
551	550	biimpar	$⊢ (R \in Ring \land (S \in SubGrp (R) \land 1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S)) \to S \in SubRing (R)$
552	6 9 104 549 551	syl13anc	$⊢ φ \to S \in SubRing (R)$

Metamath Proof Explorer

Theorem elrgspnlem2

Proof