mplcoe5 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mplcoe5		Structured version Unicode version

Theorem mplcoe5 17546

Description: Decompose a monomial into a finite product of powers of variables. Instead of assuming that

is a commutative ring (as in mplcoe2 17547), it is sufficient that

is a ring and all the variables of the multivariate polynomial commute. (Contributed by AV, 7-Oct-2019.)

**Hypotheses**
Ref	Expression
mplcoe1.p	mPoly
mplcoe1.d
mplcoe1.z
mplcoe1.o
mplcoe1.i
mplcoe2.g	mulGrp
mplcoe2.m	._g
mplcoe2.v	mVar
mplcoe5.r
mplcoe5.y
mplcoe5.c

**Assertion**
Ref	Expression
mplcoe5	_g

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem mplcoe5 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplcoe5.y	. . . . . . . . 9
2		mplcoe1.i	. . . . . . . . . 10
3		mplcoe1.d	. . . . . . . . . . 11
4	3	psrbag 17429	. . . . . . . . . 10 $/\$
5	2, 4	syl 16	. . . . . . . . 9 $/\$
6	1, 5	mpbid 210	. . . . . . . 8 $/\$
7	6	simpld 459	. . . . . . 7
8	7	feqmptd 5742	. . . . . 6
9		iftrue 3795	. . . . . . . . 9
10	9	adantl 466	. . . . . . . 8 $/\$ $/\$
11		eldif 3336	. . . . . . . . . 10 $\$ $/\$
12		ifid 3824	. . . . . . . . . . 11
13		frnnn0supp 10631	. . . . . . . . . . . . . . 15 $/\$ supp
14	2, 7, 13	syl2anc 661	. . . . . . . . . . . . . 14 supp
15		eqimss 3406	. . . . . . . . . . . . . 14 supp supp
16	14, 15	syl 16	. . . . . . . . . . . . 13 supp
17		c0ex 9378	. . . . . . . . . . . . . 14
18	17	a1i 11	. . . . . . . . . . . . 13
19	7, 16, 2, 18	suppssr 6718	. . . . . . . . . . . 12 $/\$ $\$
20	19	ifeq2d 3806	. . . . . . . . . . 11 $/\$ $\$
21	12, 20	syl5reqr 2488	. . . . . . . . . 10 $/\$ $\$
22	11, 21	sylan2br 476	. . . . . . . . 9 $/\$ $/\$
23	22	anassrs 648	. . . . . . . 8 $/\$ $/\$
24	10, 23	pm2.61dan 789	. . . . . . 7 $/\$
25	24	mpteq2dva 4376	. . . . . 6
26	8, 25	eqtr4d 2476	. . . . 5
27	26	eqeq2d 2452	. . . 4
28	27	ifbid 3809	. . 3
29	28	mpteq2dv 4377	. 2
30		cnvimass 5187	. . . . 5
31		fdm 5561	. . . . . 6
32	7, 31	syl 16	. . . . 5
33	30, 32	syl5sseq 3402	. . . 4
34	6	simprd 463	. . . . 5
35		sseq1 3375	. . . . . . . 8
36		noel 3639	. . . . . . . . . . . . . . . 16
37		eleq2 2502	. . . . . . . . . . . . . . . 16
38	36, 37	mtbiri 303	. . . . . . . . . . . . . . 15
39		iffalse 3797	. . . . . . . . . . . . . . 15
40	38, 39	syl 16	. . . . . . . . . . . . . 14
41	40	mpteq2dv 4377	. . . . . . . . . . . . 13
42		fconstmpt 4880	. . . . . . . . . . . . 13
43	41, 42	syl6eqr 2491	. . . . . . . . . . . 12
44	43	eqeq2d 2452	. . . . . . . . . . 11
45	44	ifbid 3809	. . . . . . . . . 10
46	45	mpteq2dv 4377	. . . . . . . . 9
47		mpteq1 4370	. . . . . . . . . . . 12
48		mpt0 5536	. . . . . . . . . . . 12
49	47, 48	syl6eq 2489	. . . . . . . . . . 11
50	49	oveq2d 6105	. . . . . . . . . 10 _g _g
51		mplcoe2.g	. . . . . . . . . . . 12 mulGrp
52		eqid 2441	. . . . . . . . . . . 12
53	51, 52	rngidval 16603	. . . . . . . . . . 11
54	53	gsum0 15508	. . . . . . . . . 10 _g
55	50, 54	syl6eq 2489	. . . . . . . . 9 _g
56	46, 55	eqeq12d 2455	. . . . . . . 8 _g
57	35, 56	imbi12d 320	. . . . . . 7 _g
58	57	imbi2d 316	. . . . . 6 _g
59		sseq1 3375	. . . . . . . 8
60		eleq2 2502	. . . . . . . . . . . . . 14
61	60	ifbid 3809	. . . . . . . . . . . . 13
62	61	mpteq2dv 4377	. . . . . . . . . . . 12
63	62	eqeq2d 2452	. . . . . . . . . . 11
64	63	ifbid 3809	. . . . . . . . . 10
65	64	mpteq2dv 4377	. . . . . . . . 9
66		mpteq1 4370	. . . . . . . . . 10
67	66	oveq2d 6105	. . . . . . . . 9 _g _g
68	65, 67	eqeq12d 2455	. . . . . . . 8 _g _g
69	59, 68	imbi12d 320	. . . . . . 7 _g _g
70	69	imbi2d 316	. . . . . 6 _g _g
71		sseq1 3375	. . . . . . . 8
72		eleq2 2502	. . . . . . . . . . . . . 14
73	72	ifbid 3809	. . . . . . . . . . . . 13
74	73	mpteq2dv 4377	. . . . . . . . . . . 12
75	74	eqeq2d 2452	. . . . . . . . . . 11
76	75	ifbid 3809	. . . . . . . . . 10
77	76	mpteq2dv 4377	. . . . . . . . 9
78		mpteq1 4370	. . . . . . . . . 10
79	78	oveq2d 6105	. . . . . . . . 9 _g _g
80	77, 79	eqeq12d 2455	. . . . . . . 8 _g _g
81	71, 80	imbi12d 320	. . . . . . 7 _g _g
82	81	imbi2d 316	. . . . . 6 _g _g
83		sseq1 3375	. . . . . . . 8
84		eleq2 2502	. . . . . . . . . . . . . 14
85	84	ifbid 3809	. . . . . . . . . . . . 13
86	85	mpteq2dv 4377	. . . . . . . . . . . 12
87	86	eqeq2d 2452	. . . . . . . . . . 11
88	87	ifbid 3809	. . . . . . . . . 10
89	88	mpteq2dv 4377	. . . . . . . . 9
90		mpteq1 4370	. . . . . . . . . 10
91	90	oveq2d 6105	. . . . . . . . 9 _g _g
92	89, 91	eqeq12d 2455	. . . . . . . 8 _g _g
93	83, 92	imbi12d 320	. . . . . . 7 _g _g
94	93	imbi2d 316	. . . . . 6 _g _g
95		mplcoe1.p	. . . . . . . . 9 mPoly
96		mplcoe1.z	. . . . . . . . 9
97		mplcoe1.o	. . . . . . . . 9
98		mplcoe5.r	. . . . . . . . 9
99	95, 3, 96, 97, 52, 2, 98	mpl1 17521	. . . . . . . 8
100	99	eqcomd 2446	. . . . . . 7
101	100	a1d 25	. . . . . 6
102		ssun1 3517	. . . . . . . . . . 11
103		sstr2 3361	. . . . . . . . . . 11
104	102, 103	ax-mp 5	. . . . . . . . . 10
105	104	imim1i 58	. . . . . . . . 9 _g _g
106		oveq1 6096	. . . . . . . . . . . 12 _g _g
107		eqid 2441	. . . . . . . . . . . . . . 15
108	2	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
109	98	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
110	7	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
111	110	ffvelrnda 5841	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
112		0nn0 10592	. . . . . . . . . . . . . . . . . 18
113		ifcl 3829	. . . . . . . . . . . . . . . . . 18 $/\$
114	111, 112, 113	sylancl 662	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
115		eqid 2441	. . . . . . . . . . . . . . . . 17
116	114, 115	fmptd 5865	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
117		frnnn0supp 10631	. . . . . . . . . . . . . . . . . 18 $/\$ supp
118	108, 116, 117	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
119		simprll 761	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
120		eldifn 3477	. . . . . . . . . . . . . . . . . . . . 21 $\$
121	120	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
122		iffalse 3797	. . . . . . . . . . . . . . . . . . . 20
123	121, 122	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$
124	123, 108	suppss2 6721	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ supp
125		ssfi 7531	. . . . . . . . . . . . . . . . . 18 $/\$ supp supp
126	119, 124, 125	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
127	118, 126	eqeltrrd 2516	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
128	3	psrbag 17429	. . . . . . . . . . . . . . . . 17 $/\$
129	108, 128	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
130	116, 127, 129	mpbir2and 913	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
131		eqid 2441	. . . . . . . . . . . . . . 15
132		ssun2 3518	. . . . . . . . . . . . . . . . . . 19
133		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
134	132, 133	syl5ss 3365	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		vex 2973	. . . . . . . . . . . . . . . . . . 19
136	135	snss 3997	. . . . . . . . . . . . . . . . . 18
137	134, 136	sylibr 212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
138	110, 137	ffvelrnd 5842	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
139	3	snifpsrbag 17431	. . . . . . . . . . . . . . . 16 $/\$
140	108, 138, 139	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
141	95, 107, 96, 97, 3, 108, 109, 130, 131, 140	mplmonmul 17541	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
142		mplcoe2.m	. . . . . . . . . . . . . . . 16 ._g
143		mplcoe2.v	. . . . . . . . . . . . . . . 16 mVar
144	95, 3, 96, 97, 108, 51, 142, 143, 109, 137, 138	mplcoe3 17543	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
145	144	oveq2d 6105	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	138	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
147		ifcl 3829	. . . . . . . . . . . . . . . . . . . 20 $/\$
148	146, 112, 147	sylancl 662	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
149		eqidd 2442	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
150		eqidd 2442	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
151	108, 114, 148, 149, 150	offval2 6334	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
152	111	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
153	152	nn0cnd 10636	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
154	153	addid2d 9568	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
155		elsni 3900	. . . . . . . . . . . . . . . . . . . . . . . . 25
156	155	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
157		simprlr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
158	157	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
159	156, 158	eqneltrd 2534	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
160	159, 122	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
161		iftrue 3795	. . . . . . . . . . . . . . . . . . . . . . . 24
162	156, 161	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
163	156	fveq2d 5693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
164	162, 163	eqtr4d 2476	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
165	160, 164	oveq12d 6107	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
166		simpr 461	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
167	132, 166	sseldi 3352	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
168		iftrue 3795	. . . . . . . . . . . . . . . . . . . . . 22
169	167, 168	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
170	154, 165, 169	3eqtr4d 2483	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
171	114	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
172	171	nn0cnd 10636	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	addid1d 9567	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
174		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
175		elsn 3889	. . . . . . . . . . . . . . . . . . . . . . . 24
176	174, 175	sylnib 304	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
177		iffalse 3797	. . . . . . . . . . . . . . . . . . . . . . 23
178	176, 177	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
179	178	oveq2d 6105	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
180		biorf 405	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
181		elun 3495	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
182		orcom 387	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$
183	181, 182	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
184	180, 183	syl6rbbr 264	. . . . . . . . . . . . . . . . . . . . . . 23
185	184	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
186	185	ifbid 3809	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
187	173, 179, 186	3eqtr4d 2483	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
188	170, 187	pm2.61dan 789	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
189	188	mpteq2dva 4376	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
190	151, 189	eqtrd 2473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
191	190	eqeq2d 2452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
192	191	ifbid 3809	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
193	192	mpteq2dv 4377	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
194	141, 145, 193	3eqtr3rd 2482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
195	51, 107	mgpbas 16595	. . . . . . . . . . . . . 14
196	51, 131	mgpplusg 16593	. . . . . . . . . . . . . 14
197		eqid 2441	. . . . . . . . . . . . . 14 Cntz Cntz
198		eqid 2441	. . . . . . . . . . . . . 14
199	95	mplrng 17529	. . . . . . . . . . . . . . . . 17 $/\$
200	2, 98, 199	syl2anc 661	. . . . . . . . . . . . . . . 16
201	51	rngmgp 16649	. . . . . . . . . . . . . . . 16
202	200, 201	syl 16	. . . . . . . . . . . . . . 15
203	202	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
204	1	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
205		mplcoe5.c	. . . . . . . . . . . . . . . . 17
206		fveq2 5689	. . . . . . . . . . . . . . . . . . . 20
207	206	oveq2d 6105	. . . . . . . . . . . . . . . . . . 19
208	206	oveq1d 6104	. . . . . . . . . . . . . . . . . . 19
209	207, 208	eqeq12d 2455	. . . . . . . . . . . . . . . . . 18
210		fveq2 5689	. . . . . . . . . . . . . . . . . . . 20
211	210	oveq1d 6104	. . . . . . . . . . . . . . . . . . 19
212	210	oveq2d 6105	. . . . . . . . . . . . . . . . . . 19
213	211, 212	eqeq12d 2455	. . . . . . . . . . . . . . . . . 18
214	209, 213	cbvral2v 2953	. . . . . . . . . . . . . . . . 17
215	205, 214	sylib 196	. . . . . . . . . . . . . . . 16
216	215	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
217	95, 3, 96, 97, 108, 51, 142, 143, 109, 204, 216, 133	mplcoe5lem 17545	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Cntz
218	102, 133	syl5ss 3365	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
219	218	sselda 3354	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
220	202	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
221	7	ffvelrnda 5841	. . . . . . . . . . . . . . . . 17 $/\$
222	2	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
223	98	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
224		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$
225	95, 143, 107, 222, 223, 224	mvrcl 17526	. . . . . . . . . . . . . . . . 17 $/\$
226	195, 142	mulgnn0cl 15641	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
227	220, 221, 225, 226	syl3anc 1218	. . . . . . . . . . . . . . . 16 $/\$
228	227	adantlr 714	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
229	219, 228	syldan 470	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
230	95, 143, 107, 108, 109, 137	mvrcl 17526	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
231	195, 142	mulgnn0cl 15641	. . . . . . . . . . . . . . 15 $/\$ $/\$
232	203, 138, 230, 231	syl3anc 1218	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
233		fveq2 5689	. . . . . . . . . . . . . . . 16
234		fveq2 5689	. . . . . . . . . . . . . . . 16
235	233, 234	oveq12d 6107	. . . . . . . . . . . . . . 15
236	235	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
237	195, 196, 197, 198, 203, 119, 217, 229, 137, 157, 232, 236	gsumzunsnd 16449	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ _g _g
238	194, 237	eqeq12d 2455	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ _g _g
239	106, 238	syl5ibr 221	. . . . . . . . . . 11 $/\$ $/\$ $/\$ _g _g
240	239	expr 615	. . . . . . . . . 10 $/\$ $/\$ _g _g
241	240	a2d 26	. . . . . . . . 9 $/\$ $/\$ _g _g
242	105, 241	syl5 32	. . . . . . . 8 $/\$ $/\$ _g _g
243	242	expcom 435	. . . . . . 7 $/\$ _g _g
244	243	a2d 26	. . . . . 6 $/\$ _g _g
245	58, 70, 82, 94, 101, 244	findcard2s 7551	. . . . 5 _g
246	34, 245	mpcom 36	. . . 4 _g
247	33, 246	mpd 15	. . 3 _g
248		resmpt 5154	. . . . 5
249	33, 248	syl 16	. . . 4
250	249	oveq2d 6105	. . 3 _g _g
251		eqid 2441	. . . . 5
252	227, 251	fmptd 5865	. . . 4
253		ssid 3373	. . . . . 6
254	253	a1i 11	. . . . 5
255	95, 3, 96, 97, 2, 51, 142, 143, 98, 1, 205, 254	mplcoe5lem 17545	. . . 4 Cntz
256	7, 16, 2, 18	suppssr 6718	. . . . . . 7 $/\$ $\$
257	256	oveq1d 6104	. . . . . 6 $/\$ $\$
258		eldifi 3476	. . . . . . . 8 $\$
259	258, 225	sylan2 474	. . . . . . 7 $/\$ $\$
260	195, 53, 142	mulg0 15630	. . . . . . 7
261	259, 260	syl 16	. . . . . 6 $/\$ $\$
262	257, 261	eqtrd 2473	. . . . 5 $/\$ $\$
263	262, 2	suppss2 6721	. . . 4 supp
264		mptexg 5945	. . . . . 6
265	2, 264	syl 16	. . . . 5
266		funmpt 5452	. . . . . 6
267	266	a1i 11	. . . . 5
268		fvex 5699	. . . . . 6
269	268	a1i 11	. . . . 5
270		suppssfifsupp 7633	. . . . 5 $/\$ $/\$ $/\$ $/\$ supp finSupp
271	265, 267, 269, 34, 263, 270	syl32anc 1226	. . . 4 finSupp
272	195, 53, 197, 202, 2, 252, 255, 263, 271	gsumzres 16386	. . 3 _g _g
273	247, 250, 272	3eqtr2d 2479	. 2 _g
274	29, 273	eqtrd 2473	1 _g

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1369

