mplcoe5 - Metamath Proof Explorer

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

Theorem mplcoe5 18769

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

is a commutative ring (as in mplcoe2 18770), 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 18665	. . . . . . . . . 10 $/\$
5	2, 4	syl 17	. . . . . . . . 9 $/\$
6	1, 5	mpbid 215	. . . . . . . 8 $/\$
7	6	simpld 466	. . . . . . 7
8	7	feqmptd 5932	. . . . . 6
9		iftrue 3878	. . . . . . . . 9
10	9	adantl 473	. . . . . . . 8 $/\$ $/\$
11		eldif 3400	. . . . . . . . . 10 $\$ $/\$
12		ifid 3909	. . . . . . . . . . 11
13		frnnn0supp 10947	. . . . . . . . . . . . . . 15 $/\$ supp
14	2, 7, 13	syl2anc 673	. . . . . . . . . . . . . 14 supp
15		eqimss 3470	. . . . . . . . . . . . . 14 supp supp
16	14, 15	syl 17	. . . . . . . . . . . . 13 supp
17		c0ex 9655	. . . . . . . . . . . . . 14
18	17	a1i 11	. . . . . . . . . . . . 13
19	7, 16, 2, 18	suppssr 6965	. . . . . . . . . . . 12 $/\$ $\$
20	19	ifeq2d 3891	. . . . . . . . . . 11 $/\$ $\$
21	12, 20	syl5reqr 2520	. . . . . . . . . 10 $/\$ $\$
22	11, 21	sylan2br 484	. . . . . . . . 9 $/\$ $/\$
23	22	anassrs 660	. . . . . . . 8 $/\$ $/\$
24	10, 23	pm2.61dan 808	. . . . . . 7 $/\$
25	24	mpteq2dva 4482	. . . . . 6
26	8, 25	eqtr4d 2508	. . . . 5
27	26	eqeq2d 2481	. . . 4
28	27	ifbid 3894	. . 3
29	28	mpteq2dv 4483	. 2
30		cnvimass 5194	. . . . 5
31		fdm 5745	. . . . . 6
32	7, 31	syl 17	. . . . 5
33	30, 32	syl5sseq 3466	. . . 4
34	6	simprd 470	. . . . 5
35		sseq1 3439	. . . . . . . 8
36		noel 3726	. . . . . . . . . . . . . . . 16
37		eleq2 2538	. . . . . . . . . . . . . . . 16
38	36, 37	mtbiri 310	. . . . . . . . . . . . . . 15
39	38	iffalsed 3883	. . . . . . . . . . . . . 14
40	39	mpteq2dv 4483	. . . . . . . . . . . . 13
41		fconstmpt 4883	. . . . . . . . . . . . 13
42	40, 41	syl6eqr 2523	. . . . . . . . . . . 12
43	42	eqeq2d 2481	. . . . . . . . . . 11
44	43	ifbid 3894	. . . . . . . . . 10
45	44	mpteq2dv 4483	. . . . . . . . 9
46		mpteq1 4476	. . . . . . . . . . . 12
47		mpt0 5715	. . . . . . . . . . . 12
48	46, 47	syl6eq 2521	. . . . . . . . . . 11
49	48	oveq2d 6324	. . . . . . . . . 10 _g _g
50		mplcoe2.g	. . . . . . . . . . . 12 mulGrp
51		eqid 2471	. . . . . . . . . . . 12
52	50, 51	ringidval 17815	. . . . . . . . . . 11
53	52	gsum0 16599	. . . . . . . . . 10 _g
54	49, 53	syl6eq 2521	. . . . . . . . 9 _g
55	45, 54	eqeq12d 2486	. . . . . . . 8 _g
56	35, 55	imbi12d 327	. . . . . . 7 _g
57	56	imbi2d 323	. . . . . 6 _g
58		sseq1 3439	. . . . . . . 8
59		eleq2 2538	. . . . . . . . . . . . . 14
60	59	ifbid 3894	. . . . . . . . . . . . 13
61	60	mpteq2dv 4483	. . . . . . . . . . . 12
62	61	eqeq2d 2481	. . . . . . . . . . 11
63	62	ifbid 3894	. . . . . . . . . 10
64	63	mpteq2dv 4483	. . . . . . . . 9
65		mpteq1 4476	. . . . . . . . . 10
66	65	oveq2d 6324	. . . . . . . . 9 _g _g
67	64, 66	eqeq12d 2486	. . . . . . . 8 _g _g
68	58, 67	imbi12d 327	. . . . . . 7 _g _g
69	68	imbi2d 323	. . . . . 6 _g _g
70		sseq1 3439	. . . . . . . 8
71		eleq2 2538	. . . . . . . . . . . . . 14
72	71	ifbid 3894	. . . . . . . . . . . . 13
73	72	mpteq2dv 4483	. . . . . . . . . . . 12
74	73	eqeq2d 2481	. . . . . . . . . . 11
75	74	ifbid 3894	. . . . . . . . . 10
76	75	mpteq2dv 4483	. . . . . . . . 9
77		mpteq1 4476	. . . . . . . . . 10
78	77	oveq2d 6324	. . . . . . . . 9 _g _g
79	76, 78	eqeq12d 2486	. . . . . . . 8 _g _g
80	70, 79	imbi12d 327	. . . . . . 7 _g _g
81	80	imbi2d 323	. . . . . 6 _g _g
82		sseq1 3439	. . . . . . . 8
83		eleq2 2538	. . . . . . . . . . . . . 14
84	83	ifbid 3894	. . . . . . . . . . . . 13
85	84	mpteq2dv 4483	. . . . . . . . . . . 12
86	85	eqeq2d 2481	. . . . . . . . . . 11
87	86	ifbid 3894	. . . . . . . . . 10
88	87	mpteq2dv 4483	. . . . . . . . 9
89		mpteq1 4476	. . . . . . . . . 10
90	89	oveq2d 6324	. . . . . . . . 9 _g _g
91	88, 90	eqeq12d 2486	. . . . . . . 8 _g _g
92	82, 91	imbi12d 327	. . . . . . 7 _g _g
93	92	imbi2d 323	. . . . . 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 18745	. . . . . . . 8
99	98	eqcomd 2477	. . . . . . 7
100	99	a1d 25	. . . . . 6
101		ssun1 3588	. . . . . . . . . . 11
102		sstr2 3425	. . . . . . . . . . 11
103	101, 102	ax-mp 5	. . . . . . . . . 10
104	103	imim1i 59	. . . . . . . . 9 _g _g
105		oveq1 6315	. . . . . . . . . . . 12 _g _g
106		eqid 2471	. . . . . . . . . . . . . . 15
107	2	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
108	97	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
109	7	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
110	109	ffvelrnda 6037	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
111		0nn0 10908	. . . . . . . . . . . . . . . . . 18
112		ifcl 3914	. . . . . . . . . . . . . . . . . 18 $/\$
113	110, 111, 112	sylancl 675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
114		eqid 2471	. . . . . . . . . . . . . . . . 17
115	113, 114	fmptd 6061	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
116		frnnn0supp 10947	. . . . . . . . . . . . . . . . . 18 $/\$ supp
117	107, 115, 116	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
118		simprll 780	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
119		eldifn 3545	. . . . . . . . . . . . . . . . . . . . 21 $\$
120	119	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
121	120	iffalsed 3883	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$
122	121, 107	suppss2 6968	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ supp
123		ssfi 7810	. . . . . . . . . . . . . . . . . 18 $/\$ supp supp
124	118, 122, 123	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
125	117, 124	eqeltrrd 2550	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	3	psrbag 18665	. . . . . . . . . . . . . . . . 17 $/\$
127	107, 126	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	115, 125, 127	mpbir2and 936	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129		eqid 2471	. . . . . . . . . . . . . . 15
130		ssun2 3589	. . . . . . . . . . . . . . . . . . 19
131		simprr 774	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
132	130, 131	syl5ss 3429	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
133		vex 3034	. . . . . . . . . . . . . . . . . . 19
134	133	snss 4087	. . . . . . . . . . . . . . . . . 18
135	132, 134	sylibr 217	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
136	109, 135	ffvelrnd 6038	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	3	snifpsrbag 18667	. . . . . . . . . . . . . . . 16 $/\$
138	107, 136, 137	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	94, 106, 95, 96, 3, 107, 108, 128, 129, 138	mplmonmul 18765	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140		mplcoe2.m	. . . . . . . . . . . . . . . 16 ._g
141		mplcoe2.v	. . . . . . . . . . . . . . . 16 mVar
142	94, 3, 95, 96, 107, 50, 140, 141, 108, 135, 136	mplcoe3 18767	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
143	142	oveq2d 6324	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	136	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
145		ifcl 3914	. . . . . . . . . . . . . . . . . . . 20 $/\$
146	144, 111, 145	sylancl 675	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
147		eqidd 2472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
148		eqidd 2472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
149	107, 113, 146, 147, 148	offval2 6567	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
150	110	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
151	150	nn0cnd 10951	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
152	151	addid2d 9852	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
153		elsni 3985	. . . . . . . . . . . . . . . . . . . . . . . . 25
154	153	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
155		simprlr 781	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156	155	ad2antrr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
157	154, 156	eqneltrd 2568	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
158	157	iffalsed 3883	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
159	154	iftrued 3880	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
160	154	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
161	159, 160	eqtr4d 2508	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	158, 161	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
163		simpr 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
164	130, 163	sseldi 3416	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
165	164	iftrued 3880	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
166	152, 162, 165	3eqtr4d 2515	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
167	113	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
168	167	nn0cnd 10951	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	addid1d 9851	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
170		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
171		elsn 3973	. . . . . . . . . . . . . . . . . . . . . . . 24
172	170, 171	sylnib 311	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	iffalsed 3883	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
174	173	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
175		biorf 412	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
176		elun 3565	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
177		orcom 394	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$
178	176, 177	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
179	175, 178	syl6rbbr 272	. . . . . . . . . . . . . . . . . . . . . . 23
180	179	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
181	180	ifbid 3894	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
182	169, 174, 181	3eqtr4d 2515	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
183	166, 182	pm2.61dan 808	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
184	183	mpteq2dva 4482	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185	149, 184	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
186	185	eqeq2d 2481	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
187	186	ifbid 3894	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188	187	mpteq2dv 4483	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
189	139, 143, 188	3eqtr3rd 2514	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
190	50, 106	mgpbas 17807	. . . . . . . . . . . . . 14
191	50, 129	mgpplusg 17805	. . . . . . . . . . . . . 14
192		eqid 2471	. . . . . . . . . . . . . 14 Cntz Cntz
193		eqid 2471	. . . . . . . . . . . . . 14
194	94	mplring 18753	. . . . . . . . . . . . . . . . 17 $/\$
195	2, 97, 194	syl2anc 673	. . . . . . . . . . . . . . . 16
196	50	ringmgp 17864	. . . . . . . . . . . . . . . 16
197	195, 196	syl 17	. . . . . . . . . . . . . . 15
198	197	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
199	1	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
200		mplcoe5.c	. . . . . . . . . . . . . . . . 17
201		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
202	201	oveq2d 6324	. . . . . . . . . . . . . . . . . . 19
203	201	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19
204	202, 203	eqeq12d 2486	. . . . . . . . . . . . . . . . . 18
205		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
206	205	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19
207	205	oveq2d 6324	. . . . . . . . . . . . . . . . . . 19
208	206, 207	eqeq12d 2486	. . . . . . . . . . . . . . . . . 18
209	204, 208	cbvral2v 3013	. . . . . . . . . . . . . . . . 17
210	200, 209	sylib 201	. . . . . . . . . . . . . . . 16
211	210	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
212	94, 3, 95, 96, 107, 50, 140, 141, 108, 199, 211, 131	mplcoe5lem 18768	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Cntz
213	101, 131	syl5ss 3429	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	213	sselda 3418	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
215	197	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$
216	7	ffvelrnda 6037	. . . . . . . . . . . . . . . . 17 $/\$
217	2	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
218	97	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
219		simpr 468	. . . . . . . . . . . . . . . . . 18 $/\$
220	94, 141, 106, 217, 218, 219	mvrcl 18750	. . . . . . . . . . . . . . . . 17 $/\$
221	190, 140	mulgnn0cl 16852	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
222	215, 216, 220, 221	syl3anc 1292	. . . . . . . . . . . . . . . 16 $/\$
223	222	adantlr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
224	214, 223	syldan 478	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
225	94, 141, 106, 107, 108, 135	mvrcl 18750	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	190, 140	mulgnn0cl 16852	. . . . . . . . . . . . . . 15 $/\$ $/\$
227	198, 136, 225, 226	syl3anc 1292	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
228		fveq2 5879	. . . . . . . . . . . . . . . 16
229		fveq2 5879	. . . . . . . . . . . . . . . 16
230	228, 229	oveq12d 6326	. . . . . . . . . . . . . . 15
231	230	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
232	190, 191, 192, 193, 198, 118, 212, 224, 135, 155, 227, 231	gsumzunsnd 17666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ _g _g
233	189, 232	eqeq12d 2486	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ _g _g
234	105, 233	syl5ibr 229	. . . . . . . . . . 11 $/\$ $/\$ $/\$ _g _g
235	234	expr 626	. . . . . . . . . 10 $/\$ $/\$ _g _g
236	235	a2d 28	. . . . . . . . 9 $/\$ $/\$ _g _g
237	104, 236	syl5 32	. . . . . . . 8 $/\$ $/\$ _g _g
238	237	expcom 442	. . . . . . 7 $/\$ _g _g
239	238	a2d 28	. . . . . 6 $/\$ _g _g
240	57, 69, 81, 93, 100, 239	findcard2s 7830	. . . . 5 _g
241	34, 240	mpcom 36	. . . 4 _g
242	33, 241	mpd 15	. . 3 _g
243	33	resmptd 5162	. . . 4
244	243	oveq2d 6324	. . 3 _g _g
245		eqid 2471	. . . . 5
246	222, 245	fmptd 6061	. . . 4
247		ssid 3437	. . . . . 6
248	247	a1i 11	. . . . 5
249	94, 3, 95, 96, 2, 50, 140, 141, 97, 1, 200, 248	mplcoe5lem 18768	. . . 4 Cntz
250	7, 16, 2, 18	suppssr 6965	. . . . . . 7 $/\$ $\$
251	250	oveq1d 6323	. . . . . 6 $/\$ $\$
252		eldifi 3544	. . . . . . . 8 $\$
253	252, 220	sylan2 482	. . . . . . 7 $/\$ $\$
254	190, 52, 140	mulg0 16841	. . . . . . 7
255	253, 254	syl 17	. . . . . 6 $/\$ $\$
256	251, 255	eqtrd 2505	. . . . 5 $/\$ $\$
257	256, 2	suppss2 6968	. . . 4 supp
258		mptexg 6151	. . . . . 6
259	2, 258	syl 17	. . . . 5
260		funmpt 5625	. . . . . 6
261	260	a1i 11	. . . . 5
262		fvex 5889	. . . . . 6
263	262	a1i 11	. . . . 5
264		suppssfifsupp 7916	. . . . 5 $/\$ $/\$ $/\$ $/\$ supp finSupp
265	259, 261, 263, 34, 257, 264	syl32anc 1300	. . . 4 finSupp
266	190, 52, 192, 197, 2, 246, 249, 257, 265	gsumzres 17621	. . 3 _g _g
267	242, 244, 266	3eqtr2d 2511	. 2 _g
268	29, 267	eqtrd 2505	1 _g

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376

