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 18692

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

is a commutative ring (as in mplcoe2 18693), 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 18588	. . . . . . . . . 10 $/\$
5	2, 4	syl 17	. . . . . . . . 9 $/\$
6	1, 5	mpbid 214	. . . . . . . 8 $/\$
7	6	simpld 461	. . . . . . 7
8	7	feqmptd 5918	. . . . . 6
9		iftrue 3887	. . . . . . . . 9
10	9	adantl 468	. . . . . . . 8 $/\$ $/\$
11		eldif 3414	. . . . . . . . . 10 $\$ $/\$
12		ifid 3918	. . . . . . . . . . 11
13		frnnn0supp 10923	. . . . . . . . . . . . . . 15 $/\$ supp
14	2, 7, 13	syl2anc 667	. . . . . . . . . . . . . 14 supp
15		eqimss 3484	. . . . . . . . . . . . . 14 supp supp
16	14, 15	syl 17	. . . . . . . . . . . . 13 supp
17		c0ex 9637	. . . . . . . . . . . . . 14
18	17	a1i 11	. . . . . . . . . . . . 13
19	7, 16, 2, 18	suppssr 6946	. . . . . . . . . . . 12 $/\$ $\$
20	19	ifeq2d 3900	. . . . . . . . . . 11 $/\$ $\$
21	12, 20	syl5reqr 2500	. . . . . . . . . 10 $/\$ $\$
22	11, 21	sylan2br 479	. . . . . . . . 9 $/\$ $/\$
23	22	anassrs 654	. . . . . . . 8 $/\$ $/\$
24	10, 23	pm2.61dan 800	. . . . . . 7 $/\$
25	24	mpteq2dva 4489	. . . . . 6
26	8, 25	eqtr4d 2488	. . . . 5
27	26	eqeq2d 2461	. . . 4
28	27	ifbid 3903	. . 3
29	28	mpteq2dv 4490	. 2
30		cnvimass 5188	. . . . 5
31		fdm 5733	. . . . . 6
32	7, 31	syl 17	. . . . 5
33	30, 32	syl5sseq 3480	. . . 4
34	6	simprd 465	. . . . 5
35		sseq1 3453	. . . . . . . 8
36		noel 3735	. . . . . . . . . . . . . . . 16
37		eleq2 2518	. . . . . . . . . . . . . . . 16
38	36, 37	mtbiri 305	. . . . . . . . . . . . . . 15
39	38	iffalsed 3892	. . . . . . . . . . . . . 14
40	39	mpteq2dv 4490	. . . . . . . . . . . . 13
41		fconstmpt 4878	. . . . . . . . . . . . 13
42	40, 41	syl6eqr 2503	. . . . . . . . . . . 12
43	42	eqeq2d 2461	. . . . . . . . . . 11
44	43	ifbid 3903	. . . . . . . . . 10
45	44	mpteq2dv 4490	. . . . . . . . 9
46		mpteq1 4483	. . . . . . . . . . . 12
47		mpt0 5705	. . . . . . . . . . . 12
48	46, 47	syl6eq 2501	. . . . . . . . . . 11
49	48	oveq2d 6306	. . . . . . . . . 10 _g _g
50		mplcoe2.g	. . . . . . . . . . . 12 mulGrp
51		eqid 2451	. . . . . . . . . . . 12
52	50, 51	ringidval 17737	. . . . . . . . . . 11
53	52	gsum0 16521	. . . . . . . . . 10 _g
54	49, 53	syl6eq 2501	. . . . . . . . 9 _g
55	45, 54	eqeq12d 2466	. . . . . . . 8 _g
56	35, 55	imbi12d 322	. . . . . . 7 _g
57	56	imbi2d 318	. . . . . 6 _g
58		sseq1 3453	. . . . . . . 8
59		eleq2 2518	. . . . . . . . . . . . . 14
60	59	ifbid 3903	. . . . . . . . . . . . 13
61	60	mpteq2dv 4490	. . . . . . . . . . . 12
62	61	eqeq2d 2461	. . . . . . . . . . 11
63	62	ifbid 3903	. . . . . . . . . 10
64	63	mpteq2dv 4490	. . . . . . . . 9
65		mpteq1 4483	. . . . . . . . . 10
66	65	oveq2d 6306	. . . . . . . . 9 _g _g
67	64, 66	eqeq12d 2466	. . . . . . . 8 _g _g
68	58, 67	imbi12d 322	. . . . . . 7 _g _g
69	68	imbi2d 318	. . . . . 6 _g _g
70		sseq1 3453	. . . . . . . 8
71		eleq2 2518	. . . . . . . . . . . . . 14
72	71	ifbid 3903	. . . . . . . . . . . . 13
73	72	mpteq2dv 4490	. . . . . . . . . . . 12
74	73	eqeq2d 2461	. . . . . . . . . . 11
75	74	ifbid 3903	. . . . . . . . . 10
76	75	mpteq2dv 4490	. . . . . . . . 9
77		mpteq1 4483	. . . . . . . . . 10
78	77	oveq2d 6306	. . . . . . . . 9 _g _g
79	76, 78	eqeq12d 2466	. . . . . . . 8 _g _g
80	70, 79	imbi12d 322	. . . . . . 7 _g _g
81	80	imbi2d 318	. . . . . 6 _g _g
82		sseq1 3453	. . . . . . . 8
83		eleq2 2518	. . . . . . . . . . . . . 14
84	83	ifbid 3903	. . . . . . . . . . . . 13
85	84	mpteq2dv 4490	. . . . . . . . . . . 12
86	85	eqeq2d 2461	. . . . . . . . . . 11
87	86	ifbid 3903	. . . . . . . . . 10
88	87	mpteq2dv 4490	. . . . . . . . 9
89		mpteq1 4483	. . . . . . . . . 10
90	89	oveq2d 6306	. . . . . . . . 9 _g _g
91	88, 90	eqeq12d 2466	. . . . . . . 8 _g _g
92	82, 91	imbi12d 322	. . . . . . 7 _g _g
93	92	imbi2d 318	. . . . . 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 18668	. . . . . . . 8
99	98	eqcomd 2457	. . . . . . 7
100	99	a1d 26	. . . . . 6
101		ssun1 3597	. . . . . . . . . . 11
102		sstr2 3439	. . . . . . . . . . 11
103	101, 102	ax-mp 5	. . . . . . . . . 10
104	103	imim1i 60	. . . . . . . . 9 _g _g
105		oveq1 6297	. . . . . . . . . . . 12 _g _g
106		eqid 2451	. . . . . . . . . . . . . . 15
107	2	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
108	97	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
109	7	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
110	109	ffvelrnda 6022	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
111		0nn0 10884	. . . . . . . . . . . . . . . . . 18
112		ifcl 3923	. . . . . . . . . . . . . . . . . 18 $/\$
113	110, 111, 112	sylancl 668	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
114		eqid 2451	. . . . . . . . . . . . . . . . 17
115	113, 114	fmptd 6046	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
116		frnnn0supp 10923	. . . . . . . . . . . . . . . . . 18 $/\$ supp
117	107, 115, 116	syl2anc 667	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
118		simprll 772	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
119		eldifn 3556	. . . . . . . . . . . . . . . . . . . . 21 $\$
120	119	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
121	120	iffalsed 3892	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$
122	121, 107	suppss2 6949	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ supp
123		ssfi 7792	. . . . . . . . . . . . . . . . . 18 $/\$ supp supp
124	118, 122, 123	syl2anc 667	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
125	117, 124	eqeltrrd 2530	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	3	psrbag 18588	. . . . . . . . . . . . . . . . 17 $/\$
127	107, 126	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	115, 125, 127	mpbir2and 933	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129		eqid 2451	. . . . . . . . . . . . . . 15
130		ssun2 3598	. . . . . . . . . . . . . . . . . . 19
131		simprr 766	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
132	130, 131	syl5ss 3443	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
133		vex 3048	. . . . . . . . . . . . . . . . . . 19
134	133	snss 4096	. . . . . . . . . . . . . . . . . 18
135	132, 134	sylibr 216	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
136	109, 135	ffvelrnd 6023	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	3	snifpsrbag 18590	. . . . . . . . . . . . . . . 16 $/\$
138	107, 136, 137	syl2anc 667	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	94, 106, 95, 96, 3, 107, 108, 128, 129, 138	mplmonmul 18688	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140		mplcoe2.m	. . . . . . . . . . . . . . . 16 ._g
141		mplcoe2.v	. . . . . . . . . . . . . . . 16 mVar
142	94, 3, 95, 96, 107, 50, 140, 141, 108, 135, 136	mplcoe3 18690	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
143	142	oveq2d 6306	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	136	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
145		ifcl 3923	. . . . . . . . . . . . . . . . . . . 20 $/\$
146	144, 111, 145	sylancl 668	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
147		eqidd 2452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
148		eqidd 2452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
149	107, 113, 146, 147, 148	offval2 6548	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
150	110	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
151	150	nn0cnd 10927	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
152	151	addid2d 9834	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
153		elsni 3993	. . . . . . . . . . . . . . . . . . . . . . . . 25
154	153	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
155		simprlr 773	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156	155	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
157	154, 156	eqneltrd 2548	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
158	157	iffalsed 3892	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
159	154	iftrued 3889	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
160	154	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
161	159, 160	eqtr4d 2488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	158, 161	oveq12d 6308	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
163		simpr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
164	130, 163	sseldi 3430	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
165	164	iftrued 3889	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
166	152, 162, 165	3eqtr4d 2495	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
167	113	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
168	167	nn0cnd 10927	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	addid1d 9833	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
170		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
171		elsn 3982	. . . . . . . . . . . . . . . . . . . . . . . 24
172	170, 171	sylnib 306	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	iffalsed 3892	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
174	173	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
175		biorf 407	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
176		elun 3574	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
177		orcom 389	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$
178	176, 177	bitri 253	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
179	175, 178	syl6rbbr 268	. . . . . . . . . . . . . . . . . . . . . . 23
180	179	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
181	180	ifbid 3903	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
182	169, 174, 181	3eqtr4d 2495	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
183	166, 182	pm2.61dan 800	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
184	183	mpteq2dva 4489	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185	149, 184	eqtrd 2485	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
186	185	eqeq2d 2461	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
187	186	ifbid 3903	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188	187	mpteq2dv 4490	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
189	139, 143, 188	3eqtr3rd 2494	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
190	50, 106	mgpbas 17729	. . . . . . . . . . . . . 14
191	50, 129	mgpplusg 17727	. . . . . . . . . . . . . 14
192		eqid 2451	. . . . . . . . . . . . . 14 Cntz Cntz
193		eqid 2451	. . . . . . . . . . . . . 14
194	94	mplring 18676	. . . . . . . . . . . . . . . . 17 $/\$
195	2, 97, 194	syl2anc 667	. . . . . . . . . . . . . . . 16
196	50	ringmgp 17786	. . . . . . . . . . . . . . . 16
197	195, 196	syl 17	. . . . . . . . . . . . . . 15
198	197	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
199	1	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
200		mplcoe5.c	. . . . . . . . . . . . . . . . 17
201		fveq2 5865	. . . . . . . . . . . . . . . . . . . 20
202	201	oveq2d 6306	. . . . . . . . . . . . . . . . . . 19
203	201	oveq1d 6305	. . . . . . . . . . . . . . . . . . 19
204	202, 203	eqeq12d 2466	. . . . . . . . . . . . . . . . . 18
205		fveq2 5865	. . . . . . . . . . . . . . . . . . . 20
206	205	oveq1d 6305	. . . . . . . . . . . . . . . . . . 19
207	205	oveq2d 6306	. . . . . . . . . . . . . . . . . . 19
208	206, 207	eqeq12d 2466	. . . . . . . . . . . . . . . . . 18
209	204, 208	cbvral2v 3027	. . . . . . . . . . . . . . . . 17
210	200, 209	sylib 200	. . . . . . . . . . . . . . . 16
211	210	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
212	94, 3, 95, 96, 107, 50, 140, 141, 108, 199, 211, 131	mplcoe5lem 18691	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Cntz
213	101, 131	syl5ss 3443	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	213	sselda 3432	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
215	197	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
216	7	ffvelrnda 6022	. . . . . . . . . . . . . . . . 17 $/\$
217	2	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
218	97	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
219		simpr 463	. . . . . . . . . . . . . . . . . 18 $/\$
220	94, 141, 106, 217, 218, 219	mvrcl 18673	. . . . . . . . . . . . . . . . 17 $/\$
221	190, 140	mulgnn0cl 16774	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
222	215, 216, 220, 221	syl3anc 1268	. . . . . . . . . . . . . . . 16 $/\$
223	222	adantlr 721	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
224	214, 223	syldan 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
225	94, 141, 106, 107, 108, 135	mvrcl 18673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	190, 140	mulgnn0cl 16774	. . . . . . . . . . . . . . 15 $/\$ $/\$
227	198, 136, 225, 226	syl3anc 1268	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
228		fveq2 5865	. . . . . . . . . . . . . . . 16
229		fveq2 5865	. . . . . . . . . . . . . . . 16
230	228, 229	oveq12d 6308	. . . . . . . . . . . . . . 15
231	230	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
232	190, 191, 192, 193, 198, 118, 212, 224, 135, 155, 227, 231	gsumzunsnd 17588	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ _g _g
233	189, 232	eqeq12d 2466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ _g _g
234	105, 233	syl5ibr 225	. . . . . . . . . . 11 $/\$ $/\$ $/\$ _g _g
235	234	expr 620	. . . . . . . . . 10 $/\$ $/\$ _g _g
236	235	a2d 29	. . . . . . . . 9 $/\$ $/\$ _g _g
237	104, 236	syl5 33	. . . . . . . 8 $/\$ $/\$ _g _g
238	237	expcom 437	. . . . . . 7 $/\$ _g _g
239	238	a2d 29	. . . . . 6 $/\$ _g _g
240	57, 69, 81, 93, 100, 239	findcard2s 7812	. . . . 5 _g
241	34, 240	mpcom 37	. . . 4 _g
242	33, 241	mpd 15	. . 3 _g
243	33	resmptd 5156	. . . 4
244	243	oveq2d 6306	. . 3 _g _g
245		eqid 2451	. . . . 5
246	222, 245	fmptd 6046	. . . 4
247		ssid 3451	. . . . . 6
248	247	a1i 11	. . . . 5
249	94, 3, 95, 96, 2, 50, 140, 141, 97, 1, 200, 248	mplcoe5lem 18691	. . . 4 Cntz
250	7, 16, 2, 18	suppssr 6946	. . . . . . 7 $/\$ $\$
251	250	oveq1d 6305	. . . . . 6 $/\$ $\$
252		eldifi 3555	. . . . . . . 8 $\$
253	252, 220	sylan2 477	. . . . . . 7 $/\$ $\$
254	190, 52, 140	mulg0 16763	. . . . . . 7
255	253, 254	syl 17	. . . . . 6 $/\$ $\$
256	251, 255	eqtrd 2485	. . . . 5 $/\$ $\$
257	256, 2	suppss2 6949	. . . 4 supp
258		mptexg 6135	. . . . . 6
259	2, 258	syl 17	. . . . 5
260		funmpt 5618	. . . . . 6
261	260	a1i 11	. . . . 5
262		fvex 5875	. . . . . 6
263	262	a1i 11	. . . . 5
264		suppssfifsupp 7898	. . . . 5 $/\$ $/\$ $/\$ $/\$ supp finSupp
265	259, 261, 263, 34, 257, 264	syl32anc 1276	. . . 4 finSupp
266	190, 52, 192, 197, 2, 246, 249, 257, 265	gsumzres 17543	. . 3 _g _g
267	242, 244, 266	3eqtr2d 2491	. 2 _g
268	29, 267	eqtrd 2485	1 _g

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371

