mplcoe5 - Metamath Proof Explorer

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

Theorem mplcoe5 17895

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

is a commutative ring (as in mplcoe2 17896), 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 17777	. . . . . . . . . 10 $/\$
5	2, 4	syl 16	. . . . . . . . 9 $/\$
6	1, 5	mpbid 210	. . . . . . . 8 $/\$
7	6	simpld 459	. . . . . . 7
8	7	feqmptd 5911	. . . . . 6
9		iftrue 3938	. . . . . . . . 9
10	9	adantl 466	. . . . . . . 8 $/\$ $/\$
11		eldif 3479	. . . . . . . . . 10 $\$ $/\$
12		ifid 3969	. . . . . . . . . . 11
13		frnnn0supp 10838	. . . . . . . . . . . . . . 15 $/\$ supp
14	2, 7, 13	syl2anc 661	. . . . . . . . . . . . . 14 supp
15		eqimss 3549	. . . . . . . . . . . . . 14 supp supp
16	14, 15	syl 16	. . . . . . . . . . . . 13 supp
17		c0ex 9579	. . . . . . . . . . . . . 14
18	17	a1i 11	. . . . . . . . . . . . 13
19	7, 16, 2, 18	suppssr 6921	. . . . . . . . . . . 12 $/\$ $\$
20	19	ifeq2d 3951	. . . . . . . . . . 11 $/\$ $\$
21	12, 20	syl5reqr 2516	. . . . . . . . . 10 $/\$ $\$
22	11, 21	sylan2br 476	. . . . . . . . 9 $/\$ $/\$
23	22	anassrs 648	. . . . . . . 8 $/\$ $/\$
24	10, 23	pm2.61dan 789	. . . . . . 7 $/\$
25	24	mpteq2dva 4526	. . . . . 6
26	8, 25	eqtr4d 2504	. . . . 5
27	26	eqeq2d 2474	. . . 4
28	27	ifbid 3954	. . 3
29	28	mpteq2dv 4527	. 2
30		cnvimass 5348	. . . . 5
31		fdm 5726	. . . . . 6
32	7, 31	syl 16	. . . . 5
33	30, 32	syl5sseq 3545	. . . 4
34	6	simprd 463	. . . . 5
35		sseq1 3518	. . . . . . . 8
36		noel 3782	. . . . . . . . . . . . . . . 16
37		eleq2 2533	. . . . . . . . . . . . . . . 16
38	36, 37	mtbiri 303	. . . . . . . . . . . . . . 15
39		iffalse 3941	. . . . . . . . . . . . . . 15
40	38, 39	syl 16	. . . . . . . . . . . . . 14
41	40	mpteq2dv 4527	. . . . . . . . . . . . 13
42		fconstmpt 5035	. . . . . . . . . . . . 13
43	41, 42	syl6eqr 2519	. . . . . . . . . . . 12
44	43	eqeq2d 2474	. . . . . . . . . . 11
45	44	ifbid 3954	. . . . . . . . . 10
46	45	mpteq2dv 4527	. . . . . . . . 9
47		mpteq1 4520	. . . . . . . . . . . 12
48		mpt0 5699	. . . . . . . . . . . 12
49	47, 48	syl6eq 2517	. . . . . . . . . . 11
50	49	oveq2d 6291	. . . . . . . . . 10 _g _g
51		mplcoe2.g	. . . . . . . . . . . 12 mulGrp
52		eqid 2460	. . . . . . . . . . . 12
53	51, 52	rngidval 16938	. . . . . . . . . . 11
54	53	gsum0 15816	. . . . . . . . . 10 _g
55	50, 54	syl6eq 2517	. . . . . . . . 9 _g
56	46, 55	eqeq12d 2482	. . . . . . . 8 _g
57	35, 56	imbi12d 320	. . . . . . 7 _g
58	57	imbi2d 316	. . . . . 6 _g
59		sseq1 3518	. . . . . . . 8
60		eleq2 2533	. . . . . . . . . . . . . 14
61	60	ifbid 3954	. . . . . . . . . . . . 13
62	61	mpteq2dv 4527	. . . . . . . . . . . 12
63	62	eqeq2d 2474	. . . . . . . . . . 11
64	63	ifbid 3954	. . . . . . . . . 10
65	64	mpteq2dv 4527	. . . . . . . . 9
66		mpteq1 4520	. . . . . . . . . 10
67	66	oveq2d 6291	. . . . . . . . 9 _g _g
68	65, 67	eqeq12d 2482	. . . . . . . 8 _g _g
69	59, 68	imbi12d 320	. . . . . . 7 _g _g
70	69	imbi2d 316	. . . . . 6 _g _g
71		sseq1 3518	. . . . . . . 8
72		eleq2 2533	. . . . . . . . . . . . . 14
73	72	ifbid 3954	. . . . . . . . . . . . 13
74	73	mpteq2dv 4527	. . . . . . . . . . . 12
75	74	eqeq2d 2474	. . . . . . . . . . 11
76	75	ifbid 3954	. . . . . . . . . 10
77	76	mpteq2dv 4527	. . . . . . . . 9
78		mpteq1 4520	. . . . . . . . . 10
79	78	oveq2d 6291	. . . . . . . . 9 _g _g
80	77, 79	eqeq12d 2482	. . . . . . . 8 _g _g
81	71, 80	imbi12d 320	. . . . . . 7 _g _g
82	81	imbi2d 316	. . . . . 6 _g _g
83		sseq1 3518	. . . . . . . 8
84		eleq2 2533	. . . . . . . . . . . . . 14
85	84	ifbid 3954	. . . . . . . . . . . . 13
86	85	mpteq2dv 4527	. . . . . . . . . . . 12
87	86	eqeq2d 2474	. . . . . . . . . . 11
88	87	ifbid 3954	. . . . . . . . . 10
89	88	mpteq2dv 4527	. . . . . . . . 9
90		mpteq1 4520	. . . . . . . . . 10
91	90	oveq2d 6291	. . . . . . . . 9 _g _g
92	89, 91	eqeq12d 2482	. . . . . . . 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 17870	. . . . . . . 8
100	99	eqcomd 2468	. . . . . . 7
101	100	a1d 25	. . . . . 6
102		ssun1 3660	. . . . . . . . . . 11
103		sstr2 3504	. . . . . . . . . . 11
104	102, 103	ax-mp 5	. . . . . . . . . 10
105	104	imim1i 58	. . . . . . . . 9 _g _g
106		oveq1 6282	. . . . . . . . . . . 12 _g _g
107		eqid 2460	. . . . . . . . . . . . . . 15
108	2	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
109	98	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
110	7	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
111	110	ffvelrnda 6012	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
112		0nn0 10799	. . . . . . . . . . . . . . . . . 18
113		ifcl 3974	. . . . . . . . . . . . . . . . . 18 $/\$
114	111, 112, 113	sylancl 662	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
115		eqid 2460	. . . . . . . . . . . . . . . . 17
116	114, 115	fmptd 6036	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
117		frnnn0supp 10838	. . . . . . . . . . . . . . . . . 18 $/\$ supp
118	108, 116, 117	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
119		simprll 761	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
120		eldifn 3620	. . . . . . . . . . . . . . . . . . . . 21 $\$
121	120	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
122		iffalse 3941	. . . . . . . . . . . . . . . . . . . 20
123	121, 122	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$
124	123, 108	suppss2 6924	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ supp
125		ssfi 7730	. . . . . . . . . . . . . . . . . 18 $/\$ supp supp
126	119, 124, 125	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
127	118, 126	eqeltrrd 2549	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
128	3	psrbag 17777	. . . . . . . . . . . . . . . . 17 $/\$
129	108, 128	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
130	116, 127, 129	mpbir2and 915	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
131		eqid 2460	. . . . . . . . . . . . . . 15
132		ssun2 3661	. . . . . . . . . . . . . . . . . . 19
133		simprr 756	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
134	132, 133	syl5ss 3508	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		vex 3109	. . . . . . . . . . . . . . . . . . 19
136	135	snss 4144	. . . . . . . . . . . . . . . . . 18
137	134, 136	sylibr 212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
138	110, 137	ffvelrnd 6013	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
139	3	snifpsrbag 17779	. . . . . . . . . . . . . . . 16 $/\$
140	108, 138, 139	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
141	95, 107, 96, 97, 3, 108, 109, 130, 131, 140	mplmonmul 17890	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
142		mplcoe2.m	. . . . . . . . . . . . . . . 16 ._g
143		mplcoe2.v	. . . . . . . . . . . . . . . 16 mVar
144	95, 3, 96, 97, 108, 51, 142, 143, 109, 137, 138	mplcoe3 17892	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
145	144	oveq2d 6291	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	138	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
147		ifcl 3974	. . . . . . . . . . . . . . . . . . . 20 $/\$
148	146, 112, 147	sylancl 662	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
149		eqidd 2461	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
150		eqidd 2461	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
151	108, 114, 148, 149, 150	offval2 6531	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
152	111	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
153	152	nn0cnd 10843	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
154	153	addid2d 9769	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
155		elsni 4045	. . . . . . . . . . . . . . . . . . . . . . . . 25
156	155	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
157		simprlr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
158	157	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
159	156, 158	eqneltrd 2569	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
160	159, 122	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
161		iftrue 3938	. . . . . . . . . . . . . . . . . . . . . . . 24
162	156, 161	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
163	156	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
164	162, 163	eqtr4d 2504	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
165	160, 164	oveq12d 6293	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
166		simpr 461	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
167	132, 166	sseldi 3495	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
168		iftrue 3938	. . . . . . . . . . . . . . . . . . . . . 22
169	167, 168	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
170	154, 165, 169	3eqtr4d 2511	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
171	114	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
172	171	nn0cnd 10843	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	addid1d 9768	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
174		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
175		elsn 4034	. . . . . . . . . . . . . . . . . . . . . . . 24
176	174, 175	sylnib 304	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
177		iffalse 3941	. . . . . . . . . . . . . . . . . . . . . . 23
178	176, 177	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
179	178	oveq2d 6291	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
180		biorf 405	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
181		elun 3638	. . . . . . . . . . . . . . . . . . . . . . . . 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 3954	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
187	173, 179, 186	3eqtr4d 2511	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
188	170, 187	pm2.61dan 789	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
189	188	mpteq2dva 4526	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
190	151, 189	eqtrd 2501	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
191	190	eqeq2d 2474	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
192	191	ifbid 3954	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
193	192	mpteq2dv 4527	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
194	141, 145, 193	3eqtr3rd 2510	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
195	51, 107	mgpbas 16930	. . . . . . . . . . . . . 14
196	51, 131	mgpplusg 16928	. . . . . . . . . . . . . 14
197		eqid 2460	. . . . . . . . . . . . . 14 Cntz Cntz
198		eqid 2460	. . . . . . . . . . . . . 14
199	95	mplrng 17878	. . . . . . . . . . . . . . . . 17 $/\$
200	2, 98, 199	syl2anc 661	. . . . . . . . . . . . . . . 16
201	51	rngmgp 16985	. . . . . . . . . . . . . . . 16
202	200, 201	syl 16	. . . . . . . . . . . . . . 15
203	202	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
204	1	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
205		mplcoe5.c	. . . . . . . . . . . . . . . . 17
206		fveq2 5857	. . . . . . . . . . . . . . . . . . . 20
207	206	oveq2d 6291	. . . . . . . . . . . . . . . . . . 19
208	206	oveq1d 6290	. . . . . . . . . . . . . . . . . . 19
209	207, 208	eqeq12d 2482	. . . . . . . . . . . . . . . . . 18
210		fveq2 5857	. . . . . . . . . . . . . . . . . . . 20
211	210	oveq1d 6290	. . . . . . . . . . . . . . . . . . 19
212	210	oveq2d 6291	. . . . . . . . . . . . . . . . . . 19
213	211, 212	eqeq12d 2482	. . . . . . . . . . . . . . . . . 18
214	209, 213	cbvral2v 3089	. . . . . . . . . . . . . . . . 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 17894	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Cntz
218	102, 133	syl5ss 3508	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
219	218	sselda 3497	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
220	202	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
221	7	ffvelrnda 6012	. . . . . . . . . . . . . . . . 17 $/\$
222	2	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
223	98	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
224		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$
225	95, 143, 107, 222, 223, 224	mvrcl 17875	. . . . . . . . . . . . . . . . 17 $/\$
226	195, 142	mulgnn0cl 15951	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
227	220, 221, 225, 226	syl3anc 1223	. . . . . . . . . . . . . . . 16 $/\$
228	227	adantlr 714	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
229	219, 228	syldan 470	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
230	95, 143, 107, 108, 109, 137	mvrcl 17875	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
231	195, 142	mulgnn0cl 15951	. . . . . . . . . . . . . . 15 $/\$ $/\$
232	203, 138, 230, 231	syl3anc 1223	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
233		fveq2 5857	. . . . . . . . . . . . . . . 16
234		fveq2 5857	. . . . . . . . . . . . . . . 16
235	233, 234	oveq12d 6293	. . . . . . . . . . . . . . 15
236	235	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
237	195, 196, 197, 198, 203, 119, 217, 229, 137, 157, 232, 236	gsumzunsnd 16766	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ _g _g
238	194, 237	eqeq12d 2482	. . . . . . . . . . . 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 7750	. . . . 5 _g
246	34, 245	mpcom 36	. . . 4 _g
247	33, 246	mpd 15	. . 3 _g
248		resmpt 5314	. . . . 5
249	33, 248	syl 16	. . . 4
250	249	oveq2d 6291	. . 3 _g _g
251		eqid 2460	. . . . 5
252	227, 251	fmptd 6036	. . . 4
253		ssid 3516	. . . . . 6
254	253	a1i 11	. . . . 5
255	95, 3, 96, 97, 2, 51, 142, 143, 98, 1, 205, 254	mplcoe5lem 17894	. . . 4 Cntz
256	7, 16, 2, 18	suppssr 6921	. . . . . . 7 $/\$ $\$
257	256	oveq1d 6290	. . . . . 6 $/\$ $\$
258		eldifi 3619	. . . . . . . 8 $\$
259	258, 225	sylan2 474	. . . . . . 7 $/\$ $\$
260	195, 53, 142	mulg0 15940	. . . . . . 7
261	259, 260	syl 16	. . . . . 6 $/\$ $\$
262	257, 261	eqtrd 2501	. . . . 5 $/\$ $\$
263	262, 2	suppss2 6924	. . . 4 supp
264		mptexg 6121	. . . . . 6
265	2, 264	syl 16	. . . . 5
266		funmpt 5615	. . . . . 6
267	266	a1i 11	. . . . 5
268		fvex 5867	. . . . . 6
269	268	a1i 11	. . . . 5
270		suppssfifsupp 7833	. . . . 5 $/\$ $/\$ $/\$ $/\$ supp finSupp
271	265, 267, 269, 34, 263, 270	syl32anc 1231	. . . 4 finSupp
272	195, 53, 197, 202, 2, 252, 255, 263, 271	gsumzres 16698	. . 3 _g _g
273	247, 250, 272	3eqtr2d 2507	. 2 _g
274	29, 273	eqtrd 2501	1 _g

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1374

