elrgspnlem1

	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	elrgspnlem1	$⊢ φ \to S \in SubGrp (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	6	ringgrpd	$⊢ φ \to R \in Grp$
10		simpr	$⊢ (((φ \land x \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
11		eqid	$⊢ 0_{R} = 0_{R}$
12	6	ringcmnd	$⊢ φ \to R \in CMnd$
13	12	adantr	$⊢ (φ \land g \in F) \to R \in CMnd$
14	1	fvexi	$⊢ B \in V$
15	14	a1i	$⊢ φ \to B \in V$
16	15 7	ssexd	$⊢ φ \to A \in V$
17		wrdexg	$⊢ A \in V \to Word A \in V$
18	16 17	syl	$⊢ φ \to Word A \in V$
19	18	adantr	$⊢ (φ \land g \in F) \to Word A \in V$
20	9	ad2antrr	$⊢ ((φ \land g \in F) \land w \in Word A) \to R \in Grp$
21	5	ssrab3	$⊢ F \subseteq ℤ^{Word A}$
22	21	a1i	$⊢ φ \to F \subseteq ℤ^{Word A}$
23	22	sselda	$⊢ (φ \land g \in F) \to g \in (ℤ^{Word A})$
24		zex	$⊢ ℤ \in V$
25	24	a1i	$⊢ φ \to ℤ \in V$
26	25 18	elmapd	$⊢ φ \to (g \in (ℤ^{Word A}) \leftrightarrow g : Word A ⟶ ℤ)$
27	26	adantr	$⊢ (φ \land g \in F) \to (g \in (ℤ^{Word A}) \leftrightarrow g : Word A ⟶ ℤ)$
28	23 27	mpbid	$⊢ (φ \land g \in F) \to g : Word A ⟶ ℤ$
29	28	ffvelcdmda	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) \in ℤ$
30	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
31	6 30	syl	$⊢ φ \to M \in Mnd$
32		sswrd	$⊢ A \subseteq B \to Word A \subseteq Word B$
33	7 32	syl	$⊢ φ \to Word A \subseteq Word B$
34	33	sselda	$⊢ (φ \land w \in Word A) \to w \in Word B$
35	2 1	mgpbas	$⊢ B = {Base}_{M}$
36	35	gsumwcl	$⊢ (M \in Mnd \land w \in Word B) \to \sum_{M} w \in B$
37	31 34 36	syl2an2r	$⊢ (φ \land w \in Word A) \to \sum_{M} w \in B$
38	37	adantlr	$⊢ ((φ \land g \in F) \land w \in Word A) \to \sum_{M} w \in B$
39	1 3 20 29 38	mulgcld	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
40	39	fmpttd	$⊢ (φ \land g \in F) \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) : Word A ⟶ B$
41		fvexd	$⊢ (φ \land g \in F) \to 0_{R} \in V$
42		0zd	$⊢ (φ \land g \in F) \to 0 \in ℤ$
43		ssidd	$⊢ (φ \land g \in F) \to Word A \subseteq Word A$
44		breq1	$⊢ f = g \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} (g))$
45	44 5	elrab2	$⊢ g \in F \leftrightarrow (g \in (ℤ^{Word A}) \land {finSupp}_{0} (g))$
46	45	simprbi	$⊢ g \in F \to {finSupp}_{0} (g)$
47	46	adantl	$⊢ (φ \land g \in F) \to {finSupp}_{0} (g)$
48	1 11 3	mulg0	$⊢ y \in B \to 0 \underset{˙}{\cdot} y = 0_{R}$
49	48	adantl	$⊢ ((φ \land g \in F) \land y \in B) \to 0 \underset{˙}{\cdot} y = 0_{R}$
50	41 42 19 43 38 28 47 49	fisuppov1	$⊢ (φ \land g \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
51	1 11 13 19 40 50	gsumcl	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in B$
52	51	ad4ant13	$⊢ (((φ \land x \in S) \land g \in F) \land x = \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 B$
53	10 52	eqeltrd	$⊢ (((φ \land x \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to x \in B$
54	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)))$
55		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)))$
56	55	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)))$
57	56	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))$
58	54 57	sylbb	$⊢ x \in S \to \exists g \in F x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
59	58	adantl	$⊢ (φ \land x \in S) \to \exists g \in F x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
60	53 59	r19.29a	$⊢ (φ \land x \in S) \to x \in B$
61	60 1	eleqtrdi	$⊢ (φ \land x \in S) \to x \in {Base}_{R}$
62	61	ex	$⊢ φ \to (x \in S \to x \in {Base}_{R})$
63	62	ssrdv	$⊢ φ \to S \subseteq {Base}_{R}$
64	63 1	sseqtrrdi	$⊢ φ \to S \subseteq B$
65		breq1	$⊢ f = Word A \times \{0\} \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} ((Word A \times \{0\})))$
66		0z	$⊢ 0 \in ℤ$
67	66	fconst6	$⊢ (Word A \times \{0\}) : Word A ⟶ ℤ$
68	67	a1i	$⊢ φ \to (Word A \times \{0\}) : Word A ⟶ ℤ$
69	25 18 68	elmapdd	$⊢ φ \to Word A \times \{0\} \in (ℤ^{Word A})$
70		c0ex	$⊢ 0 \in V$
71	70	a1i	$⊢ φ \to 0 \in V$
72	18 71	fczfsuppd	$⊢ φ \to {finSupp}_{0} ((Word A \times \{0\}))$
73	65 69 72	elrabd	$⊢ φ \to Word A \times \{0\} \in \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
74	73 5	eleqtrrdi	$⊢ φ \to Word A \times \{0\} \in F$
75		simplr	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to g = Word A \times \{0\}$
76	75	fveq1d	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to g (w) = (Word A \times \{0\}) (w)$
77	70	fconst	$⊢ (Word A \times \{0\}) : Word A ⟶ \{0\}$
78	77	a1i	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to (Word A \times \{0\}) : Word A ⟶ \{0\}$
79		simpr	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to w \in Word A$
80		fvconst	$⊢ ((Word A \times \{0\}) : Word A ⟶ \{0\} \land w \in Word A) \to (Word A \times \{0\}) (w) = 0$
81	78 79 80	syl2anc	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to (Word A \times \{0\}) (w) = 0$
82	76 81	eqtrd	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to g (w) = 0$
83	82	oveq1d	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0 \underset{˙}{\cdot} (\sum_{M}, w)$
84	37	adantlr	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to \sum_{M} w \in B$
85	1 11 3	mulg0	$⊢ \sum_{M} w \in B \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
86	84 85	syl	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
87	83 86	eqtrd	$⊢ ((φ \land g = Word A \times \{0\}) \land w \in Word A) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
88	87	mpteq2dva	$⊢ (φ \land g = Word A \times \{0\}) \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ 0_{R})$
89	88	oveq2d	$⊢ (φ \land g = Word A \times \{0\}) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} 0_{R}$
90	12	cmnmndd	$⊢ φ \to R \in Mnd$
91	11	gsumz	$⊢ (R \in Mnd \land Word A \in V) \to \underset{w \in Word A}{\sum_{R}} 0_{R} = 0_{R}$
92	90 18 91	syl2anc	$⊢ φ \to \underset{w \in Word A}{\sum_{R}} 0_{R} = 0_{R}$
93	92	adantr	$⊢ (φ \land g = Word A \times \{0\}) \to \underset{w \in Word A}{\sum_{R}} 0_{R} = 0_{R}$
94	89 93	eqtrd	$⊢ (φ \land g = Word A \times \{0\}) \to \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = 0_{R}$
95	94	eqeq2d	$⊢ (φ \land g = Word A \times \{0\}) \to (0_{R} = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) \leftrightarrow 0_{R} = 0_{R})$
96		eqidd	$⊢ φ \to 0_{R} = 0_{R}$
97	74 95 96	rspcedvd	$⊢ φ \to \exists g \in F 0_{R} = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
98		fvexd	$⊢ φ \to 0_{R} \in V$
99	55 97 98	elrnmptd	$⊢ φ \to 0_{R} \in ran (g \in F ⟼ \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
100	99 8	eleqtrrdi	$⊢ φ \to 0_{R} \in S$
101	100	ne0d	$⊢ φ \to S \neq \emptyset$
102		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))$
103		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))$
104	102 103	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 +_{R} y = (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
105		eqid	$⊢ +_{R} = +_{R}$
106	13	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to R \in CMnd$
107	19	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to Word A \in V$
108	39	adantlr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
109	9	ad2antrr	$⊢ ((φ \land i \in F) \land w \in Word A) \to R \in Grp$
110		breq1	$⊢ f = i \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} (i))$
111	110 5	elrab2	$⊢ i \in F \leftrightarrow (i \in (ℤ^{Word A}) \land {finSupp}_{0} (i))$
112	111	simplbi	$⊢ i \in F \to i \in (ℤ^{Word A})$
113	112	adantl	$⊢ (φ \land i \in F) \to i \in (ℤ^{Word A})$
114	25 18	elmapd	$⊢ φ \to (i \in (ℤ^{Word A}) \leftrightarrow i : Word A ⟶ ℤ)$
115	114	adantr	$⊢ (φ \land i \in F) \to (i \in (ℤ^{Word A}) \leftrightarrow i : Word A ⟶ ℤ)$
116	113 115	mpbid	$⊢ (φ \land i \in F) \to i : Word A ⟶ ℤ$
117	116	ffvelcdmda	$⊢ ((φ \land i \in F) \land w \in Word A) \to i (w) \in ℤ$
118	37	adantlr	$⊢ ((φ \land i \in F) \land w \in Word A) \to \sum_{M} w \in B$
119	1 3 109 117 118	mulgcld	$⊢ ((φ \land i \in F) \land w \in Word A) \to i (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
120	119	adantllr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to i (w) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
121		eqidd	$⊢ ((φ \land g \in F) \land i \in F) \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
122		eqidd	$⊢ ((φ \land g \in F) \land i \in F) \to (w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
123	50	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
124	50	ralrimiva	$⊢ φ \to \forall g \in F {finSupp}_{0_{R}} ((w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
125		fveq1	$⊢ g = i \to g (w) = i (w)$
126	125	oveq1d	$⊢ g = i \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) = i (w) \underset{˙}{\cdot} (\sum_{M}, w)$
127	126	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))$
128	127	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))))$
129	128	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)))$
130	124 129	sylib	$⊢ φ \to \forall i \in F {finSupp}_{0_{R}} ((w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
131	130	r19.21bi	$⊢ (φ \land i \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
132	131	adantlr	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
133	1 11 105 106 107 108 120 121 122 123 132	gsummptfsadd	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{w \in Word A}{\sum_{R}} ((g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) = (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
134	28	ffnd	$⊢ (φ \land g \in F) \to g Fn Word A$
135	134	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to g Fn Word A$
136	116	ffnd	$⊢ (φ \land i \in F) \to i Fn Word A$
137	136	adantlr	$⊢ ((φ \land g \in F) \land i \in F) \to i Fn Word A$
138		inidm	$⊢ Word A \cap Word A = Word A$
139		eqidd	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to g (w) = g (w)$
140		eqidd	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to i (w) = i (w)$
141	135 137 107 107 138 139 140	ofval	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to (g +_{f} i) (w) = g (w) + i (w)$
142	141	oveq1d	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to (g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w) = (g (w) + i (w)) \underset{˙}{\cdot} (\sum_{M}, w)$
143	20	adantlr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to R \in Grp$
144	29	adantlr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to g (w) \in ℤ$
145	117	adantllr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to i (w) \in ℤ$
146	38	adantlr	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to \sum_{M} w \in B$
147	1 3 105	mulgdir	$⊢ (R \in Grp \land (g (w) \in ℤ \land i (w) \in ℤ \land \sum_{M} w \in B)) \to (g (w) + i (w)) \underset{˙}{\cdot} (\sum_{M}, w) = (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
148	143 144 145 146 147	syl13anc	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to (g (w) + i (w)) \underset{˙}{\cdot} (\sum_{M}, w) = (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
149	142 148	eqtr2d	$⊢ (((φ \land g \in F) \land i \in F) \land w \in Word A) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} (i (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w)$
150	149	mpteq2dva	$⊢ ((φ \land g \in F) \land i \in F) \to (w \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) = (w \in Word A ⟼ (g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
151	150	oveq2d	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{w \in Word A}{\sum_{R}} ((g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) = \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
152	133 151	eqtr3d	$⊢ ((φ \land g \in F) \land i \in F) \to (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) = \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
153		fveq1	$⊢ g = h \to g (w) = h (w)$
154	153	oveq1d	$⊢ g = h \to g (w) \underset{˙}{\cdot} (\sum_{M}, w) = h (w) \underset{˙}{\cdot} (\sum_{M}, w)$
155	154	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))$
156	155	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))$
157	156	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)))$
158		fveq1	$⊢ h = g +_{f} i \to h (w) = (g +_{f} i) (w)$
159	158	oveq1d	$⊢ h = g +_{f} i \to h (w) \underset{˙}{\cdot} (\sum_{M}, w) = (g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w)$
160	159	mpteq2dv	$⊢ h = g +_{f} i \to (w \in Word A ⟼ h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ (g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
161	160	oveq2d	$⊢ h = g +_{f} i \to \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
162	161	eqeq2d	$⊢ h = g +_{f} i \to (\underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)) \leftrightarrow \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
163		breq1	$⊢ f = g +_{f} i \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} ((g +_{f} i)))$
164	24	a1i	$⊢ ((φ \land g \in F) \land i \in F) \to ℤ \in V$
165		zaddcl	$⊢ (x \in ℤ \land y \in ℤ) \to x + y \in ℤ$
166	165	adantl	$⊢ (((φ \land g \in F) \land i \in F) \land (x \in ℤ \land y \in ℤ)) \to x + y \in ℤ$
167	28	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to g : Word A ⟶ ℤ$
168	116	adantlr	$⊢ ((φ \land g \in F) \land i \in F) \to i : Word A ⟶ ℤ$
169	166 167 168 107 107 138	off	$⊢ ((φ \land g \in F) \land i \in F) \to (g +_{f} i) : Word A ⟶ ℤ$
170	164 107 169	elmapdd	$⊢ ((φ \land g \in F) \land i \in F) \to g +_{f} i \in (ℤ^{Word A})$
171		zringring	$⊢ ℤ_{ring} \in Ring$
172		ringmnd	$⊢ ℤ_{ring} \in Ring \to ℤ_{ring} \in Mnd$
173	171 172	ax-mp	$⊢ ℤ_{ring} \in Mnd$
174	173	a1i	$⊢ ((φ \land g \in F) \land i \in F) \to ℤ_{ring} \in Mnd$
175	23	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to g \in (ℤ^{Word A})$
176	112	adantl	$⊢ ((φ \land g \in F) \land i \in F) \to i \in (ℤ^{Word A})$
177	47	adantr	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0} (g)$
178		zring0	$⊢ 0 = 0_{ℤ_{ring}}$
179	177 178	breqtrdi	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{ℤ_{ring}}} (g)$
180	111	simprbi	$⊢ i \in F \to {finSupp}_{0} (i)$
181	180	adantl	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0} (i)$
182	181 178	breqtrdi	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{ℤ_{ring}}} (i)$
183		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
184	183	mndpfsupp	$⊢ ((ℤ_{ring} \in Mnd \land Word A \in V) \land (g \in (ℤ^{Word A}) \land i \in (ℤ^{Word A})) \land ({finSupp}_{0_{ℤ_{ring}}} (g) \land {finSupp}_{0_{ℤ_{ring}}} (i))) \to {finSupp}_{0_{ℤ_{ring}}} ((g {+_{ℤ_{ring}}}_{f} i))$
185	174 107 175 176 179 182 184	syl222anc	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0_{ℤ_{ring}}} ((g {+_{ℤ_{ring}}}_{f} i))$
186		zringplusg	$⊢ + = +_{ℤ_{ring}}$
187	186	a1i	$⊢ ((φ \land g \in F) \land i \in F) \to + = +_{ℤ_{ring}}$
188	187	ofeqd	$⊢ ((φ \land g \in F) \land i \in F) \to \circ_{f} + = \circ_{f} +_{ℤ_{ring}}$
189	188	oveqd	$⊢ ((φ \land g \in F) \land i \in F) \to g +_{f} i = g {+_{ℤ_{ring}}}_{f} i$
190	178	a1i	$⊢ ((φ \land g \in F) \land i \in F) \to 0 = 0_{ℤ_{ring}}$
191	185 189 190	3brtr4d	$⊢ ((φ \land g \in F) \land i \in F) \to {finSupp}_{0} ((g +_{f} i))$
192	163 170 191	elrabd	$⊢ ((φ \land g \in F) \land i \in F) \to g +_{f} i \in \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
193	192 5	eleqtrrdi	$⊢ ((φ \land g \in F) \land i \in F) \to g +_{f} i \in F$
194		eqidd	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
195	162 193 194	rspcedvdw	$⊢ ((φ \land g \in F) \land i \in F) \to \exists h \in F \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w))$
196		ovexd	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in V$
197	157 195 196	elrnmptd	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (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)))$
198	197 8	eleqtrrdi	$⊢ ((φ \land g \in F) \land i \in F) \to \underset{w \in Word A}{\sum_{R}} ((g +_{f} i) (w) \underset{˙}{\cdot} (\sum_{M}, w)) \in S$
199	152 198	eqeltrd	$⊢ ((φ \land g \in F) \land i \in F) \to (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \in S$
200	199	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))) +_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \in S$
201	200	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))) +_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \in S$
202	201	ad4ant13	$⊢ ((((((φ \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))) +_{R} (\underset{w \in Word A}{\sum_{R}}, (i (w) \underset{˙}{\cdot} (\sum_{M}, w))) \in S$
203	104 202	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 +_{R} y \in S$
204	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)))$
205	127	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))$
206	205	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)))$
207	206	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)))$
208	207	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))$
209	204 208	sylbb	$⊢ y \in S \to \exists i \in F y = \underset{w \in Word A}{\sum_{R}} (i (w) \underset{˙}{\cdot} (\sum_{M}, w))$
210	209	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))$
211	210	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))$
212	203 211	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 +_{R} y \in S$
213	59	adantr	$⊢ ((φ \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))$
214	212 213	r19.29a	$⊢ ((φ \land x \in S) \land y \in S) \to x +_{R} y \in S$
215	214	ralrimiva	$⊢ (φ \land x \in S) \to \forall y \in S x +_{R} y \in S$
216	9	ad3antrrr	$⊢ (((φ \land x \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to R \in Grp$
217	29	znegcld	$⊢ ((φ \land g \in F) \land w \in Word A) \to - g (w) \in ℤ$
218	1 3 20 217 38	mulgcld	$⊢ ((φ \land g \in F) \land w \in Word A) \to (- g (w)) \underset{˙}{\cdot} (\sum_{M}, w) \in B$
219	218	fmpttd	$⊢ (φ \land g \in F) \to (w \in Word A ⟼ (- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)) : Word A ⟶ B$
220	28	adantr	$⊢ ((φ \land g \in F) \land w \in Word A) \to g : Word A ⟶ ℤ$
221		simpr	$⊢ ((φ \land g \in F) \land w \in Word A) \to w \in Word A$
222	220 221	fvco3d	$⊢ ((φ \land g \in F) \land w \in Word A) \to ((z \in ℤ ⟼ - z) \circ g) (w) = (z \in ℤ ⟼ - z) (g (w))$
223		eqid	$⊢ (z \in ℤ ⟼ - z) = (z \in ℤ ⟼ - z)$
224		negeq	$⊢ z = g (w) \to - z = - g (w)$
225	223 224 29 217	fvmptd3	$⊢ ((φ \land g \in F) \land w \in Word A) \to (z \in ℤ ⟼ - z) (g (w)) = - g (w)$
226	222 225	eqtrd	$⊢ ((φ \land g \in F) \land w \in Word A) \to ((z \in ℤ ⟼ - z) \circ g) (w) = - g (w)$
227	226	oveq1d	$⊢ ((φ \land g \in F) \land w \in Word A) \to ((z \in ℤ ⟼ - z) \circ g) (w) \underset{˙}{\cdot} (\sum_{M}, w) = (- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)$
228	227	mpteq2dva	$⊢ (φ \land g \in F) \to (w \in Word A ⟼ ((z \in ℤ ⟼ - z) \circ g) (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ (- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))$
229		simpr	$⊢ (φ \land z \in ℤ) \to z \in ℤ$
230	229	znegcld	$⊢ (φ \land z \in ℤ) \to - z \in ℤ$
231	230	fmpttd	$⊢ φ \to (z \in ℤ ⟼ - z) : ℤ ⟶ ℤ$
232	231	adantr	$⊢ (φ \land g \in F) \to (z \in ℤ ⟼ - z) : ℤ ⟶ ℤ$
233	232 28	fcod	$⊢ (φ \land g \in F) \to ((z \in ℤ ⟼ - z) \circ g) : Word A ⟶ ℤ$
234	24	a1i	$⊢ (φ \land g \in F) \to ℤ \in V$
235		negeq	$⊢ z = 0 \to - z = - 0$
236		neg0	$⊢ - 0 = 0$
237	235 236	eqtrdi	$⊢ z = 0 \to - z = 0$
238		0zd	$⊢ φ \to 0 \in ℤ$
239	223 237 238 238	fvmptd3	$⊢ φ \to (z \in ℤ ⟼ - z) (0) = 0$
240	239	adantr	$⊢ (φ \land g \in F) \to (z \in ℤ ⟼ - z) (0) = 0$
241	42 28 232 19 234 47 240	fsuppco2	$⊢ (φ \land g \in F) \to {finSupp}_{0} (((z \in ℤ ⟼ - z) \circ g))$
242	41 42 19 43 38 233 241 49	fisuppov1	$⊢ (φ \land g \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ ((z \in ℤ ⟼ - z) \circ g) (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
243	228 242	eqbrtrrd	$⊢ (φ \land g \in F) \to {finSupp}_{0_{R}} ((w \in Word A ⟼ (- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)))$
244	1 11 13 19 219 243	gsumcl	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)) \in B$
245	244	ad4ant13	$⊢ (((φ \land x \in S) \land g \in F) \land x = \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 B$
246	10	oveq1d	$⊢ (((φ \land x \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to x +_{R} (\underset{w \in Word A}{\sum_{R}}, ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (\underset{w \in Word A}{\sum_{R}}, ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)))$
247		eqidd	$⊢ (φ \land g \in F) \to (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ g (w) \underset{˙}{\cdot} (\sum_{M}, w))$
248		eqidd	$⊢ (φ \land g \in F) \to (w \in Word A ⟼ (- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ (- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))$
249	1 11 105 13 19 39 218 247 248 50 243	gsummptfsadd	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} ((g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (\underset{w \in Word A}{\sum_{R}}, ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)))$
250	249	ad4ant13	$⊢ (((φ \land x \in S) \land g \in F) \land x = \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)) +_{R} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = (\underset{w \in Word A}{\sum_{R}}, (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) +_{R} (\underset{w \in Word A}{\sum_{R}}, ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)))$
251	29	zcnd	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) \in ℂ$
252	251	negidd	$⊢ ((φ \land g \in F) \land w \in Word A) \to g (w) + (- g (w)) = 0$
253	252	oveq1d	$⊢ ((φ \land g \in F) \land w \in Word A) \to (g (w) + (- g (w))) \underset{˙}{\cdot} (\sum_{M}, w) = 0 \underset{˙}{\cdot} (\sum_{M}, w)$
254	1 3 105	mulgdir	$⊢ (R \in Grp \land (g (w) \in ℤ \land - g (w) \in ℤ \land \sum_{M} w \in B)) \to (g (w) + (- g (w))) \underset{˙}{\cdot} (\sum_{M}, w) = (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))$
255	20 29 217 38 254	syl13anc	$⊢ ((φ \land g \in F) \land w \in Word A) \to (g (w) + (- g (w))) \underset{˙}{\cdot} (\sum_{M}, w) = (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))$
256	38 85	syl	$⊢ ((φ \land g \in F) \land w \in Word A) \to 0 \underset{˙}{\cdot} (\sum_{M}, w) = 0_{R}$
257	253 255 256	3eqtr3d	$⊢ ((φ \land g \in F) \land w \in Word A) \to (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)) = 0_{R}$
258	257	mpteq2dva	$⊢ (φ \land g \in F) \to (w \in Word A ⟼ (g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = (w \in Word A ⟼ 0_{R})$
259	258	oveq2d	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} ((g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = \underset{w \in Word A}{\sum_{R}} 0_{R}$
260	92	adantr	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} 0_{R} = 0_{R}$
261	259 260	eqtrd	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} ((g (w) \underset{˙}{\cdot} (\sum_{M}, w)) +_{R} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = 0_{R}$
262	261	ad4ant13	$⊢ (((φ \land x \in S) \land g \in F) \land x = \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)) +_{R} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = 0_{R}$
263	246 250 262	3eqtr2d	$⊢ (((φ \land x \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to x +_{R} (\underset{w \in Word A}{\sum_{R}}, ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = 0_{R}$
264		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
265	1 105 11 264	grpinvid1	$⊢ (R \in Grp \land x \in B \land \underset{w \in Word A}{\sum_{R}} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)) \in B) \to ({inv}_{g} (R) (x) = \underset{w \in Word A}{\sum_{R}} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)) \leftrightarrow x +_{R} (\underset{w \in Word A}{\sum_{R}}, ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = 0_{R})$
266	265	biimpar	$⊢ ((R \in Grp \land x \in B \land \underset{w \in Word A}{\sum_{R}} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)) \in B) \land x +_{R} (\underset{w \in Word A}{\sum_{R}}, ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))) = 0_{R}) \to {inv}_{g} (R) (x) = \underset{w \in Word A}{\sum_{R}} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))$
267	216 53 245 263 266	syl31anc	$⊢ (((φ \land x \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to {inv}_{g} (R) (x) = \underset{w \in Word A}{\sum_{R}} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w))$
268		fveq1	$⊢ h = (v \in Word A ⟼ - g (v)) \to h (w) = (v \in Word A ⟼ - g (v)) (w)$
269	268	oveq1d	$⊢ h = (v \in Word A ⟼ - g (v)) \to h (w) \underset{˙}{\cdot} (\sum_{M}, w) = (v \in Word A ⟼ - g (v)) (w) \underset{˙}{\cdot} (\sum_{M}, w)$
270	269	mpteq2dv	$⊢ h = (v \in Word A ⟼ - g (v)) \to (w \in Word A ⟼ h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ (v \in Word A ⟼ - g (v)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
271	270	oveq2d	$⊢ h = (v \in Word A ⟼ - g (v)) \to \underset{w \in Word A}{\sum_{R}} (h (w) \underset{˙}{\cdot} (\sum_{M}, w)) = \underset{w \in Word A}{\sum_{R}} ((v \in Word A ⟼ - g (v)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
272	271	eqeq2d	$⊢ h = (v \in Word A ⟼ - g (v)) \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)) \leftrightarrow \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 ⟼ - g (v)) (w) \underset{˙}{\cdot} (\sum_{M}, w)))$
273		breq1	$⊢ f = (v \in Word A ⟼ - g (v)) \to ({finSupp}_{0} (f) \leftrightarrow {finSupp}_{0} ((v \in Word A ⟼ - g (v))))$
274	28	ffvelcdmda	$⊢ ((φ \land g \in F) \land v \in Word A) \to g (v) \in ℤ$
275	274	znegcld	$⊢ ((φ \land g \in F) \land v \in Word A) \to - g (v) \in ℤ$
276	275	fmpttd	$⊢ (φ \land g \in F) \to (v \in Word A ⟼ - g (v)) : Word A ⟶ ℤ$
277	234 19 276	elmapdd	$⊢ (φ \land g \in F) \to (v \in Word A ⟼ - g (v)) \in (ℤ^{Word A})$
278	276	ffund	$⊢ (φ \land g \in F) \to Fun (v \in Word A ⟼ - g (v))$
279	134	adantr	$⊢ ((φ \land g \in F) \land v \in (Word A ∖ {supp}_{0} (g))) \to g Fn Word A$
280	19	adantr	$⊢ ((φ \land g \in F) \land v \in (Word A ∖ {supp}_{0} (g))) \to Word A \in V$
281		0zd	$⊢ ((φ \land g \in F) \land v \in (Word A ∖ {supp}_{0} (g))) \to 0 \in ℤ$
282		simpr	$⊢ ((φ \land g \in F) \land v \in (Word A ∖ {supp}_{0} (g))) \to v \in (Word A ∖ {supp}_{0} (g))$
283	279 280 281 282	fvdifsupp	$⊢ ((φ \land g \in F) \land v \in (Word A ∖ {supp}_{0} (g))) \to g (v) = 0$
284	283	negeqd	$⊢ ((φ \land g \in F) \land v \in (Word A ∖ {supp}_{0} (g))) \to - g (v) = - 0$
285	284 236	eqtrdi	$⊢ ((φ \land g \in F) \land v \in (Word A ∖ {supp}_{0} (g))) \to - g (v) = 0$
286	285 19	suppss2	$⊢ (φ \land g \in F) \to (v \in Word A ⟼ - g (v)) supp 0 \subseteq g supp 0$
287	277 42 278 47 286	fsuppsssuppgd	$⊢ (φ \land g \in F) \to {finSupp}_{0} ((v \in Word A ⟼ - g (v)))$
288	273 277 287	elrabd	$⊢ (φ \land g \in F) \to (v \in Word A ⟼ - g (v)) \in \{f \in (ℤ^{Word A}) \| {finSupp}_{0} (f)\}$
289	288 5	eleqtrrdi	$⊢ (φ \land g \in F) \to (v \in Word A ⟼ - g (v)) \in F$
290		eqid	$⊢ (v \in Word A ⟼ - g (v)) = (v \in Word A ⟼ - g (v))$
291		fveq2	$⊢ v = w \to g (v) = g (w)$
292	291	negeqd	$⊢ v = w \to - g (v) = - g (w)$
293	290 292 221 217	fvmptd3	$⊢ ((φ \land g \in F) \land w \in Word A) \to (v \in Word A ⟼ - g (v)) (w) = - g (w)$
294	293	eqcomd	$⊢ ((φ \land g \in F) \land w \in Word A) \to - g (w) = (v \in Word A ⟼ - g (v)) (w)$
295	294	oveq1d	$⊢ ((φ \land g \in F) \land w \in Word A) \to (- g (w)) \underset{˙}{\cdot} (\sum_{M}, w) = (v \in Word A ⟼ - g (v)) (w) \underset{˙}{\cdot} (\sum_{M}, w)$
296	295	mpteq2dva	$⊢ (φ \land g \in F) \to (w \in Word A ⟼ (- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)) = (w \in Word A ⟼ (v \in Word A ⟼ - g (v)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
297	296	oveq2d	$⊢ (φ \land g \in F) \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 ⟼ - g (v)) (w) \underset{˙}{\cdot} (\sum_{M}, w))$
298	272 289 297	rspcedvdw	$⊢ (φ \land g \in F) \to \exists h \in F \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))$
299	157 298 244	elrnmptd	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} ((- g (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)))$
300	299 8	eleqtrrdi	$⊢ (φ \land g \in F) \to \underset{w \in Word A}{\sum_{R}} ((- g (w)) \underset{˙}{\cdot} (\sum_{M}, w)) \in S$
301	300	ad4ant13	$⊢ (((φ \land x \in S) \land g \in F) \land x = \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 S$
302	267 301	eqeltrd	$⊢ (((φ \land x \in S) \land g \in F) \land x = \underset{w \in Word A}{\sum_{R}} (g (w) \underset{˙}{\cdot} (\sum_{M}, w))) \to {inv}_{g} (R) (x) \in S$
303	302 59	r19.29a	$⊢ (φ \land x \in S) \to {inv}_{g} (R) (x) \in S$
304	215 303	jca	$⊢ (φ \land x \in S) \to (\forall y \in S x +_{R} y \in S \land {inv}_{g} (R) (x) \in S)$
305	304	ralrimiva	$⊢ φ \to \forall x \in S (\forall y \in S x +_{R} y \in S \land {inv}_{g} (R) (x) \in S)$
306	1 105 264	issubg2	$⊢ R \in Grp \to (S \in SubGrp (R) \leftrightarrow (S \subseteq B \land S \neq \emptyset \land \forall x \in S (\forall y \in S x +_{R} y \in S \land {inv}_{g} (R) (x) \in S)))$
307	306	biimpar	$⊢ (R \in Grp \land (S \subseteq B \land S \neq \emptyset \land \forall x \in S (\forall y \in S x +_{R} y \in S \land {inv}_{g} (R) (x) \in S))) \to S \in SubGrp (R)$
308	9 64 101 305 307	syl13anc	$⊢ φ \to S \in SubGrp (R)$

Metamath Proof Explorer

Theorem elrgspnlem1

Proof