elrgspnlem4

	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	elrgspnlem4	$⊢ φ \to N (A) = S$

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	a1i	$⊢ φ \to B = {Base}_{R}$
10	4	a1i	$⊢ φ \to N = RingSpan (R)$
11		eqidd	$⊢ φ \to N (A) = N (A)$
12	6 9 7 10 11	rgspnval	$⊢ φ \to N (A) = ⋂ \{t \in SubRing (R) \| A \subseteq t\}$
13		sseq2	$⊢ t = S \to (A \subseteq t \leftrightarrow A \subseteq S)$
14	1 2 3 4 5 6 7 8	elrgspnlem2	$⊢ φ \to S \in SubRing (R)$
15	1 2 3 4 5 6 7 8	elrgspnlem3	$⊢ φ \to A \subseteq S$
16	13 14 15	elrabd	$⊢ φ \to S \in \{t \in SubRing (R) \| A \subseteq t\}$
17		intss1	$⊢ S \in \{t \in SubRing (R) \| A \subseteq t\} \to ⋂ \{t \in SubRing (R) \| A \subseteq t\} \subseteq S$
18	16 17	syl	$⊢ φ \to ⋂ \{t \in SubRing (R) \| A \subseteq t\} \subseteq S$
19		simpr	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land s \in S) \land g \in F) \land s = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to s = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
20		eqidd	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \to g supp 0 = g supp 0$
21		oveq1	$⊢ f = g \to f supp 0 = g supp 0$
22	21	eqeq1d	$⊢ f = g \to (f supp 0 = g supp 0 \leftrightarrow g supp 0 = g supp 0)$
23		fveq1	$⊢ f = g \to f (w) = g (w)$
24	23	oveq1d	$⊢ f = g \to f (w) \underset{˙}{\cdot} (\sum_{M}, w) = g (w) \underset{˙}{\cdot} (\sum_{M}, w)$
25	24	mpteq2dv	$⊢ f = g \to (w \in Word A ⟼ f (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
26	25	oveq2d	$⊢ f = g \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
27	26	eleq1d	$⊢ f = g \to (\underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t \leftrightarrow \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
28	22 27	imbi12d	$⊢ f = g \to ((f supp 0 = g supp 0 \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow (g supp 0 = g supp 0 \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
29		eqeq2	$⊢ i = \emptyset \to (f supp 0 = i \leftrightarrow f supp 0 = \emptyset)$
30	29	imbi1d	$⊢ i = \emptyset \to ((f supp 0 = i \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow (f supp 0 = \emptyset \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
31	30	ralbidv	$⊢ i = \emptyset \to (\forall f \in F (f supp 0 = i \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow \forall f \in F (f supp 0 = \emptyset \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
32		eqeq2	$⊢ i = h \to (f supp 0 = i \leftrightarrow f supp 0 = h)$
33	32	imbi1d	$⊢ i = h \to ((f supp 0 = i \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
34	33	ralbidv	$⊢ i = h \to (\forall f \in F (f supp 0 = i \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
35		eqeq2	$⊢ i = h \cup \{x\} \to (f supp 0 = i \leftrightarrow f supp 0 = h \cup \{x\})$
36	35	imbi1d	$⊢ i = h \cup \{x\} \to ((f supp 0 = i \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow (f supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
37	36	ralbidv	$⊢ i = h \cup \{x\} \to (\forall f \in F (f supp 0 = i \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow \forall f \in F (f supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
38		eqeq2	$⊢ i = g supp 0 \to (f supp 0 = i \leftrightarrow f supp 0 = g supp 0)$
39	38	imbi1d	$⊢ i = g supp 0 \to ((f supp 0 = i \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow (f supp 0 = g supp 0 \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
40	39	ralbidv	$⊢ i = g supp 0 \to (\forall f \in F (f supp 0 = i \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow \forall f \in F (f supp 0 = g supp 0 \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
41		eqid	$⊢ 0_{R} = 0_{R}$
42	6	ringcmnd	$⊢ φ \to R \in CMnd$
43	42	ad5antr	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to R \in CMnd$
44	1	fvexi	$⊢ B \in V$
45	44	a1i	$⊢ φ \to B \in V$
46	45 7	ssexd	$⊢ φ \to A \in V$
47		wrdexg	$⊢ A \in V \to Word A \in V$
48	46 47	syl	$⊢ φ \to Word A \in V$
49	48	ad5antr	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to Word A \in V$
50		simp-4l	$⊢ ((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \to φ$
51	5	reqabi	$⊢ f \in F \leftrightarrow (f \in (ℤ^{Word A}) \land {finSupp}_{0} (f))$
52	51	simplbi	$⊢ f \in F \to f \in (ℤ^{Word A})$
53	52	adantl	$⊢ ((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \to f \in (ℤ^{Word A})$
54		zex	$⊢ ℤ \in V$
55	54	a1i	$⊢ φ \to ℤ \in V$
56	55 48	elmapd	$⊢ φ \to (f \in (ℤ^{Word A}) \leftrightarrow f : Word A ⟶ ℤ)$
57	56	biimpa	$⊢ (φ \land f \in (ℤ^{Word A})) \to f : Word A ⟶ ℤ$
58	50 53 57	syl2anc	$⊢ ((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \to f : Word A ⟶ ℤ$
59	58	ffnd	$⊢ ((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \to f Fn Word A$
60	59	ad2antrr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to f Fn Word A$
61	49	adantr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to Word A \in V$
62		0zd	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to 0 \in ℤ$
63		simpr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to w \in (Word A ∖ \emptyset)$
64	63	eldifad	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to w \in Word A$
65	63	eldifbd	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to \neg w \in \emptyset$
66		simplr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to f supp 0 = \emptyset$
67	65 66	neleqtrrd	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to \neg w \in {supp}_{0} (f)$
68	64 67	eldifd	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to w \in (Word A ∖ {supp}_{0} (f))$
69	60 61 62 68	fvdifsupp	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to f (w) = 0$
70	69	oveq1d	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to f (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0 \underset{˙}{\cdot} (\sum_{M}, w)$
71	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
72	6 71	syl	$⊢ φ \to M \in Mnd$
73	72	ad6antr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to M \in Mnd$
74		sswrd	$⊢ A \subseteq B \to Word A \subseteq Word B$
75	7 74	syl	$⊢ φ \to Word A \subseteq Word B$
76	75	ad6antr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to Word A \subseteq Word B$
77	76 64	sseldd	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to w \in Word B$
78	2 1	mgpbas	$⊢ B = {Base}_{M}$
79	78	gsumwcl	$⊢ (M \in Mnd \land w \in Word B) \to \sum_{M} w \in B$
80	73 77 79	syl2anc	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to \sum_{M} w \in B$
81	1 41 3	mulg0	$⊢ \sum_{M} w \in B \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
82	80 81	syl	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
83	70 82	eqtrd	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in (Word A ∖ \emptyset)) \to f (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
84		0fi	$⊢ \emptyset \in Fin$
85	84	a1i	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to \emptyset \in Fin$
86	6	ringgrpd	$⊢ φ \to R \in Grp$
87	86	ad6antr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in Word A) \to R \in Grp$
88	58	ad2antrr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in Word A) \to f : Word A ⟶ ℤ$
89		simpr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in Word A) \to w \in Word A$
90	88 89	ffvelcdmd	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in Word A) \to f (w) \in ℤ$
91	72	ad6antr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in Word A) \to M \in Mnd$
92	75	ad6antr	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in Word A) \to Word A \subseteq Word B$
93	92 89	sseldd	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in Word A) \to w \in Word B$
94	91 93 79	syl2anc	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in Word A) \to \sum_{M} w \in B$
95	1 3 87 90 94	mulgcld	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \land w \in Word A) \to f (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
96		0ss	$⊢ \emptyset \subseteq Word A$
97	96	a1i	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to \emptyset \subseteq Word A$
98	1 41 43 49 83 85 95 97	gsummptres2	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in \emptyset}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w))$
99		mpt0	$⊢ (w \in \emptyset ⟼ f (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \emptyset$
100	99	a1i	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to (w \in \emptyset ⟼ f (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \emptyset$
101	100	oveq2d	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to \underset{w \in \emptyset}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \sum_{R} \emptyset$
102	41	gsum0	$⊢ \sum_{R} \emptyset = 0_{R}$
103	102	a1i	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to \sum_{R} \emptyset = 0_{R}$
104	98 101 103	3eqtrd	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) = 0_{R}$
105		subrgsubg	$⊢ t \in SubRing (R) \to t \in SubGrp (R)$
106	41	subg0cl	$⊢ t \in SubGrp (R) \to 0_{R} \in t$
107	105 106	syl	$⊢ t \in SubRing (R) \to 0_{R} \in t$
108	107	adantl	$⊢ (φ \land t \in SubRing (R)) \to 0_{R} \in t$
109	108	ad4antr	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to 0_{R} \in t$
110	104 109	eqeltrd	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \land f supp 0 = \emptyset) \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t$
111	110	ex	$⊢ ((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land f \in F) \to (f supp 0 = \emptyset \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
112	111	ralrimiva	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \to \forall f \in F (f supp 0 = \emptyset \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
113	42	ad7antr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to R \in CMnd$
114	48	ad7antr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to Word A \in V$
115		simp-5l	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \to φ$
116		breq1	$⊢ f = e \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} (e))$
117	116 5	elrab2	$⊢ e \in F \leftrightarrow (e \in (ℤ^{Word A}) \land {finSupp}_{0} (e))$
118	117	simplbi	$⊢ e \in F \to e \in (ℤ^{Word A})$
119	55 48	elmapd	$⊢ φ \to (e \in (ℤ^{Word A}) \leftrightarrow e : Word A ⟶ ℤ)$
120	119	biimpa	$⊢ (φ \land e \in (ℤ^{Word A})) \to e : Word A ⟶ ℤ$
121	118 120	sylan2	$⊢ (φ \land e \in F) \to e : Word A ⟶ ℤ$
122	115 121	sylancom	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \to e : Word A ⟶ ℤ$
123	122	adantl3r	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \to e : Word A ⟶ ℤ$
124	123	ffnd	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \to e Fn Word A$
125	124	ad2antrr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to e Fn Word A$
126	114	adantr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to Word A \in V$
127		0zd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to 0 \in ℤ$
128		simpr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to w \in (Word A ∖ {supp}_{0} (e))$
129	125 126 127 128	fvdifsupp	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to e (w) = 0$
130	129	oveq1d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to e (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0 \underset{˙}{\cdot} (\sum_{M}, w)$
131	72	ad8antr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to M \in Mnd$
132	75	ad8antr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to Word A \subseteq Word B$
133	128	eldifad	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to w \in Word A$
134	132 133	sseldd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to w \in Word B$
135	131 134 79	syl2anc	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to \sum_{M} w \in B$
136	135 81	syl	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
137	130 136	eqtrd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ {supp}_{0} (e))) \to e (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
138	117	simprbi	$⊢ e \in F \to {finSupp}_{0} (e)$
139	138	ad2antlr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to {finSupp}_{0} (e)$
140	139	fsuppimpd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e supp 0 \in Fin$
141	86	ad8antr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to R \in Grp$
142	123	ad2antrr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to e : Word A ⟶ ℤ$
143		simpr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to w \in Word A$
144	142 143	ffvelcdmd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to e (w) \in ℤ$
145	72	ad8antr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to M \in Mnd$
146	75	ad7antr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to Word A \subseteq Word B$
147	146	sselda	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to w \in Word B$
148	145 147 79	syl2anc	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to \sum_{M} w \in B$
149	1 3 141 144 148	mulgcld	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to e (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
150		suppssdm	$⊢ e supp 0 \subseteq dom e$
151	123	adantr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e : Word A ⟶ ℤ$
152	150 151	fssdm	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e supp 0 \subseteq Word A$
153	1 41 113 114 137 140 149 152	gsummptres2	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in e supp 0}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w))$
154	153	adantllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in e supp 0}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w))$
155		simpr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e supp 0 = h \cup \{x\}$
156	155	mpteq1d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (w \in {supp}_{0} (e) ⟼ e (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in (h \cup \{x\}) ⟼ e (w) \underset{˙}{\cdot} (\sum_{M}, w))$
157	156	oveq2d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in e supp 0}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in h \cup \{x\}}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w))$
158		eqid	$⊢ +_{R} = +_{R}$
159		breq1	$⊢ f = g \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} (g))$
160	159 5	elrab2	$⊢ g \in F \leftrightarrow (g \in (ℤ^{Word A}) \land {finSupp}_{0} (g))$
161	160	simprbi	$⊢ g \in F \to {finSupp}_{0} (g)$
162	161	adantl	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \to {finSupp}_{0} (g)$
163	162	fsuppimpd	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \to g supp 0 \in Fin$
164	163	ad4antr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to g supp 0 \in Fin$
165		simp-4r	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to h \subseteq g supp 0$
166	164 165	ssfid	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to h \in Fin$
167	86	ad8antr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to R \in Grp$
168	151	adantr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to e : Word A ⟶ ℤ$
169		suppssdm	$⊢ g supp 0 \subseteq dom g$
170		simp-7l	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to φ$
171		simp-5r	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to g \in F$
172	160	simplbi	$⊢ g \in F \to g \in (ℤ^{Word A})$
173	55 48	elmapd	$⊢ φ \to (g \in (ℤ^{Word A}) \leftrightarrow g : Word A ⟶ ℤ)$
174	173	biimpa	$⊢ (φ \land g \in (ℤ^{Word A})) \to g : Word A ⟶ ℤ$
175	172 174	sylan2	$⊢ (φ \land g \in F) \to g : Word A ⟶ ℤ$
176	170 171 175	syl2anc	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to g : Word A ⟶ ℤ$
177	169 176	fssdm	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to g supp 0 \subseteq Word A$
178	165 177	sstrd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to h \subseteq Word A$
179	178	sselda	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to w \in Word A$
180	168 179	ffvelcdmd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to e (w) \in ℤ$
181	179 148	syldan	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to \sum_{M} w \in B$
182	1 3 167 180 181	mulgcld	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to e (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
183		simpllr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to x \in ({supp}_{0} (g) ∖ h)$
184	183	eldifbd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \neg x \in h$
185	170 86	syl	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to R \in Grp$
186	183	eldifad	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to x \in {supp}_{0} (g)$
187	177 186	sseldd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to x \in Word A$
188	151 187	ffvelcdmd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e (x) \in ℤ$
189	170 72	syl	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to M \in Mnd$
190	146 187	sseldd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to x \in Word B$
191	78	gsumwcl	$⊢ (M \in Mnd \land x \in Word B) \to \sum_{M} x \in B$
192	189 190 191	syl2anc	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \sum_{M} x \in B$
193	1 3 185 188 192	mulgcld	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e (x) \underset{˙}{\cdot} (\sum_{M}, x) \in B$
194		fveq2	$⊢ w = x \to e (w) = e (x)$
195		oveq2	$⊢ w = x \to \sum_{M} w = \sum_{M} x$
196	194 195	oveq12d	$⊢ w = x \to e (w) \underset{˙}{\cdot} (\sum_{M}, w) = e (x) \underset{˙}{\cdot} (\sum_{M}, x)$
197	1 158 113 166 182 183 184 193 196	gsumunsn	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in h \cup \{x\}}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (\underset{w \in h}{\sum_{R}}, (e (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (e (x) \underset{˙}{\cdot} (\sum_{M}, x))$
198	197	adantllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in h \cup \{x\}}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (\underset{w \in h}{\sum_{R}}, (e (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (e (x) \underset{˙}{\cdot} (\sum_{M}, x))$
199	154 157 198	3eqtrd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (\underset{w \in h}{\sum_{R}}, (e (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (e (x) \underset{˙}{\cdot} (\sum_{M}, x))$
200	105	ad8antlr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to t \in SubGrp (R)$
201	124	adantr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e Fn Word A$
202		0zd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to 0 \in ℤ$
203	201 187 202	fmptunsnop	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (y \in Word A ⟼ if (y = x, 0, e (y))) = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}$
204	203	adantr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to (y \in Word A ⟼ if (y = x, 0, e (y))) = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}$
205	204	fveq1d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to (y \in Word A ⟼ if (y = x, 0, e (y))) (w) = (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w)$
206		eqid	$⊢ (y \in Word A ⟼ if (y = x, 0, e (y))) = (y \in Word A ⟼ if (y = x, 0, e (y)))$
207		eqidd	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land y = x) \to 0 = 0$
208	201	ad3antrrr	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to e Fn Word A$
209	114	ad3antrrr	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to Word A \in V$
210		0zd	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to 0 \in ℤ$
211		simplr	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to y = w$
212		simpllr	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to w \in (Word A ∖ h)$
213	212	eldifad	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to w \in Word A$
214	211 213	eqeltrd	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to y \in Word A$
215		simp-4r	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to e supp 0 = h \cup \{x\}$
216	212	eldifbd	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to \neg w \in h$
217	211 216	eqneltrd	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to \neg y \in h$
218		simpr	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to \neg y = x$
219	218	neqned	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to y \neq x$
220		nelsn	$⊢ y \neq x \to \neg y \in \{x\}$
221	219 220	syl	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to \neg y \in \{x\}$
222		nelun	$⊢ e supp 0 = h \cup \{x\} \to (\neg y \in {supp}_{0} (e) \leftrightarrow (\neg y \in h \land \neg y \in \{x\}))$
223	222	biimpar	$⊢ (e supp 0 = h \cup \{x\} \land (\neg y \in h \land \neg y \in \{x\})) \to \neg y \in {supp}_{0} (e)$
224	215 217 221 223	syl12anc	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to \neg y \in {supp}_{0} (e)$
225	214 224	eldifd	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to y \in (Word A ∖ {supp}_{0} (e))$
226	208 209 210 225	fvdifsupp	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \land \neg y = x) \to e (y) = 0$
227	207 226	ifeqda	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \land y = w) \to if (y = x, 0, e (y)) = 0$
228		simpr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to w \in (Word A ∖ h)$
229	228	eldifad	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to w \in Word A$
230		0zd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to 0 \in ℤ$
231	206 227 229 230	fvmptd2	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to (y \in Word A ⟼ if (y = x, 0, e (y))) (w) = 0$
232	205 231	eqtr3d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) = 0$
233	232	oveq1d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0 \underset{˙}{\cdot} (\sum_{M}, w)$
234	229 148	syldan	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to \sum_{M} w \in B$
235	234 81	syl	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
236	233 235	eqtrd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in (Word A ∖ h)) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
237	203	adantr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to (y \in Word A ⟼ if (y = x, 0, e (y))) = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}$
238	237	fveq1d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to (y \in Word A ⟼ if (y = x, 0, e (y))) (w) = (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w)$
239		0zd	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land y = x) \to 0 \in ℤ$
240	151	ad2antrr	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land \neg y = x) \to e : Word A ⟶ ℤ$
241		simplr	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land \neg y = x) \to y \in Word A$
242	240 241	ffvelcdmd	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land \neg y = x) \to e (y) \in ℤ$
243	239 242	ifclda	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \to if (y = x, 0, e (y)) \in ℤ$
244	243	fmpttd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (y \in Word A ⟼ if (y = x, 0, e (y))) : Word A ⟶ ℤ$
245	244	ffvelcdmda	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to (y \in Word A ⟼ if (y = x, 0, e (y))) (w) \in ℤ$
246	238 245	eqeltrrd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \in ℤ$
247	1 3 141 246 148	mulgcld	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in Word A) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
248	1 41 113 114 236 166 247 178	gsummptres2	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in Word A}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in h}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
249	248	adantllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in Word A}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in h}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
250	203	adantr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to (y \in Word A ⟼ if (y = x, 0, e (y))) = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}$
251	250	fveq1d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to (y \in Word A ⟼ if (y = x, 0, e (y))) (w) = (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w)$
252		simpr	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \land y = w) \to y = w$
253		simplr	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \land y = w) \to w \in h$
254	252 253	eqeltrd	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \land y = w) \to y \in h$
255	184	ad2antrr	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \land y = w) \to \neg x \in h$
256		nelneq	$⊢ (y \in h \land \neg x \in h) \to \neg y = x$
257	254 255 256	syl2anc	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \land y = w) \to \neg y = x$
258	257	iffalsed	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \land y = w) \to if (y = x, 0, e (y)) = e (y)$
259	252	fveq2d	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \land y = w) \to e (y) = e (w)$
260	258 259	eqtrd	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \land y = w) \to if (y = x, 0, e (y)) = e (w)$
261	206 260 179 180	fvmptd2	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to (y \in Word A ⟼ if (y = x, 0, e (y))) (w) = e (w)$
262	251 261	eqtr3d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) = e (w)$
263	262	oveq1d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land w \in h) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w) = e (w) \underset{˙}{\cdot} (\sum_{M}, w)$
264	263	mpteq2dva	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (w \in h ⟼ (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in h ⟼ e (w) \underset{˙}{\cdot} (\sum_{M}, w))$
265	264	adantllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (w \in h ⟼ (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in h ⟼ e (w) \underset{˙}{\cdot} (\sum_{M}, w))$
266	265	oveq2d	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in h}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in h}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w))$
267	249 266	eqtrd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in Word A}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in h}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w))$
268		simplr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e \in F$
269	268	resexd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to {e ↾}_{(Word A ∖ \{x\})} \in V$
270		snex	$⊢ \{⟨x, 0⟩\} \in V$
271	270	a1i	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \{⟨x, 0⟩\} \in V$
272	269 271 202	suppun2	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) supp 0 = {supp}_{0} (({e ↾}_{(Word A ∖ \{x\})})) \cup {supp}_{0} (\{⟨x, 0⟩\})$
273	114 202 201	fdifsupp	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to ({e ↾}_{(Word A ∖ \{x\})}) supp 0 = {supp}_{0} (e) ∖ \{x\}$
274		simpr	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e supp 0 = h \cup \{x\}$
275	274	difeq1d	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to {supp}_{0} (e) ∖ \{x\} = (h \cup \{x\}) ∖ \{x\}$
276		disjsn	$⊢ h \cap \{x\} = \emptyset \leftrightarrow \neg x \in h$
277		undif5	$⊢ h \cap \{x\} = \emptyset \to (h \cup \{x\}) ∖ \{x\} = h$
278	276 277	sylbir	$⊢ \neg x \in h \to (h \cup \{x\}) ∖ \{x\} = h$
279	184 278	syl	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (h \cup \{x\}) ∖ \{x\} = h$
280	273 275 279	3eqtrd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to ({e ↾}_{(Word A ∖ \{x\})}) supp 0 = h$
281		vex	$⊢ x \in V$
282		c0ex	$⊢ 0 \in V$
283	281 282	xpsn	$⊢ \{x\} \times \{0\} = \{⟨x, 0⟩\}$
284	283	oveq1i	$⊢ (\{x\} \times \{0\}) supp 0 = \{⟨x, 0⟩\} supp 0$
285		fczsupp0	$⊢ (\{x\} \times \{0\}) supp 0 = \emptyset$
286	284 285	eqtr3i	$⊢ \{⟨x, 0⟩\} supp 0 = \emptyset$
287	286	a1i	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \{⟨x, 0⟩\} supp 0 = \emptyset$
288	280 287	uneq12d	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to {supp}_{0} (({e ↾}_{(Word A ∖ \{x\})})) \cup {supp}_{0} (\{⟨x, 0⟩\}) = h \cup \emptyset$
289		un0	$⊢ h \cup \emptyset = h$
290	289	a1i	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to h \cup \emptyset = h$
291	272 288 290	3eqtrd	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) supp 0 = h$
292	291	adantllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) supp 0 = h$
293		oveq1	$⊢ f = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \to f supp 0 = (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) supp 0$
294	293	eqeq1d	$⊢ f = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \to (f supp 0 = h \leftrightarrow (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) supp 0 = h)$
295		fveq1	$⊢ f = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \to f (w) = (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w)$
296	295	oveq1d	$⊢ f = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \to f (w) \underset{˙}{\cdot} (\sum_{M}, w) = (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)$
297	296	mpteq2dv	$⊢ f = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \to (w \in Word A ⟼ f (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
298	297	oveq2d	$⊢ f = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
299	298	eleq1d	$⊢ f = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \to (\underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t \leftrightarrow \underset{w \in Word A}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
300	294 299	imbi12d	$⊢ f = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \to ((f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) supp 0 = h \to \underset{w \in Word A}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
301		simpllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
302		breq1	$⊢ f = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\})))$
303	54	a1i	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to ℤ \in V$
304	114	adantllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to Word A \in V$
305	203	adantllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (y \in Word A ⟼ if (y = x, 0, e (y))) = ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}$
306		0zd	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land y = x) \to 0 \in ℤ$
307		simp-10l	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land \neg y = x) \to φ$
308		simp-4r	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land \neg y = x) \to e \in F$
309	307 308 121	syl2anc	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land \neg y = x) \to e : Word A ⟶ ℤ$
310		simplr	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land \neg y = x) \to y \in Word A$
311	309 310	ffvelcdmd	$⊢ ((((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \land \neg y = x) \to e (y) \in ℤ$
312	306 311	ifclda	$⊢ (((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \land y \in Word A) \to if (y = x, 0, e (y)) \in ℤ$
313	312	fmpttd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (y \in Word A ⟼ if (y = x, 0, e (y))) : Word A ⟶ ℤ$
314	305 313	feq1dd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) : Word A ⟶ ℤ$
315	303 304 314	elmapdd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \in (ℤ^{Word A})$
316		0zd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to 0 \in ℤ$
317	314	ffund	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to Fun (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\})$
318	166	adantllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to h \in Fin$
319	292 318	eqeltrd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) supp 0 \in Fin$
320	315 316 317 319	isfsuppd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to {finSupp}_{0} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}))$
321	302 315 320	elrabd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \in \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
322	321 5	eleqtrrdi	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to ({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\} \in F$
323	300 301 322	rspcdva	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) supp 0 = h \to \underset{w \in Word A}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
324	292 323	mpd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in Word A}{\sum_{R}} ((({e ↾}_{(Word A ∖ \{x\})}) \cup \{⟨x, 0⟩\}) (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t$
325	267 324	eqeltrrd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in h}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t$
326	86	ad8antr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to R \in Grp$
327	2	subrgsubm	$⊢ t \in SubRing (R) \to t \in SubMnd (M)$
328	327	ad8antlr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to t \in SubMnd (M)$
329		sswrd	$⊢ A \subseteq t \to Word A \subseteq Word t$
330	329	ad7antlr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to Word A \subseteq Word t$
331	187	adantllr	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to x \in Word A$
332	330 331	sseldd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to x \in Word t$
333		gsumwsubmcl	$⊢ (t \in SubMnd (M) \land x \in Word t) \to \sum_{M} x \in t$
334	328 332 333	syl2anc	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \sum_{M} x \in t$
335	123	ad4ant13	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e : Word A ⟶ ℤ$
336	335 331	ffvelcdmd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e (x) \in ℤ$
337	1 3 326 334 200 336	subgmulgcld	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to e (x) \underset{˙}{\cdot} (\sum_{M}, x) \in t$
338	158 200 325 337	subgcld	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to (\underset{w \in h}{\sum_{R}}, (e (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (e (x) \underset{˙}{\cdot} (\sum_{M}, x)) \in t$
339	199 338	eqeltrd	$⊢ ((((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \land e supp 0 = h \cup \{x\}) \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t$
340	339	ex	$⊢ (((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \land e \in F) \to (e supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
341	340	ralrimiva	$⊢ ((((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \land \forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)) \to \forall e \in F (e supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
342	341	ex	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land h \subseteq g supp 0) \land x \in ({supp}_{0} (g) ∖ h)) \to (\forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \to \forall e \in F (e supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
343	342	anasss	$⊢ ((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land (h \subseteq g supp 0 \land x \in ({supp}_{0} (g) ∖ h))) \to (\forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \to \forall e \in F (e supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
344		oveq1	$⊢ e = f \to e supp 0 = f supp 0$
345	344	eqeq1d	$⊢ e = f \to (e supp 0 = h \cup \{x\} \leftrightarrow f supp 0 = h \cup \{x\})$
346		fveq1	$⊢ e = f \to e (w) = f (w)$
347	346	oveq1d	$⊢ e = f \to e (w) \underset{˙}{\cdot} (\sum_{M}, w) = f (w) \underset{˙}{\cdot} (\sum_{M}, w)$
348	347	mpteq2dv	$⊢ e = f \to (w \in Word A ⟼ e (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ f (w) \underset{˙}{\cdot} (\sum_{M}, w))$
349	348	oveq2d	$⊢ e = f \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w))$
350	349	eleq1d	$⊢ e = f \to (\underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t \leftrightarrow \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
351	345 350	imbi12d	$⊢ e = f \to ((e supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow (f supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
352	351	cbvralvw	$⊢ \forall e \in F (e supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (e (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \leftrightarrow \forall f \in F (f supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
353	343 352	imbitrdi	$⊢ ((((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \land (h \subseteq g supp 0 \land x \in ({supp}_{0} (g) ∖ h))) \to (\forall f \in F (f supp 0 = h \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t) \to \forall f \in F (f supp 0 = h \cup \{x\} \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t))$
354	31 34 37 40 112 353 163	findcard2d	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \to \forall f \in F (f supp 0 = g supp 0 \to \underset{w \in Word A}{\sum_{R}} (f (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
355		simpr	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \to g \in F$
356	28 354 355	rspcdva	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \to (g supp 0 = g supp 0 \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t)$
357	20 356	mpd	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land g \in F) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t$
358	357	ad4ant13	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land s \in S) \land g \in F) \land s = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in t$
359	19 358	eqeltrd	$⊢ (((((φ \land t \in SubRing (R)) \land A \subseteq t) \land s \in S) \land g \in F) \land s = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to s \in t$
360		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)))$
361	8	eleq2i	$⊢ s \in S \leftrightarrow s \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
362	361	biimpi	$⊢ s \in S \to s \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
363	362	adantl	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land s \in S) \to s \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
364	360 363	elrnmpt2d	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land s \in S) \to \exists g \in F s = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
365	359 364	r19.29a	$⊢ (((φ \land t \in SubRing (R)) \land A \subseteq t) \land s \in S) \to s \in t$
366	365	ex	$⊢ ((φ \land t \in SubRing (R)) \land A \subseteq t) \to (s \in S \to s \in t)$
367	366	ssrdv	$⊢ ((φ \land t \in SubRing (R)) \land A \subseteq t) \to S \subseteq t$
368	367	ex	$⊢ (φ \land t \in SubRing (R)) \to (A \subseteq t \to S \subseteq t)$
369	368	ralrimiva	$⊢ φ \to \forall t \in SubRing (R) (A \subseteq t \to S \subseteq t)$
370		ssintrab	$⊢ S \subseteq ⋂ \{t \in SubRing (R) \| A \subseteq t\} \leftrightarrow \forall t \in SubRing (R) (A \subseteq t \to S \subseteq t)$
371	369 370	sylibr	$⊢ φ \to S \subseteq ⋂ \{t \in SubRing (R) \| A \subseteq t\}$
372	18 371	eqssd	$⊢ φ \to ⋂ \{t \in SubRing (R) \| A \subseteq t\} = S$
373	12 372	eqtrd	$⊢ φ \to N (A) = S$

Metamath Proof Explorer

Theorem elrgspnlem4

Proof