mplcoe5 - Metamath Proof Explorer

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

Theorem mplcoe5 18258

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

is a commutative ring (as in mplcoe2 18259), 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 18140	. . . . . . . . . 10 $/\$
5	2, 4	syl 16	. . . . . . . . 9 $/\$
6	1, 5	mpbid 210	. . . . . . . 8 $/\$
7	6	simpld 459	. . . . . . 7
8	7	feqmptd 5926	. . . . . 6
9		iftrue 3950	. . . . . . . . 9
10	9	adantl 466	. . . . . . . 8 $/\$ $/\$
11		eldif 3481	. . . . . . . . . 10 $\$ $/\$
12		ifid 3981	. . . . . . . . . . 11
13		frnnn0supp 10870	. . . . . . . . . . . . . . 15 $/\$ supp
14	2, 7, 13	syl2anc 661	. . . . . . . . . . . . . 14 supp
15		eqimss 3551	. . . . . . . . . . . . . 14 supp supp
16	14, 15	syl 16	. . . . . . . . . . . . 13 supp
17		c0ex 9607	. . . . . . . . . . . . . 14
18	17	a1i 11	. . . . . . . . . . . . 13
19	7, 16, 2, 18	suppssr 6949	. . . . . . . . . . . 12 $/\$ $\$
20	19	ifeq2d 3963	. . . . . . . . . . 11 $/\$ $\$
21	12, 20	syl5reqr 2513	. . . . . . . . . 10 $/\$ $\$
22	11, 21	sylan2br 476	. . . . . . . . 9 $/\$ $/\$
23	22	anassrs 648	. . . . . . . 8 $/\$ $/\$
24	10, 23	pm2.61dan 791	. . . . . . 7 $/\$
25	24	mpteq2dva 4543	. . . . . 6
26	8, 25	eqtr4d 2501	. . . . 5
27	26	eqeq2d 2471	. . . 4
28	27	ifbid 3966	. . 3
29	28	mpteq2dv 4544	. 2
30		cnvimass 5367	. . . . 5
31		fdm 5741	. . . . . 6
32	7, 31	syl 16	. . . . 5
33	30, 32	syl5sseq 3547	. . . 4
34	6	simprd 463	. . . . 5
35		sseq1 3520	. . . . . . . 8
36		noel 3797	. . . . . . . . . . . . . . . 16
37		eleq2 2530	. . . . . . . . . . . . . . . 16
38	36, 37	mtbiri 303	. . . . . . . . . . . . . . 15
39	38	iffalsed 3955	. . . . . . . . . . . . . 14
40	39	mpteq2dv 4544	. . . . . . . . . . . . 13
41		fconstmpt 5052	. . . . . . . . . . . . 13
42	40, 41	syl6eqr 2516	. . . . . . . . . . . 12
43	42	eqeq2d 2471	. . . . . . . . . . 11
44	43	ifbid 3966	. . . . . . . . . 10
45	44	mpteq2dv 4544	. . . . . . . . 9
46		mpteq1 4537	. . . . . . . . . . . 12
47		mpt0 5714	. . . . . . . . . . . 12
48	46, 47	syl6eq 2514	. . . . . . . . . . 11
49	48	oveq2d 6312	. . . . . . . . . 10 _g _g
50		mplcoe2.g	. . . . . . . . . . . 12 mulGrp
51		eqid 2457	. . . . . . . . . . . 12
52	50, 51	ringidval 17282	. . . . . . . . . . 11
53	52	gsum0 16032	. . . . . . . . . 10 _g
54	49, 53	syl6eq 2514	. . . . . . . . 9 _g
55	45, 54	eqeq12d 2479	. . . . . . . 8 _g
56	35, 55	imbi12d 320	. . . . . . 7 _g
57	56	imbi2d 316	. . . . . 6 _g
58		sseq1 3520	. . . . . . . 8
59		eleq2 2530	. . . . . . . . . . . . . 14
60	59	ifbid 3966	. . . . . . . . . . . . 13
61	60	mpteq2dv 4544	. . . . . . . . . . . 12
62	61	eqeq2d 2471	. . . . . . . . . . 11
63	62	ifbid 3966	. . . . . . . . . 10
64	63	mpteq2dv 4544	. . . . . . . . 9
65		mpteq1 4537	. . . . . . . . . 10
66	65	oveq2d 6312	. . . . . . . . 9 _g _g
67	64, 66	eqeq12d 2479	. . . . . . . 8 _g _g
68	58, 67	imbi12d 320	. . . . . . 7 _g _g
69	68	imbi2d 316	. . . . . 6 _g _g
70		sseq1 3520	. . . . . . . 8
71		eleq2 2530	. . . . . . . . . . . . . 14
72	71	ifbid 3966	. . . . . . . . . . . . 13
73	72	mpteq2dv 4544	. . . . . . . . . . . 12
74	73	eqeq2d 2471	. . . . . . . . . . 11
75	74	ifbid 3966	. . . . . . . . . 10
76	75	mpteq2dv 4544	. . . . . . . . 9
77		mpteq1 4537	. . . . . . . . . 10
78	77	oveq2d 6312	. . . . . . . . 9 _g _g
79	76, 78	eqeq12d 2479	. . . . . . . 8 _g _g
80	70, 79	imbi12d 320	. . . . . . 7 _g _g
81	80	imbi2d 316	. . . . . 6 _g _g
82		sseq1 3520	. . . . . . . 8
83		eleq2 2530	. . . . . . . . . . . . . 14
84	83	ifbid 3966	. . . . . . . . . . . . 13
85	84	mpteq2dv 4544	. . . . . . . . . . . 12
86	85	eqeq2d 2471	. . . . . . . . . . 11
87	86	ifbid 3966	. . . . . . . . . 10
88	87	mpteq2dv 4544	. . . . . . . . 9
89		mpteq1 4537	. . . . . . . . . 10
90	89	oveq2d 6312	. . . . . . . . 9 _g _g
91	88, 90	eqeq12d 2479	. . . . . . . 8 _g _g
92	82, 91	imbi12d 320	. . . . . . 7 _g _g
93	92	imbi2d 316	. . . . . 6 _g _g
94		mplcoe1.p	. . . . . . . . 9 mPoly
95		mplcoe1.z	. . . . . . . . 9
96		mplcoe1.o	. . . . . . . . 9
97		mplcoe5.r	. . . . . . . . 9
98	94, 3, 95, 96, 51, 2, 97	mpl1 18233	. . . . . . . 8
99	98	eqcomd 2465	. . . . . . 7
100	99	a1d 25	. . . . . 6
101		ssun1 3663	. . . . . . . . . . 11
102		sstr2 3506	. . . . . . . . . . 11
103	101, 102	ax-mp 5	. . . . . . . . . 10
104	103	imim1i 58	. . . . . . . . 9 _g _g
105		oveq1 6303	. . . . . . . . . . . 12 _g _g
106		eqid 2457	. . . . . . . . . . . . . . 15
107	2	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
108	97	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
109	7	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
110	109	ffvelrnda 6032	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
111		0nn0 10831	. . . . . . . . . . . . . . . . . 18
112		ifcl 3986	. . . . . . . . . . . . . . . . . 18 $/\$
113	110, 111, 112	sylancl 662	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
114		eqid 2457	. . . . . . . . . . . . . . . . 17
115	113, 114	fmptd 6056	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
116		frnnn0supp 10870	. . . . . . . . . . . . . . . . . 18 $/\$ supp
117	107, 115, 116	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
118		simprll 763	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
119		eldifn 3623	. . . . . . . . . . . . . . . . . . . . 21 $\$
120	119	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
121	120	iffalsed 3955	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$
122	121, 107	suppss2 6952	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ supp
123		ssfi 7759	. . . . . . . . . . . . . . . . . 18 $/\$ supp supp
124	118, 122, 123	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
125	117, 124	eqeltrrd 2546	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	3	psrbag 18140	. . . . . . . . . . . . . . . . 17 $/\$
127	107, 126	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	115, 125, 127	mpbir2and 922	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129		eqid 2457	. . . . . . . . . . . . . . 15
130		ssun2 3664	. . . . . . . . . . . . . . . . . . 19
131		simprr 757	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
132	130, 131	syl5ss 3510	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
133		vex 3112	. . . . . . . . . . . . . . . . . . 19
134	133	snss 4156	. . . . . . . . . . . . . . . . . 18
135	132, 134	sylibr 212	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
136	109, 135	ffvelrnd 6033	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	3	snifpsrbag 18142	. . . . . . . . . . . . . . . 16 $/\$
138	107, 136, 137	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	94, 106, 95, 96, 3, 107, 108, 128, 129, 138	mplmonmul 18253	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140		mplcoe2.m	. . . . . . . . . . . . . . . 16 ._g
141		mplcoe2.v	. . . . . . . . . . . . . . . 16 mVar
142	94, 3, 95, 96, 107, 50, 140, 141, 108, 135, 136	mplcoe3 18255	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
143	142	oveq2d 6312	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	136	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
145		ifcl 3986	. . . . . . . . . . . . . . . . . . . 20 $/\$
146	144, 111, 145	sylancl 662	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
147		eqidd 2458	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
148		eqidd 2458	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
149	107, 113, 146, 147, 148	offval2 6555	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
150	110	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
151	150	nn0cnd 10875	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
152	151	addid2d 9798	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
153		elsni 4057	. . . . . . . . . . . . . . . . . . . . . . . . 25
154	153	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
155		simprlr 764	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156	155	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
157	154, 156	eqneltrd 2566	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
158	157	iffalsed 3955	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
159	154	iftrued 3952	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
160	154	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
161	159, 160	eqtr4d 2501	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	158, 161	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
163		simpr 461	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
164	130, 163	sseldi 3497	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
165	164	iftrued 3952	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
166	152, 162, 165	3eqtr4d 2508	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
167	113	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
168	167	nn0cnd 10875	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	addid1d 9797	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
170		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
171		elsn 4046	. . . . . . . . . . . . . . . . . . . . . . . 24
172	170, 171	sylnib 304	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	iffalsed 3955	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
174	173	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
175		biorf 405	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
176		elun 3641	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
177		orcom 387	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$
178	176, 177	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
179	175, 178	syl6rbbr 264	. . . . . . . . . . . . . . . . . . . . . . 23
180	179	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
181	180	ifbid 3966	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
182	169, 174, 181	3eqtr4d 2508	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
183	166, 182	pm2.61dan 791	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
184	183	mpteq2dva 4543	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185	149, 184	eqtrd 2498	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
186	185	eqeq2d 2471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
187	186	ifbid 3966	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188	187	mpteq2dv 4544	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
189	139, 143, 188	3eqtr3rd 2507	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
190	50, 106	mgpbas 17274	. . . . . . . . . . . . . 14
191	50, 129	mgpplusg 17272	. . . . . . . . . . . . . 14
192		eqid 2457	. . . . . . . . . . . . . 14 Cntz Cntz
193		eqid 2457	. . . . . . . . . . . . . 14
194	94	mplring 18241	. . . . . . . . . . . . . . . . 17 $/\$
195	2, 97, 194	syl2anc 661	. . . . . . . . . . . . . . . 16
196	50	ringmgp 17331	. . . . . . . . . . . . . . . 16
197	195, 196	syl 16	. . . . . . . . . . . . . . 15
198	197	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
199	1	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
200		mplcoe5.c	. . . . . . . . . . . . . . . . 17
201		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20
202	201	oveq2d 6312	. . . . . . . . . . . . . . . . . . 19
203	201	oveq1d 6311	. . . . . . . . . . . . . . . . . . 19
204	202, 203	eqeq12d 2479	. . . . . . . . . . . . . . . . . 18
205		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20
206	205	oveq1d 6311	. . . . . . . . . . . . . . . . . . 19
207	205	oveq2d 6312	. . . . . . . . . . . . . . . . . . 19
208	206, 207	eqeq12d 2479	. . . . . . . . . . . . . . . . . 18
209	204, 208	cbvral2v 3092	. . . . . . . . . . . . . . . . 17
210	200, 209	sylib 196	. . . . . . . . . . . . . . . 16
211	210	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
212	94, 3, 95, 96, 107, 50, 140, 141, 108, 199, 211, 131	mplcoe5lem 18257	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Cntz
213	101, 131	syl5ss 3510	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	213	sselda 3499	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
215	197	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
216	7	ffvelrnda 6032	. . . . . . . . . . . . . . . . 17 $/\$
217	2	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
218	97	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
219		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$
220	94, 141, 106, 217, 218, 219	mvrcl 18238	. . . . . . . . . . . . . . . . 17 $/\$
221	190, 140	mulgnn0cl 16285	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
222	215, 216, 220, 221	syl3anc 1228	. . . . . . . . . . . . . . . 16 $/\$
223	222	adantlr 714	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
224	214, 223	syldan 470	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
225	94, 141, 106, 107, 108, 135	mvrcl 18238	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	190, 140	mulgnn0cl 16285	. . . . . . . . . . . . . . 15 $/\$ $/\$
227	198, 136, 225, 226	syl3anc 1228	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
228		fveq2 5872	. . . . . . . . . . . . . . . 16
229		fveq2 5872	. . . . . . . . . . . . . . . 16
230	228, 229	oveq12d 6314	. . . . . . . . . . . . . . 15
231	230	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
232	190, 191, 192, 193, 198, 118, 212, 224, 135, 155, 227, 231	gsumzunsnd 17109	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ _g _g
233	189, 232	eqeq12d 2479	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ _g _g
234	105, 233	syl5ibr 221	. . . . . . . . . . 11 $/\$ $/\$ $/\$ _g _g
235	234	expr 615	. . . . . . . . . 10 $/\$ $/\$ _g _g
236	235	a2d 26	. . . . . . . . 9 $/\$ $/\$ _g _g
237	104, 236	syl5 32	. . . . . . . 8 $/\$ $/\$ _g _g
238	237	expcom 435	. . . . . . 7 $/\$ _g _g
239	238	a2d 26	. . . . . 6 $/\$ _g _g
240	57, 69, 81, 93, 100, 239	findcard2s 7779	. . . . 5 _g
241	34, 240	mpcom 36	. . . 4 _g
242	33, 241	mpd 15	. . 3 _g
243	33	resmptd 5335	. . . 4
244	243	oveq2d 6312	. . 3 _g _g
245		eqid 2457	. . . . 5
246	222, 245	fmptd 6056	. . . 4
247		ssid 3518	. . . . . 6
248	247	a1i 11	. . . . 5
249	94, 3, 95, 96, 2, 50, 140, 141, 97, 1, 200, 248	mplcoe5lem 18257	. . . 4 Cntz
250	7, 16, 2, 18	suppssr 6949	. . . . . . 7 $/\$ $\$
251	250	oveq1d 6311	. . . . . 6 $/\$ $\$
252		eldifi 3622	. . . . . . . 8 $\$
253	252, 220	sylan2 474	. . . . . . 7 $/\$ $\$
254	190, 52, 140	mulg0 16274	. . . . . . 7
255	253, 254	syl 16	. . . . . 6 $/\$ $\$
256	251, 255	eqtrd 2498	. . . . 5 $/\$ $\$
257	256, 2	suppss2 6952	. . . 4 supp
258		mptexg 6143	. . . . . 6
259	2, 258	syl 16	. . . . 5
260		funmpt 5630	. . . . . 6
261	260	a1i 11	. . . . 5
262		fvex 5882	. . . . . 6
263	262	a1i 11	. . . . 5
264		suppssfifsupp 7862	. . . . 5 $/\$ $/\$ $/\$ $/\$ supp finSupp
265	259, 261, 263, 34, 257, 264	syl32anc 1236	. . . 4 finSupp
266	190, 52, 192, 197, 2, 246, 249, 257, 265	gsumzres 17041	. . 3 _g _g
267	242, 244, 266	3eqtr2d 2504	. 2 _g
268	29, 267	eqtrd 2498	1 _g

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1395