wceq 1452

wcel 1904

wral 2756

crab 2760

cvv 3031 $\$ cdif 3387

cun 3388

wss 3390

c0 3722

cif 3872

csn 3959 class class class wbr 4395

cmpt 4454

cxp 4837

ccnv 4838

cdm 4839

cres 4841

cima 4842

wfun 5583

wf 5585

cfv 5589 (class class class)co 6308

cof 6548 supp csupp 6933

cmap 7490

cfn 7587 finSupp cfsupp 7901

cc0 9557

caddc 9560

cn 10631

cn0 10893

cbs 15199

cplusg 15268

cmulr 15269

c0g 15416

_g cgsu 15417

cmnd 16613 ._gcmg 16750 Cntzccntz 17047 mulGrpcmgp 17801

cur 17813

crg 17858 mVar cmvr 18653 mPoly cmpl 18654

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-ofr 6551 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-oi 8043 df-card 8391 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811 df-fzo 11943 df-seq 12252 df-hash 12554 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-sca 15284 df-vsca 15285 df-tset 15287 df-0g 15418 df-gsum 15419 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-mhm 16660 df-submnd 16661 df-grp 16751 df-minusg 16752 df-mulg 16754 df-subg 16892 df-ghm 16959 df-cntz 17049 df-cmn 17510 df-abl 17511 df-mgp 17802 df-ur 17814 df-srg 17818 df-ring 17860 df-subrg 18084 df-psr 18657 df-mvr 18658 df-mpl 18659

This theorem is referenced by: mplcoe2 18770 ply1coe 18966

W3C validator