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 19468

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

is a commutative ring (as in mplcoe2 19469), 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 19364	. . . . . . . . . 10 $/\$
5	2, 4	syl 17	. . . . . . . . 9 $/\$
6	1, 5	mpbid 222	. . . . . . . 8 $/\$
7	6	simpld 475	. . . . . . 7
8	7	feqmptd 6249	. . . . . 6
9		iftrue 4092	. . . . . . . . 9
10	9	adantl 482	. . . . . . . 8 $/\$ $/\$
11		eldif 3584	. . . . . . . . . 10 $\$ $/\$
12		ifid 4125	. . . . . . . . . . 11
13		frnnn0supp 11349	. . . . . . . . . . . . . . 15 $/\$ supp
14	2, 7, 13	syl2anc 693	. . . . . . . . . . . . . 14 supp
15		eqimss 3657	. . . . . . . . . . . . . 14 supp supp
16	14, 15	syl 17	. . . . . . . . . . . . 13 supp
17		c0ex 10034	. . . . . . . . . . . . . 14
18	17	a1i 11	. . . . . . . . . . . . 13
19	7, 16, 2, 18	suppssr 7326	. . . . . . . . . . . 12 $/\$ $\$
20	19	ifeq2d 4105	. . . . . . . . . . 11 $/\$ $\$
21	12, 20	syl5reqr 2671	. . . . . . . . . 10 $/\$ $\$
22	11, 21	sylan2br 493	. . . . . . . . 9 $/\$ $/\$
23	22	anassrs 680	. . . . . . . 8 $/\$ $/\$
24	10, 23	pm2.61dan 832	. . . . . . 7 $/\$
25	24	mpteq2dva 4744	. . . . . 6
26	8, 25	eqtr4d 2659	. . . . 5
27	26	eqeq2d 2632	. . . 4
28	27	ifbid 4108	. . 3
29	28	mpteq2dv 4745	. 2
30		cnvimass 5485	. . . . 5
31		fdm 6051	. . . . . 6
32	7, 31	syl 17	. . . . 5
33	30, 32	syl5sseq 3653	. . . 4
34	6	simprd 479	. . . . 5
35		sseq1 3626	. . . . . . . 8
36		noel 3919	. . . . . . . . . . . . . . . 16
37		eleq2 2690	. . . . . . . . . . . . . . . 16
38	36, 37	mtbiri 317	. . . . . . . . . . . . . . 15
39	38	iffalsed 4097	. . . . . . . . . . . . . 14
40	39	mpteq2dv 4745	. . . . . . . . . . . . 13
41		fconstmpt 5163	. . . . . . . . . . . . 13
42	40, 41	syl6eqr 2674	. . . . . . . . . . . 12
43	42	eqeq2d 2632	. . . . . . . . . . 11
44	43	ifbid 4108	. . . . . . . . . 10
45	44	mpteq2dv 4745	. . . . . . . . 9
46		mpteq1 4737	. . . . . . . . . . . 12
47		mpt0 6021	. . . . . . . . . . . 12
48	46, 47	syl6eq 2672	. . . . . . . . . . 11
49	48	oveq2d 6666	. . . . . . . . . 10 _g _g
50		mplcoe2.g	. . . . . . . . . . . 12 mulGrp
51		eqid 2622	. . . . . . . . . . . 12
52	50, 51	ringidval 18503	. . . . . . . . . . 11
53	52	gsum0 17278	. . . . . . . . . 10 _g
54	49, 53	syl6eq 2672	. . . . . . . . 9 _g
55	45, 54	eqeq12d 2637	. . . . . . . 8 _g
56	35, 55	imbi12d 334	. . . . . . 7 _g
57	56	imbi2d 330	. . . . . 6 _g
58		sseq1 3626	. . . . . . . 8
59		eleq2 2690	. . . . . . . . . . . . . 14
60	59	ifbid 4108	. . . . . . . . . . . . 13
61	60	mpteq2dv 4745	. . . . . . . . . . . 12
62	61	eqeq2d 2632	. . . . . . . . . . 11
63	62	ifbid 4108	. . . . . . . . . 10
64	63	mpteq2dv 4745	. . . . . . . . 9
65		mpteq1 4737	. . . . . . . . . 10
66	65	oveq2d 6666	. . . . . . . . 9 _g _g
67	64, 66	eqeq12d 2637	. . . . . . . 8 _g _g
68	58, 67	imbi12d 334	. . . . . . 7 _g _g
69	68	imbi2d 330	. . . . . 6 _g _g
70		sseq1 3626	. . . . . . . 8
71		eleq2 2690	. . . . . . . . . . . . . 14
72	71	ifbid 4108	. . . . . . . . . . . . 13
73	72	mpteq2dv 4745	. . . . . . . . . . . 12
74	73	eqeq2d 2632	. . . . . . . . . . 11
75	74	ifbid 4108	. . . . . . . . . 10
76	75	mpteq2dv 4745	. . . . . . . . 9
77		mpteq1 4737	. . . . . . . . . 10
78	77	oveq2d 6666	. . . . . . . . 9 _g _g
79	76, 78	eqeq12d 2637	. . . . . . . 8 _g _g
80	70, 79	imbi12d 334	. . . . . . 7 _g _g
81	80	imbi2d 330	. . . . . 6 _g _g
82		sseq1 3626	. . . . . . . 8
83		eleq2 2690	. . . . . . . . . . . . . 14
84	83	ifbid 4108	. . . . . . . . . . . . 13
85	84	mpteq2dv 4745	. . . . . . . . . . . 12
86	85	eqeq2d 2632	. . . . . . . . . . 11
87	86	ifbid 4108	. . . . . . . . . 10
88	87	mpteq2dv 4745	. . . . . . . . 9
89		mpteq1 4737	. . . . . . . . . 10
90	89	oveq2d 6666	. . . . . . . . 9 _g _g
91	88, 90	eqeq12d 2637	. . . . . . . 8 _g _g
92	82, 91	imbi12d 334	. . . . . . 7 _g _g
93	92	imbi2d 330	. . . . . 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 19444	. . . . . . . 8
99	98	eqcomd 2628	. . . . . . 7
100	99	a1d 25	. . . . . 6
101		ssun1 3776	. . . . . . . . . . 11
102		sstr2 3610	. . . . . . . . . . 11
103	101, 102	ax-mp 5	. . . . . . . . . 10
104	103	imim1i 63	. . . . . . . . 9 _g _g
105		oveq1 6657	. . . . . . . . . . . 12 _g _g
106		eqid 2622	. . . . . . . . . . . . . . 15
107	2	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
108	97	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
109	7	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
110	109	ffvelrnda 6359	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
111		0nn0 11307	. . . . . . . . . . . . . . . . . 18
112		ifcl 4130	. . . . . . . . . . . . . . . . . 18 $/\$
113	110, 111, 112	sylancl 694	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
114		eqid 2622	. . . . . . . . . . . . . . . . 17
115	113, 114	fmptd 6385	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
116		frnnn0supp 11349	. . . . . . . . . . . . . . . . . 18 $/\$ supp
117	107, 115, 116	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
118		simprll 802	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
119		eldifn 3733	. . . . . . . . . . . . . . . . . . . . 21 $\$
120	119	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
121	120	iffalsed 4097	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$
122	121, 107	suppss2 7329	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ supp
123		ssfi 8180	. . . . . . . . . . . . . . . . . 18 $/\$ supp supp
124	118, 122, 123	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
125	117, 124	eqeltrrd 2702	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	3	psrbag 19364	. . . . . . . . . . . . . . . . 17 $/\$
127	107, 126	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	115, 125, 127	mpbir2and 957	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129		eqid 2622	. . . . . . . . . . . . . . 15
130		ssun2 3777	. . . . . . . . . . . . . . . . . . 19
131		simprr 796	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
132	130, 131	syl5ss 3614	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
133		vex 3203	. . . . . . . . . . . . . . . . . . 19
134	133	snss 4316	. . . . . . . . . . . . . . . . . 18
135	132, 134	sylibr 224	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
136	109, 135	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	3	snifpsrbag 19366	. . . . . . . . . . . . . . . 16 $/\$
138	107, 136, 137	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	94, 106, 95, 96, 3, 107, 108, 128, 129, 138	mplmonmul 19464	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140		mplcoe2.m	. . . . . . . . . . . . . . . 16 ._g
141		mplcoe2.v	. . . . . . . . . . . . . . . 16 mVar
142	94, 3, 95, 96, 107, 50, 140, 141, 108, 135, 136	mplcoe3 19466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
143	142	oveq2d 6666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	136	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
145		ifcl 4130	. . . . . . . . . . . . . . . . . . . 20 $/\$
146	144, 111, 145	sylancl 694	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
147		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
148		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
149	107, 113, 146, 147, 148	offval2 6914	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
150	110	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
151	150	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
152	151	addid2d 10237	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
153		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . 25
154	153	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
155		simprlr 803	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156	155	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
157	154, 156	eqneltrd 2720	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
158	157	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
159	154	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
160	154	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
161	159, 160	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	158, 161	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
163		simpr 477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
164	130, 163	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
165	164	iftrued 4094	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
166	152, 162, 165	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
167	113	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
168	167	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	addid1d 10236	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
170		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
171		velsn 4193	. . . . . . . . . . . . . . . . . . . . . . . 24
172	170, 171	sylnib 318	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
174	173	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
175		biorf 420	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
176		elun 3753	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
177		orcom 402	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$
178	176, 177	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
179	175, 178	syl6rbbr 279	. . . . . . . . . . . . . . . . . . . . . . 23
180	179	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
181	180	ifbid 4108	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
182	169, 174, 181	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
183	166, 182	pm2.61dan 832	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
184	183	mpteq2dva 4744	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185	149, 184	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
186	185	eqeq2d 2632	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
187	186	ifbid 4108	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188	187	mpteq2dv 4745	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
189	139, 143, 188	3eqtr3rd 2665	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
190	50, 106	mgpbas 18495	. . . . . . . . . . . . . 14
191	50, 129	mgpplusg 18493	. . . . . . . . . . . . . 14
192		eqid 2622	. . . . . . . . . . . . . 14 Cntz Cntz
193		eqid 2622	. . . . . . . . . . . . . 14
194	94	mplring 19452	. . . . . . . . . . . . . . . . 17 $/\$
195	2, 97, 194	syl2anc 693	. . . . . . . . . . . . . . . 16
196	50	ringmgp 18553	. . . . . . . . . . . . . . . 16
197	195, 196	syl 17	. . . . . . . . . . . . . . 15
198	197	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
199	1	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
200		mplcoe5.c	. . . . . . . . . . . . . . . . 17
201		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
202	201	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
203	201	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19
204	202, 203	eqeq12d 2637	. . . . . . . . . . . . . . . . . 18
205		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
206	205	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19
207	205	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
208	206, 207	eqeq12d 2637	. . . . . . . . . . . . . . . . . 18
209	204, 208	cbvral2v 3179	. . . . . . . . . . . . . . . . 17
210	200, 209	sylib 208	. . . . . . . . . . . . . . . 16
211	210	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
212	94, 3, 95, 96, 107, 50, 140, 141, 108, 199, 211, 131	mplcoe5lem 19467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Cntz
213	101, 131	syl5ss 3614	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	213	sselda 3603	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
215	197	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
216	7	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 $/\$
217	2	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
218	97	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
219		simpr 477	. . . . . . . . . . . . . . . . . 18 $/\$
220	94, 141, 106, 217, 218, 219	mvrcl 19449	. . . . . . . . . . . . . . . . 17 $/\$
221	190, 140	mulgnn0cl 17558	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
222	215, 216, 220, 221	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$
223	222	adantlr 751	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
224	214, 223	syldan 487	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
225	94, 141, 106, 107, 108, 135	mvrcl 19449	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	190, 140	mulgnn0cl 17558	. . . . . . . . . . . . . . 15 $/\$ $/\$
227	198, 136, 225, 226	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
228		fveq2 6191	. . . . . . . . . . . . . . . 16
229		fveq2 6191	. . . . . . . . . . . . . . . 16
230	228, 229	oveq12d 6668	. . . . . . . . . . . . . . 15
231	230	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
232	190, 191, 192, 193, 198, 118, 212, 224, 135, 155, 227, 231	gsumzunsnd 18355	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ _g _g
233	189, 232	eqeq12d 2637	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ _g _g
234	105, 233	syl5ibr 236	. . . . . . . . . . 11 $/\$ $/\$ $/\$ _g _g
235	234	expr 643	. . . . . . . . . 10 $/\$ $/\$ _g _g
236	235	a2d 29	. . . . . . . . 9 $/\$ $/\$ _g _g
237	104, 236	syl5 34	. . . . . . . 8 $/\$ $/\$ _g _g
238	237	expcom 451	. . . . . . 7 $/\$ _g _g
239	238	a2d 29	. . . . . 6 $/\$ _g _g
240	57, 69, 81, 93, 100, 239	findcard2s 8201	. . . . 5 _g
241	34, 240	mpcom 38	. . . 4 _g
242	33, 241	mpd 15	. . 3 _g
243	33	resmptd 5452	. . . 4
244	243	oveq2d 6666	. . 3 _g _g
245		eqid 2622	. . . . 5
246	222, 245	fmptd 6385	. . . 4
247		ssid 3624	. . . . . 6
248	247	a1i 11	. . . . 5
249	94, 3, 95, 96, 2, 50, 140, 141, 97, 1, 200, 248	mplcoe5lem 19467	. . . 4 Cntz
250	7, 16, 2, 18	suppssr 7326	. . . . . . 7 $/\$ $\$
251	250	oveq1d 6665	. . . . . 6 $/\$ $\$
252		eldifi 3732	. . . . . . . 8 $\$
253	252, 220	sylan2 491	. . . . . . 7 $/\$ $\$
254	190, 52, 140	mulg0 17546	. . . . . . 7
255	253, 254	syl 17	. . . . . 6 $/\$ $\$
256	251, 255	eqtrd 2656	. . . . 5 $/\$ $\$
257	256, 2	suppss2 7329	. . . 4 supp
258		mptexg 6484	. . . . . 6
259	2, 258	syl 17	. . . . 5
260		funmpt 5926	. . . . . 6
261	260	a1i 11	. . . . 5
262		fvexd 6203	. . . . 5
263		suppssfifsupp 8290	. . . . 5 $/\$ $/\$ $/\$ $/\$ supp finSupp
264	259, 261, 262, 34, 257, 263	syl32anc 1334	. . . 4 finSupp
265	190, 52, 192, 197, 2, 246, 249, 257, 264	gsumzres 18310	. . 3 _g _g
266	242, 244, 265	3eqtr2d 2662	. 2 _g
267	29, 266	eqtrd 2656	1 _g

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

