mplcoe5 - Metamath Proof Explorer

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

Theorem mplcoe5 18685

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

is a commutative ring (as in mplcoe2 18686), 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 18581	. . . . . . . . . 10 $/\$
5	2, 4	syl 17	. . . . . . . . 9 $/\$
6	1, 5	mpbid 214	. . . . . . . 8 $/\$
7	6	simpld 461	. . . . . . 7
8	7	feqmptd 5932	. . . . . 6
9		iftrue 3916	. . . . . . . . 9
10	9	adantl 468	. . . . . . . 8 $/\$ $/\$
11		eldif 3447	. . . . . . . . . 10 $\$ $/\$
12		ifid 3947	. . . . . . . . . . 11
13		frnnn0supp 10925	. . . . . . . . . . . . . . 15 $/\$ supp
14	2, 7, 13	syl2anc 666	. . . . . . . . . . . . . 14 supp
15		eqimss 3517	. . . . . . . . . . . . . 14 supp supp
16	14, 15	syl 17	. . . . . . . . . . . . 13 supp
17		c0ex 9639	. . . . . . . . . . . . . 14
18	17	a1i 11	. . . . . . . . . . . . 13
19	7, 16, 2, 18	suppssr 6955	. . . . . . . . . . . 12 $/\$ $\$
20	19	ifeq2d 3929	. . . . . . . . . . 11 $/\$ $\$
21	12, 20	syl5reqr 2479	. . . . . . . . . 10 $/\$ $\$
22	11, 21	sylan2br 479	. . . . . . . . 9 $/\$ $/\$
23	22	anassrs 653	. . . . . . . 8 $/\$ $/\$
24	10, 23	pm2.61dan 799	. . . . . . 7 $/\$
25	24	mpteq2dva 4508	. . . . . 6
26	8, 25	eqtr4d 2467	. . . . 5
27	26	eqeq2d 2437	. . . 4
28	27	ifbid 3932	. . 3
29	28	mpteq2dv 4509	. 2
30		cnvimass 5205	. . . . 5
31		fdm 5748	. . . . . 6
32	7, 31	syl 17	. . . . 5
33	30, 32	syl5sseq 3513	. . . 4
34	6	simprd 465	. . . . 5
35		sseq1 3486	. . . . . . . 8
36		noel 3766	. . . . . . . . . . . . . . . 16
37		eleq2 2496	. . . . . . . . . . . . . . . 16
38	36, 37	mtbiri 305	. . . . . . . . . . . . . . 15
39	38	iffalsed 3921	. . . . . . . . . . . . . 14
40	39	mpteq2dv 4509	. . . . . . . . . . . . 13
41		fconstmpt 4895	. . . . . . . . . . . . 13
42	40, 41	syl6eqr 2482	. . . . . . . . . . . 12
43	42	eqeq2d 2437	. . . . . . . . . . 11
44	43	ifbid 3932	. . . . . . . . . 10
45	44	mpteq2dv 4509	. . . . . . . . 9
46		mpteq1 4502	. . . . . . . . . . . 12
47		mpt0 5721	. . . . . . . . . . . 12
48	46, 47	syl6eq 2480	. . . . . . . . . . 11
49	48	oveq2d 6319	. . . . . . . . . 10 _g _g
50		mplcoe2.g	. . . . . . . . . . . 12 mulGrp
51		eqid 2423	. . . . . . . . . . . 12
52	50, 51	ringidval 17730	. . . . . . . . . . 11
53	52	gsum0 16514	. . . . . . . . . 10 _g
54	49, 53	syl6eq 2480	. . . . . . . . 9 _g
55	45, 54	eqeq12d 2445	. . . . . . . 8 _g
56	35, 55	imbi12d 322	. . . . . . 7 _g
57	56	imbi2d 318	. . . . . 6 _g
58		sseq1 3486	. . . . . . . 8
59		eleq2 2496	. . . . . . . . . . . . . 14
60	59	ifbid 3932	. . . . . . . . . . . . 13
61	60	mpteq2dv 4509	. . . . . . . . . . . 12
62	61	eqeq2d 2437	. . . . . . . . . . 11
63	62	ifbid 3932	. . . . . . . . . 10
64	63	mpteq2dv 4509	. . . . . . . . 9
65		mpteq1 4502	. . . . . . . . . 10
66	65	oveq2d 6319	. . . . . . . . 9 _g _g
67	64, 66	eqeq12d 2445	. . . . . . . 8 _g _g
68	58, 67	imbi12d 322	. . . . . . 7 _g _g
69	68	imbi2d 318	. . . . . 6 _g _g
70		sseq1 3486	. . . . . . . 8
71		eleq2 2496	. . . . . . . . . . . . . 14
72	71	ifbid 3932	. . . . . . . . . . . . 13
73	72	mpteq2dv 4509	. . . . . . . . . . . 12
74	73	eqeq2d 2437	. . . . . . . . . . 11
75	74	ifbid 3932	. . . . . . . . . 10
76	75	mpteq2dv 4509	. . . . . . . . 9
77		mpteq1 4502	. . . . . . . . . 10
78	77	oveq2d 6319	. . . . . . . . 9 _g _g
79	76, 78	eqeq12d 2445	. . . . . . . 8 _g _g
80	70, 79	imbi12d 322	. . . . . . 7 _g _g
81	80	imbi2d 318	. . . . . 6 _g _g
82		sseq1 3486	. . . . . . . 8
83		eleq2 2496	. . . . . . . . . . . . . 14
84	83	ifbid 3932	. . . . . . . . . . . . 13
85	84	mpteq2dv 4509	. . . . . . . . . . . 12
86	85	eqeq2d 2437	. . . . . . . . . . 11
87	86	ifbid 3932	. . . . . . . . . 10
88	87	mpteq2dv 4509	. . . . . . . . 9
89		mpteq1 4502	. . . . . . . . . 10
90	89	oveq2d 6319	. . . . . . . . 9 _g _g
91	88, 90	eqeq12d 2445	. . . . . . . 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 18661	. . . . . . . 8
99	98	eqcomd 2431	. . . . . . 7
100	99	a1d 27	. . . . . 6
101		ssun1 3630	. . . . . . . . . . 11
102		sstr2 3472	. . . . . . . . . . 11
103	101, 102	ax-mp 5	. . . . . . . . . 10
104	103	imim1i 61	. . . . . . . . 9 _g _g
105		oveq1 6310	. . . . . . . . . . . 12 _g _g
106		eqid 2423	. . . . . . . . . . . . . . 15
107	2	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
108	97	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
109	7	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
110	109	ffvelrnda 6035	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
111		0nn0 10886	. . . . . . . . . . . . . . . . . 18
112		ifcl 3952	. . . . . . . . . . . . . . . . . 18 $/\$
113	110, 111, 112	sylancl 667	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
114		eqid 2423	. . . . . . . . . . . . . . . . 17
115	113, 114	fmptd 6059	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
116		frnnn0supp 10925	. . . . . . . . . . . . . . . . . 18 $/\$ supp
117	107, 115, 116	syl2anc 666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
118		simprll 771	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
119		eldifn 3589	. . . . . . . . . . . . . . . . . . . . 21 $\$
120	119	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
121	120	iffalsed 3921	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$
122	121, 107	suppss2 6958	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ supp
123		ssfi 7796	. . . . . . . . . . . . . . . . . 18 $/\$ supp supp
124	118, 122, 123	syl2anc 666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
125	117, 124	eqeltrrd 2512	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	3	psrbag 18581	. . . . . . . . . . . . . . . . 17 $/\$
127	107, 126	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	115, 125, 127	mpbir2and 931	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129		eqid 2423	. . . . . . . . . . . . . . 15
130		ssun2 3631	. . . . . . . . . . . . . . . . . . 19
131		simprr 765	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
132	130, 131	syl5ss 3476	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
133		vex 3085	. . . . . . . . . . . . . . . . . . 19
134	133	snss 4122	. . . . . . . . . . . . . . . . . 18
135	132, 134	sylibr 216	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
136	109, 135	ffvelrnd 6036	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	3	snifpsrbag 18583	. . . . . . . . . . . . . . . 16 $/\$
138	107, 136, 137	syl2anc 666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	94, 106, 95, 96, 3, 107, 108, 128, 129, 138	mplmonmul 18681	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140		mplcoe2.m	. . . . . . . . . . . . . . . 16 ._g
141		mplcoe2.v	. . . . . . . . . . . . . . . 16 mVar
142	94, 3, 95, 96, 107, 50, 140, 141, 108, 135, 136	mplcoe3 18683	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
143	142	oveq2d 6319	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	136	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
145		ifcl 3952	. . . . . . . . . . . . . . . . . . . 20 $/\$
146	144, 111, 145	sylancl 667	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
147		eqidd 2424	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
148		eqidd 2424	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
149	107, 113, 146, 147, 148	offval2 6560	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
150	110	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
151	150	nn0cnd 10929	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
152	151	addid2d 9836	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
153		elsni 4022	. . . . . . . . . . . . . . . . . . . . . . . . 25
154	153	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
155		simprlr 772	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156	155	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
157	154, 156	eqneltrd 2532	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
158	157	iffalsed 3921	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
159	154	iftrued 3918	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
160	154	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
161	159, 160	eqtr4d 2467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	158, 161	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
163		simpr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
164	130, 163	sseldi 3463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
165	164	iftrued 3918	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
166	152, 162, 165	3eqtr4d 2474	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
167	113	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
168	167	nn0cnd 10929	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	addid1d 9835	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
170		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
171		elsn 4011	. . . . . . . . . . . . . . . . . . . . . . . 24
172	170, 171	sylnib 306	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	iffalsed 3921	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
174	173	oveq2d 6319	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
175		biorf 407	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
176		elun 3607	. . . . . . . . . . . . . . . . . . . . . . . . 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 3932	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
182	169, 174, 181	3eqtr4d 2474	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
183	166, 182	pm2.61dan 799	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
184	183	mpteq2dva 4508	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185	149, 184	eqtrd 2464	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
186	185	eqeq2d 2437	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
187	186	ifbid 3932	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188	187	mpteq2dv 4509	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
189	139, 143, 188	3eqtr3rd 2473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
190	50, 106	mgpbas 17722	. . . . . . . . . . . . . 14
191	50, 129	mgpplusg 17720	. . . . . . . . . . . . . 14
192		eqid 2423	. . . . . . . . . . . . . 14 Cntz Cntz
193		eqid 2423	. . . . . . . . . . . . . 14
194	94	mplring 18669	. . . . . . . . . . . . . . . . 17 $/\$
195	2, 97, 194	syl2anc 666	. . . . . . . . . . . . . . . 16
196	50	ringmgp 17779	. . . . . . . . . . . . . . . 16
197	195, 196	syl 17	. . . . . . . . . . . . . . 15
198	197	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
199	1	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
200		mplcoe5.c	. . . . . . . . . . . . . . . . 17
201		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
202	201	oveq2d 6319	. . . . . . . . . . . . . . . . . . 19
203	201	oveq1d 6318	. . . . . . . . . . . . . . . . . . 19
204	202, 203	eqeq12d 2445	. . . . . . . . . . . . . . . . . 18
205		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
206	205	oveq1d 6318	. . . . . . . . . . . . . . . . . . 19
207	205	oveq2d 6319	. . . . . . . . . . . . . . . . . . 19
208	206, 207	eqeq12d 2445	. . . . . . . . . . . . . . . . . 18
209	204, 208	cbvral2v 3064	. . . . . . . . . . . . . . . . 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 18684	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Cntz
213	101, 131	syl5ss 3476	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	213	sselda 3465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
215	197	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
216	7	ffvelrnda 6035	. . . . . . . . . . . . . . . . 17 $/\$
217	2	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
218	97	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
219		simpr 463	. . . . . . . . . . . . . . . . . 18 $/\$
220	94, 141, 106, 217, 218, 219	mvrcl 18666	. . . . . . . . . . . . . . . . 17 $/\$
221	190, 140	mulgnn0cl 16767	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
222	215, 216, 220, 221	syl3anc 1265	. . . . . . . . . . . . . . . 16 $/\$
223	222	adantlr 720	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
224	214, 223	syldan 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
225	94, 141, 106, 107, 108, 135	mvrcl 18666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	190, 140	mulgnn0cl 16767	. . . . . . . . . . . . . . 15 $/\$ $/\$
227	198, 136, 225, 226	syl3anc 1265	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
228		fveq2 5879	. . . . . . . . . . . . . . . 16
229		fveq2 5879	. . . . . . . . . . . . . . . 16
230	228, 229	oveq12d 6321	. . . . . . . . . . . . . . 15
231	230	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
232	190, 191, 192, 193, 198, 118, 212, 224, 135, 155, 227, 231	gsumzunsnd 17581	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ _g _g
233	189, 232	eqeq12d 2445	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ _g _g
234	105, 233	syl5ibr 225	. . . . . . . . . . 11 $/\$ $/\$ $/\$ _g _g
235	234	expr 619	. . . . . . . . . 10 $/\$ $/\$ _g _g
236	235	a2d 30	. . . . . . . . 9 $/\$ $/\$ _g _g
237	104, 236	syl5 34	. . . . . . . 8 $/\$ $/\$ _g _g
238	237	expcom 437	. . . . . . 7 $/\$ _g _g
239	238	a2d 30	. . . . . 6 $/\$ _g _g
240	57, 69, 81, 93, 100, 239	findcard2s 7816	. . . . 5 _g
241	34, 240	mpcom 38	. . . 4 _g
242	33, 241	mpd 15	. . 3 _g
243	33	resmptd 5173	. . . 4
244	243	oveq2d 6319	. . 3 _g _g
245		eqid 2423	. . . . 5
246	222, 245	fmptd 6059	. . . 4
247		ssid 3484	. . . . . 6
248	247	a1i 11	. . . . 5
249	94, 3, 95, 96, 2, 50, 140, 141, 97, 1, 200, 248	mplcoe5lem 18684	. . . 4 Cntz
250	7, 16, 2, 18	suppssr 6955	. . . . . . 7 $/\$ $\$
251	250	oveq1d 6318	. . . . . 6 $/\$ $\$
252		eldifi 3588	. . . . . . . 8 $\$
253	252, 220	sylan2 477	. . . . . . 7 $/\$ $\$
254	190, 52, 140	mulg0 16756	. . . . . . 7
255	253, 254	syl 17	. . . . . 6 $/\$ $\$
256	251, 255	eqtrd 2464	. . . . 5 $/\$ $\$
257	256, 2	suppss2 6958	. . . 4 supp
258		mptexg 6148	. . . . . 6
259	2, 258	syl 17	. . . . 5
260		funmpt 5635	. . . . . 6
261	260	a1i 11	. . . . 5
262		fvex 5889	. . . . . 6
263	262	a1i 11	. . . . 5
264		suppssfifsupp 7902	. . . . 5 $/\$ $/\$ $/\$ $/\$ supp finSupp
265	259, 261, 263, 34, 257, 264	syl32anc 1273	. . . 4 finSupp
266	190, 52, 192, 197, 2, 246, 249, 257, 265	gsumzres 17536	. . 3 _g _g
267	242, 244, 266	3eqtr2d 2470	. 2 _g
268	29, 267	eqtrd 2464	1 _g

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1438