wceq 1444

wcel 1887

wral 2737

crab 2741

cvv 3045 $\$ cdif 3401

cun 3402

wss 3404

c0 3731

cif 3881

csn 3968 class class class wbr 4402

cmpt 4461

cxp 4832

ccnv 4833

cdm 4834

cres 4836

cima 4837

wfun 5576

wf 5578

cfv 5582 (class class class)co 6290

cof 6529 supp csupp 6914

cmap 7472

cfn 7569 finSupp cfsupp 7883

cc0 9539

caddc 9542

cn 10609

cn0 10869

cbs 15121

cplusg 15190

cmulr 15191

c0g 15338

_g cgsu 15339

cmnd 16535 ._gcmg 16672 Cntzccntz 16969 mulGrpcmgp 17723

cur 17735

crg 17780 mVar cmvr 18576 mPoly cmpl 18577

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-iin 4281 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-ofr 6532 df-om 6693 df-1st 6793 df-2nd 6794 df-supp 6915 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fsupp 7884 df-oi 8025 df-card 8373 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-n0 10870 df-z 10938 df-uz 11160 df-fz 11785 df-fzo 11916 df-seq 12214 df-hash 12516 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-sca 15206 df-vsca 15207 df-tset 15209 df-0g 15340 df-gsum 15341 df-mre 15492 df-mrc 15493 df-acs 15495 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-mhm 16582 df-submnd 16583 df-grp 16673 df-minusg 16674 df-mulg 16676 df-subg 16814 df-ghm 16881 df-cntz 16971 df-cmn 17432 df-abl 17433 df-mgp 17724 df-ur 17736 df-srg 17740 df-ring 17782 df-subrg 18006 df-psr 18580 df-mvr 18581 df-mpl 18582

This theorem is referenced by: mplcoe2 18693 ply1coe 18889

W3C validator