wcel 1819

wral 2807

crab 2811

cvv 3109 $\$ cdif 3468

cun 3469

wss 3471

c0 3793

cif 3944

csn 4032 class class class wbr 4456

cmpt 4515

cxp 5006

ccnv 5007

cdm 5008

cres 5010

cima 5011

wfun 5588

wf 5590

cfv 5594 (class class class)co 6296

cof 6537 supp csupp 6917

cmap 7438

cfn 7535 finSupp cfsupp 7847

cc0 9509

caddc 9512

cn 10556

cn0 10816

cbs 14644

cplusg 14712

cmulr 14713

c0g 14857

_g cgsu 14858

cmnd 16046 ._gcmg 16183 Cntzccntz 16480 mulGrpcmgp 17268

cur 17280

crg 17325 mVar cmvr 18128 mPoly cmpl 18129

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-iin 4335 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-ofr 6540 df-om 6700 df-1st 6799 df-2nd 6800 df-supp 6918 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-ixp 7489 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fsupp 7848 df-oi 7953 df-card 8337 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-n0 10817 df-z 10886 df-uz 11107 df-fz 11698 df-fzo 11822 df-seq 12111 df-hash 12409 df-struct 14646 df-ndx 14647 df-slot 14648 df-base 14649 df-sets 14650 df-ress 14651 df-plusg 14725 df-mulr 14726 df-sca 14728 df-vsca 14729 df-tset 14731 df-0g 14859 df-gsum 14860 df-mre 15003 df-mrc 15004 df-acs 15006 df-mgm 15999 df-sgrp 16038 df-mnd 16048 df-mhm 16093 df-submnd 16094 df-grp 16184 df-minusg 16185 df-mulg 16187 df-subg 16325 df-ghm 16392 df-cntz 16482 df-cmn 16927 df-abl 16928 df-mgp 17269 df-ur 17281 df-srg 17285 df-ring 17327 df-subrg 17554 df-psr 18132 df-mvr 18133 df-mpl 18134

This theorem is referenced by: mplcoe2 18259 ply1coe 18464

W3C validator