wcel 1756

wral 2713

crab 2717

cvv 2970 $\$ cdif 3323

cun 3324

wss 3326

c0 3635

cif 3789

csn 3875 class class class wbr 4290

cmpt 4348

cxp 4836

ccnv 4837

cdm 4838

cres 4840

cima 4841

wfun 5410

wf 5412

cfv 5416 (class class class)co 6089

cof 6316 supp csupp 6688

cmap 7212

cfn 7308 finSupp cfsupp 7618

cc0 9280

caddc 9283

cn 10320

cn0 10577

cbs 14172

cplusg 14236

cmulr 14237

c0g 14376

_g cgsu 14377

cmnd 15407 ._gcmg 15412 Cntzccntz 15831 mulGrpcmgp 16589

cur 16601

crg 16643 mVar cmvr 17417 mPoly cmpl 17418

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2422 ax-rep 4401 ax-sep 4411 ax-nul 4419 ax-pow 4468 ax-pr 4529 ax-un 6370 ax-inf2 7845 ax-cnex 9336 ax-resscn 9337 ax-1cn 9338 ax-icn 9339 ax-addcl 9340 ax-addrcl 9341 ax-mulcl 9342 ax-mulrcl 9343 ax-mulcom 9344 ax-addass 9345 ax-mulass 9346 ax-distr 9347 ax-i2m1 9348 ax-1ne0 9349 ax-1rid 9350 ax-rnegex 9351 ax-rrecex 9352 ax-cnre 9353 ax-pre-lttri 9354 ax-pre-lttrn 9355 ax-pre-ltadd 9356 ax-pre-mulgt0 9357

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3185 df-csb 3287 df-dif 3329 df-un 3331 df-in 3333 df-ss 3340 df-pss 3342 df-nul 3636 df-if 3790 df-pw 3860 df-sn 3876 df-pr 3878 df-tp 3880 df-op 3882 df-uni 4090 df-int 4127 df-iun 4171 df-iin 4172 df-br 4291 df-opab 4349 df-mpt 4350 df-tr 4384 df-eprel 4630 df-id 4634 df-po 4639 df-so 4640 df-fr 4677 df-se 4678 df-we 4679 df-ord 4720 df-on 4721 df-lim 4722 df-suc 4723 df-xp 4844 df-rel 4845 df-cnv 4846 df-co 4847 df-dm 4848 df-rn 4849 df-res 4850 df-ima 4851 df-iota 5379 df-fun 5418 df-fn 5419 df-f 5420 df-f1 5421 df-fo 5422 df-f1o 5423 df-fv 5424 df-isom 5425 df-riota 6050 df-ov 6092 df-oprab 6093 df-mpt2 6094 df-of 6318 df-ofr 6319 df-om 6475 df-1st 6575 df-2nd 6576 df-supp 6689 df-recs 6830 df-rdg 6864 df-1o 6918 df-2o 6919 df-oadd 6922 df-er 7099 df-map 7214 df-pm 7215 df-ixp 7262 df-en 7309 df-dom 7310 df-sdom 7311 df-fin 7312 df-fsupp 7619 df-oi 7722 df-card 8107 df-pnf 9418 df-mnf 9419 df-xr 9420 df-ltxr 9421 df-le 9422 df-sub 9595 df-neg 9596 df-nn 10321 df-2 10378 df-3 10379 df-4 10380 df-5 10381 df-6 10382 df-7 10383 df-8 10384 df-9 10385 df-n0 10578 df-z 10645 df-uz 10860 df-fz 11436 df-fzo 11547 df-seq 11805 df-hash 12102 df-struct 14174 df-ndx 14175 df-slot 14176 df-base 14177 df-sets 14178 df-ress 14179 df-plusg 14249 df-mulr 14250 df-sca 14252 df-vsca 14253 df-tset 14255 df-0g 14378 df-gsum 14379 df-mre 14522 df-mrc 14523 df-acs 14525 df-mnd 15413 df-mhm 15462 df-submnd 15463 df-grp 15543 df-minusg 15544 df-mulg 15546 df-subg 15676 df-ghm 15743 df-cntz 15833 df-cmn 16277 df-abl 16278 df-mgp 16590 df-ur 16602 df-srg 16606 df-rng 16645 df-subrg 16861 df-psr 17421 df-mvr 17422 df-mpl 17423

This theorem is referenced by: mplcoe2 17547 ply1coe 17744

W3C validator