wcel 1869

wral 2776

crab 2780

cvv 3082 $\$ cdif 3434

cun 3435

wss 3437

c0 3762

cif 3910

csn 3997 class class class wbr 4421

cmpt 4480

cxp 4849

ccnv 4850

cdm 4851

cres 4853

cima 4854

wfun 5593

wf 5595

cfv 5599 (class class class)co 6303

cof 6541 supp csupp 6923

cmap 7478

cfn 7575 finSupp cfsupp 7887

cc0 9541

caddc 9544

cn 10611

cn0 10871

cbs 15114

cplusg 15183

cmulr 15184

c0g 15331

_g cgsu 15332

cmnd 16528 ._gcmg 16665 Cntzccntz 16962 mulGrpcmgp 17716

cur 17728

crg 17773 mVar cmvr 18569 mPoly cmpl 18570

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-inf2 8150 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-int 4254 df-iun 4299 df-iin 4300 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-se 4811 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-isom 5608 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-of 6543 df-ofr 6544 df-om 6705 df-1st 6805 df-2nd 6806 df-supp 6924 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-1o 7188 df-2o 7189 df-oadd 7192 df-er 7369 df-map 7480 df-pm 7481 df-ixp 7529 df-en 7576 df-dom 7577 df-sdom 7578 df-fin 7579 df-fsupp 7888 df-oi 8029 df-card 8376 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-nn 10612 df-2 10670 df-3 10671 df-4 10672 df-5 10673 df-6 10674 df-7 10675 df-8 10676 df-9 10677 df-n0 10872 df-z 10940 df-uz 11162 df-fz 11787 df-fzo 11918 df-seq 12215 df-hash 12517 df-struct 15116 df-ndx 15117 df-slot 15118 df-base 15119 df-sets 15120 df-ress 15121 df-plusg 15196 df-mulr 15197 df-sca 15199 df-vsca 15200 df-tset 15202 df-0g 15333 df-gsum 15334 df-mre 15485 df-mrc 15486 df-acs 15488 df-mgm 16481 df-sgrp 16520 df-mnd 16530 df-mhm 16575 df-submnd 16576 df-grp 16666 df-minusg 16667 df-mulg 16669 df-subg 16807 df-ghm 16874 df-cntz 16964 df-cmn 17425 df-abl 17426 df-mgp 17717 df-ur 17729 df-srg 17733 df-ring 17775 df-subrg 17999 df-psr 18573 df-mvr 18574 df-mpl 18575

This theorem is referenced by: mplcoe2 18686 ply1coe 18882

W3C validator