wral 2912

crab 2916

cvv 3200 $\$ cdif 3571

cun 3572

wss 3574

c0 3915

cif 4086

csn 4177 class class class wbr 4653

cmpt 4729

cxp 5112

ccnv 5113

cdm 5114

cres 5116

cima 5117

wfun 5882

wf 5884

cfv 5888 (class class class)co 6650

cof 6895 supp csupp 7295

cmap 7857

cfn 7955 finSupp cfsupp 8275

cc0 9936

caddc 9939

cn 11020

cn0 11292

cbs 15857

cplusg 15941

cmulr 15942

c0g 16100

_g cgsu 16101

cmnd 17294 ._gcmg 17540 Cntzccntz 17748 mulGrpcmgp 18489

cur 18501

crg 18547 mVar cmvr 19352 mPoly cmpl 19353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-ofr 6898 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-seq 12802 df-hash 13118 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-sca 15957 df-vsca 15958 df-tset 15960 df-0g 16102 df-gsum 16103 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-mhm 17335 df-submnd 17336 df-grp 17425 df-minusg 17426 df-mulg 17541 df-subg 17591 df-ghm 17658 df-cntz 17750 df-cmn 18195 df-abl 18196 df-mgp 18490 df-ur 18502 df-srg 18506 df-ring 18549 df-subrg 18778 df-psr 19356 df-mvr 19357 df-mpl 19358

This theorem is referenced by: mplcoe2 19469 ply1coe 19666

W3C validator