wcel 1762

wral 2807

crab 2811

cvv 3106 $\$ cdif 3466

cun 3467

wss 3469

c0 3778

cif 3932

csn 4020 class class class wbr 4440

cmpt 4498

cxp 4990

ccnv 4991

cdm 4992

cres 4994

cima 4995

wfun 5573

wf 5575

cfv 5579 (class class class)co 6275

cof 6513 supp csupp 6891

cmap 7410

cfn 7506 finSupp cfsupp 7818

cc0 9481

caddc 9484

cn 10525

cn0 10784

cbs 14479

cplusg 14544

cmulr 14545

c0g 14684

_g cgsu 14685

cmnd 15715 ._gcmg 15720 Cntzccntz 16141 mulGrpcmgp 16924

cur 16936

crg 16979 mVar cmvr 17765 mPoly cmpl 17766

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-inf2 8047 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-iin 4321 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-se 4832 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-isom 5588 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-of 6515 df-ofr 6516 df-om 6672 df-1st 6774 df-2nd 6775 df-supp 6892 df-recs 7032 df-rdg 7066 df-1o 7120 df-2o 7121 df-oadd 7124 df-er 7301 df-map 7412 df-pm 7413 df-ixp 7460 df-en 7507 df-dom 7508 df-sdom 7509 df-fin 7510 df-fsupp 7819 df-oi 7924 df-card 8309 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9796 df-neg 9797 df-nn 10526 df-2 10583 df-3 10584 df-4 10585 df-5 10586 df-6 10587 df-7 10588 df-8 10589 df-9 10590 df-n0 10785 df-z 10854 df-uz 11072 df-fz 11662 df-fzo 11782 df-seq 12064 df-hash 12361 df-struct 14481 df-ndx 14482 df-slot 14483 df-base 14484 df-sets 14485 df-ress 14486 df-plusg 14557 df-mulr 14558 df-sca 14560 df-vsca 14561 df-tset 14563 df-0g 14686 df-gsum 14687 df-mre 14830 df-mrc 14831 df-acs 14833 df-mnd 15721 df-mhm 15770 df-submnd 15771 df-grp 15851 df-minusg 15852 df-mulg 15854 df-subg 15986 df-ghm 16053 df-cntz 16143 df-cmn 16589 df-abl 16590 df-mgp 16925 df-ur 16937 df-srg 16941 df-rng 16981 df-subrg 17203 df-psr 17769 df-mvr 17770 df-mpl 17771

This theorem is referenced by: mplcoe2 17896 ply1coe 18101

W3C validator