mplcoe5 - Metamath Proof Explorer

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

Theorem mplcoe5 18453

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

is a commutative ring (as in mplcoe2 18454), 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 18335	. . . . . . . . . 10 $/\$
5	2, 4	syl 17	. . . . . . . . 9 $/\$
6	1, 5	mpbid 212	. . . . . . . 8 $/\$
7	6	simpld 459	. . . . . . 7
8	7	feqmptd 5904	. . . . . 6
9		iftrue 3893	. . . . . . . . 9
10	9	adantl 466	. . . . . . . 8 $/\$ $/\$
11		eldif 3426	. . . . . . . . . 10 $\$ $/\$
12		ifid 3924	. . . . . . . . . . 11
13		frnnn0supp 10892	. . . . . . . . . . . . . . 15 $/\$ supp
14	2, 7, 13	syl2anc 661	. . . . . . . . . . . . . 14 supp
15		eqimss 3496	. . . . . . . . . . . . . 14 supp supp
16	14, 15	syl 17	. . . . . . . . . . . . 13 supp
17		c0ex 9622	. . . . . . . . . . . . . 14
18	17	a1i 11	. . . . . . . . . . . . 13
19	7, 16, 2, 18	suppssr 6936	. . . . . . . . . . . 12 $/\$ $\$
20	19	ifeq2d 3906	. . . . . . . . . . 11 $/\$ $\$
21	12, 20	syl5reqr 2460	. . . . . . . . . 10 $/\$ $\$
22	11, 21	sylan2br 476	. . . . . . . . 9 $/\$ $/\$
23	22	anassrs 648	. . . . . . . 8 $/\$ $/\$
24	10, 23	pm2.61dan 794	. . . . . . 7 $/\$
25	24	mpteq2dva 4483	. . . . . 6
26	8, 25	eqtr4d 2448	. . . . 5
27	26	eqeq2d 2418	. . . 4
28	27	ifbid 3909	. . 3
29	28	mpteq2dv 4484	. 2
30		cnvimass 5179	. . . . 5
31		fdm 5720	. . . . . 6
32	7, 31	syl 17	. . . . 5
33	30, 32	syl5sseq 3492	. . . 4
34	6	simprd 463	. . . . 5
35		sseq1 3465	. . . . . . . 8
36		noel 3744	. . . . . . . . . . . . . . . 16
37		eleq2 2477	. . . . . . . . . . . . . . . 16
38	36, 37	mtbiri 303	. . . . . . . . . . . . . . 15
39	38	iffalsed 3898	. . . . . . . . . . . . . 14
40	39	mpteq2dv 4484	. . . . . . . . . . . . 13
41		fconstmpt 4869	. . . . . . . . . . . . 13
42	40, 41	syl6eqr 2463	. . . . . . . . . . . 12
43	42	eqeq2d 2418	. . . . . . . . . . 11
44	43	ifbid 3909	. . . . . . . . . 10
45	44	mpteq2dv 4484	. . . . . . . . 9
46		mpteq1 4477	. . . . . . . . . . . 12
47		mpt0 5693	. . . . . . . . . . . 12
48	46, 47	syl6eq 2461	. . . . . . . . . . 11
49	48	oveq2d 6296	. . . . . . . . . 10 _g _g
50		mplcoe2.g	. . . . . . . . . . . 12 mulGrp
51		eqid 2404	. . . . . . . . . . . 12
52	50, 51	ringidval 17477	. . . . . . . . . . 11
53	52	gsum0 16231	. . . . . . . . . 10 _g
54	49, 53	syl6eq 2461	. . . . . . . . 9 _g
55	45, 54	eqeq12d 2426	. . . . . . . 8 _g
56	35, 55	imbi12d 320	. . . . . . 7 _g
57	56	imbi2d 316	. . . . . 6 _g
58		sseq1 3465	. . . . . . . 8
59		eleq2 2477	. . . . . . . . . . . . . 14
60	59	ifbid 3909	. . . . . . . . . . . . 13
61	60	mpteq2dv 4484	. . . . . . . . . . . 12
62	61	eqeq2d 2418	. . . . . . . . . . 11
63	62	ifbid 3909	. . . . . . . . . 10
64	63	mpteq2dv 4484	. . . . . . . . 9
65		mpteq1 4477	. . . . . . . . . 10
66	65	oveq2d 6296	. . . . . . . . 9 _g _g
67	64, 66	eqeq12d 2426	. . . . . . . 8 _g _g
68	58, 67	imbi12d 320	. . . . . . 7 _g _g
69	68	imbi2d 316	. . . . . 6 _g _g
70		sseq1 3465	. . . . . . . 8
71		eleq2 2477	. . . . . . . . . . . . . 14
72	71	ifbid 3909	. . . . . . . . . . . . 13
73	72	mpteq2dv 4484	. . . . . . . . . . . 12
74	73	eqeq2d 2418	. . . . . . . . . . 11
75	74	ifbid 3909	. . . . . . . . . 10
76	75	mpteq2dv 4484	. . . . . . . . 9
77		mpteq1 4477	. . . . . . . . . 10
78	77	oveq2d 6296	. . . . . . . . 9 _g _g
79	76, 78	eqeq12d 2426	. . . . . . . 8 _g _g
80	70, 79	imbi12d 320	. . . . . . 7 _g _g
81	80	imbi2d 316	. . . . . 6 _g _g
82		sseq1 3465	. . . . . . . 8
83		eleq2 2477	. . . . . . . . . . . . . 14
84	83	ifbid 3909	. . . . . . . . . . . . 13
85	84	mpteq2dv 4484	. . . . . . . . . . . 12
86	85	eqeq2d 2418	. . . . . . . . . . 11
87	86	ifbid 3909	. . . . . . . . . 10
88	87	mpteq2dv 4484	. . . . . . . . 9
89		mpteq1 4477	. . . . . . . . . 10
90	89	oveq2d 6296	. . . . . . . . 9 _g _g
91	88, 90	eqeq12d 2426	. . . . . . . 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 18428	. . . . . . . 8
99	98	eqcomd 2412	. . . . . . 7
100	99	a1d 26	. . . . . 6
101		ssun1 3608	. . . . . . . . . . 11
102		sstr2 3451	. . . . . . . . . . 11
103	101, 102	ax-mp 5	. . . . . . . . . 10
104	103	imim1i 59	. . . . . . . . 9 _g _g
105		oveq1 6287	. . . . . . . . . . . 12 _g _g
106		eqid 2404	. . . . . . . . . . . . . . 15
107	2	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
108	97	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
109	7	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
110	109	ffvelrnda 6011	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
111		0nn0 10853	. . . . . . . . . . . . . . . . . 18
112		ifcl 3929	. . . . . . . . . . . . . . . . . 18 $/\$
113	110, 111, 112	sylancl 662	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
114		eqid 2404	. . . . . . . . . . . . . . . . 17
115	113, 114	fmptd 6035	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
116		frnnn0supp 10892	. . . . . . . . . . . . . . . . . 18 $/\$ supp
117	107, 115, 116	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
118		simprll 766	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
119		eldifn 3568	. . . . . . . . . . . . . . . . . . . . 21 $\$
120	119	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$
121	120	iffalsed 3898	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$
122	121, 107	suppss2 6939	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ supp
123		ssfi 7777	. . . . . . . . . . . . . . . . . 18 $/\$ supp supp
124	118, 122, 123	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
125	117, 124	eqeltrrd 2493	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
126	3	psrbag 18335	. . . . . . . . . . . . . . . . 17 $/\$
127	107, 126	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	115, 125, 127	mpbir2and 925	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
129		eqid 2404	. . . . . . . . . . . . . . 15
130		ssun2 3609	. . . . . . . . . . . . . . . . . . 19
131		simprr 760	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
132	130, 131	syl5ss 3455	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
133		vex 3064	. . . . . . . . . . . . . . . . . . 19
134	133	snss 4098	. . . . . . . . . . . . . . . . . 18
135	132, 134	sylibr 214	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
136	109, 135	ffvelrnd 6012	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
137	3	snifpsrbag 18337	. . . . . . . . . . . . . . . 16 $/\$
138	107, 136, 137	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
139	94, 106, 95, 96, 3, 107, 108, 128, 129, 138	mplmonmul 18448	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
140		mplcoe2.m	. . . . . . . . . . . . . . . 16 ._g
141		mplcoe2.v	. . . . . . . . . . . . . . . 16 mVar
142	94, 3, 95, 96, 107, 50, 140, 141, 108, 135, 136	mplcoe3 18450	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
143	142	oveq2d 6296	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	136	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
145		ifcl 3929	. . . . . . . . . . . . . . . . . . . 20 $/\$
146	144, 111, 145	sylancl 662	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
147		eqidd 2405	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
148		eqidd 2405	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
149	107, 113, 146, 147, 148	offval2 6540	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
150	110	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
151	150	nn0cnd 10897	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
152	151	addid2d 9817	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
153		elsni 3999	. . . . . . . . . . . . . . . . . . . . . . . . 25
154	153	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
155		simprlr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
156	155	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
157	154, 156	eqneltrd 2513	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
158	157	iffalsed 3898	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
159	154	iftrued 3895	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
160	154	fveq2d 5855	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
161	159, 160	eqtr4d 2448	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
162	158, 161	oveq12d 6298	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
163		simpr 461	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
164	130, 163	sseldi 3442	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
165	164	iftrued 3895	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
166	152, 162, 165	3eqtr4d 2455	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
167	113	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
168	167	nn0cnd 10897	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	addid1d 9816	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
170		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$
171		elsn 3988	. . . . . . . . . . . . . . . . . . . . . . . 24
172	170, 171	sylnib 304	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
173	172	iffalsed 3898	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
174	173	oveq2d 6296	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
175		biorf 405	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
176		elun 3586	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
177		orcom 387	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$
178	176, 177	bitri 251	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
179	175, 178	syl6rbbr 266	. . . . . . . . . . . . . . . . . . . . . . 23
180	179	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
181	180	ifbid 3909	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
182	169, 174, 181	3eqtr4d 2455	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
183	166, 182	pm2.61dan 794	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
184	183	mpteq2dva 4483	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
185	149, 184	eqtrd 2445	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
186	185	eqeq2d 2418	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
187	186	ifbid 3909	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188	187	mpteq2dv 4484	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
189	139, 143, 188	3eqtr3rd 2454	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
190	50, 106	mgpbas 17469	. . . . . . . . . . . . . 14
191	50, 129	mgpplusg 17467	. . . . . . . . . . . . . 14
192		eqid 2404	. . . . . . . . . . . . . 14 Cntz Cntz
193		eqid 2404	. . . . . . . . . . . . . 14
194	94	mplring 18436	. . . . . . . . . . . . . . . . 17 $/\$
195	2, 97, 194	syl2anc 661	. . . . . . . . . . . . . . . 16
196	50	ringmgp 17526	. . . . . . . . . . . . . . . 16
197	195, 196	syl 17	. . . . . . . . . . . . . . 15
198	197	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
199	1	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
200		mplcoe5.c	. . . . . . . . . . . . . . . . 17
201		fveq2 5851	. . . . . . . . . . . . . . . . . . . 20
202	201	oveq2d 6296	. . . . . . . . . . . . . . . . . . 19
203	201	oveq1d 6295	. . . . . . . . . . . . . . . . . . 19
204	202, 203	eqeq12d 2426	. . . . . . . . . . . . . . . . . 18
205		fveq2 5851	. . . . . . . . . . . . . . . . . . . 20
206	205	oveq1d 6295	. . . . . . . . . . . . . . . . . . 19
207	205	oveq2d 6296	. . . . . . . . . . . . . . . . . . 19
208	206, 207	eqeq12d 2426	. . . . . . . . . . . . . . . . . 18
209	204, 208	cbvral2v 3044	. . . . . . . . . . . . . . . . 17
210	200, 209	sylib 198	. . . . . . . . . . . . . . . 16
211	210	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
212	94, 3, 95, 96, 107, 50, 140, 141, 108, 199, 211, 131	mplcoe5lem 18452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ Cntz
213	101, 131	syl5ss 3455	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	213	sselda 3444	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
215	197	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$
216	7	ffvelrnda 6011	. . . . . . . . . . . . . . . . 17 $/\$
217	2	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
218	97	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
219		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$
220	94, 141, 106, 217, 218, 219	mvrcl 18433	. . . . . . . . . . . . . . . . 17 $/\$
221	190, 140	mulgnn0cl 16484	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
222	215, 216, 220, 221	syl3anc 1232	. . . . . . . . . . . . . . . 16 $/\$
223	222	adantlr 715	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
224	214, 223	syldan 470	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
225	94, 141, 106, 107, 108, 135	mvrcl 18433	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
226	190, 140	mulgnn0cl 16484	. . . . . . . . . . . . . . 15 $/\$ $/\$
227	198, 136, 225, 226	syl3anc 1232	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
228		fveq2 5851	. . . . . . . . . . . . . . . 16
229		fveq2 5851	. . . . . . . . . . . . . . . 16
230	228, 229	oveq12d 6298	. . . . . . . . . . . . . . 15
231	230	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
232	190, 191, 192, 193, 198, 118, 212, 224, 135, 155, 227, 231	gsumzunsnd 17305	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ _g _g
233	189, 232	eqeq12d 2426	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ _g _g
234	105, 233	syl5ibr 223	. . . . . . . . . . 11 $/\$ $/\$ $/\$ _g _g
235	234	expr 615	. . . . . . . . . 10 $/\$ $/\$ _g _g
236	235	a2d 28	. . . . . . . . 9 $/\$ $/\$ _g _g
237	104, 236	syl5 32	. . . . . . . 8 $/\$ $/\$ _g _g
238	237	expcom 435	. . . . . . 7 $/\$ _g _g
239	238	a2d 28	. . . . . 6 $/\$ _g _g
240	57, 69, 81, 93, 100, 239	findcard2s 7797	. . . . 5 _g
241	34, 240	mpcom 36	. . . 4 _g
242	33, 241	mpd 15	. . 3 _g
243	33	resmptd 5147	. . . 4
244	243	oveq2d 6296	. . 3 _g _g
245		eqid 2404	. . . . 5
246	222, 245	fmptd 6035	. . . 4
247		ssid 3463	. . . . . 6
248	247	a1i 11	. . . . 5
249	94, 3, 95, 96, 2, 50, 140, 141, 97, 1, 200, 248	mplcoe5lem 18452	. . . 4 Cntz
250	7, 16, 2, 18	suppssr 6936	. . . . . . 7 $/\$ $\$
251	250	oveq1d 6295	. . . . . 6 $/\$ $\$
252		eldifi 3567	. . . . . . . 8 $\$
253	252, 220	sylan2 474	. . . . . . 7 $/\$ $\$
254	190, 52, 140	mulg0 16473	. . . . . . 7
255	253, 254	syl 17	. . . . . 6 $/\$ $\$
256	251, 255	eqtrd 2445	. . . . 5 $/\$ $\$
257	256, 2	suppss2 6939	. . . 4 supp
258		mptexg 6125	. . . . . 6
259	2, 258	syl 17	. . . . 5
260		funmpt 5607	. . . . . 6
261	260	a1i 11	. . . . 5
262		fvex 5861	. . . . . 6
263	262	a1i 11	. . . . 5
264		suppssfifsupp 7880	. . . . 5 $/\$ $/\$ $/\$ $/\$ supp finSupp
265	259, 261, 263, 34, 257, 264	syl32anc 1240	. . . 4 finSupp
266	190, 52, 192, 197, 2, 246, 249, 257, 265	gsumzres 17240	. . 3 _g _g
267	242, 244, 266	3eqtr2d 2451	. 2 _g
268	29, 267	eqtrd 2445	1 _g

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1407

wcel 1844

wral 2756

crab 2760

cvv 3061 $\$ cdif 3413

cun 3414

wss 3416

c0 3740

cif 3887

csn 3974 class class class wbr 4397

cmpt 4455

cxp 4823

ccnv 4824

cdm 4825

cres 4827

cima 4828

wfun 5565

wf 5567

cfv 5571 (class class class)co 6280

cof 6521 supp csupp 6904

cmap 7459

cfn 7556 finSupp cfsupp 7865

cc0 9524

caddc 9527

cn 10578

cn0 10838

cbs 14843

cplusg 14911

cmulr 14912

c0g 15056

_g cgsu 15057

cmnd 16245 ._gcmg 16382 Cntzccntz 16679 mulGrpcmgp 17463

cur 17475

crg 17520 mVar cmvr 18323 mPoly cmpl 18324

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1641 ax-4 1654 ax-5 1727 ax-6 1773 ax-7 1816 ax-8 1846 ax-9 1848 ax-10 1863 ax-11 1868 ax-12 1880 ax-13 2028 ax-ext 2382 ax-rep 4509 ax-sep 4519 ax-nul 4527 ax-pow 4574 ax-pr 4632 ax-un 6576 ax-inf2 8093 ax-cnex 9580 ax-resscn 9581 ax-1cn 9582 ax-icn 9583 ax-addcl 9584 ax-addrcl 9585 ax-mulcl 9586 ax-mulrcl 9587 ax-mulcom 9588 ax-addass 9589 ax-mulass 9590 ax-distr 9591 ax-i2m1 9592 ax-1ne0 9593 ax-1rid 9594 ax-rnegex 9595 ax-rrecex 9596 ax-cnre 9597 ax-pre-lttri 9598 ax-pre-lttrn 9599 ax-pre-ltadd 9600 ax-pre-mulgt0 9601

This theorem depends on definitions: df-bi 187 df-or 370 df-an 371 df-3or 977 df-3an 978 df-tru 1410 df-ex 1636 df-nf 1640 df-sb 1766 df-eu 2244 df-mo 2245 df-clab 2390 df-cleq 2396 df-clel 2399 df-nfc 2554 df-ne 2602 df-nel 2603 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3063 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3741 df-if 3888 df-pw 3959 df-sn 3975 df-pr 3977 df-tp 3979 df-op 3981 df-uni 4194 df-int 4230 df-iun 4275 df-iin 4276 df-br 4398 df-opab 4456 df-mpt 4457 df-tr 4492 df-eprel 4736 df-id 4740 df-po 4746 df-so 4747 df-fr 4784 df-se 4785 df-we 4786 df-xp 4831 df-rel 4832 df-cnv 4833 df-co 4834 df-dm 4835 df-rn 4836 df-res 4837 df-ima 4838 df-pred 5369 df-ord 5415 df-on 5416 df-lim 5417 df-suc 5418 df-iota 5535 df-fun 5573 df-fn 5574 df-f 5575 df-f1 5576 df-fo 5577 df-f1o 5578 df-fv 5579 df-isom 5580 df-riota 6242 df-ov 6283 df-oprab 6284 df-mpt2 6285 df-of 6523 df-ofr 6524 df-om 6686 df-1st 6786 df-2nd 6787 df-supp 6905 df-wrecs 7015 df-recs 7077 df-rdg 7115 df-1o 7169 df-2o 7170 df-oadd 7173 df-er 7350 df-map 7461 df-pm 7462 df-ixp 7510 df-en 7557 df-dom 7558 df-sdom 7559 df-fin 7560 df-fsupp 7866 df-oi 7971 df-card 8354 df-pnf 9662 df-mnf 9663 df-xr 9664 df-ltxr 9665 df-le 9666 df-sub 9845 df-neg 9846 df-nn 10579 df-2 10637 df-3 10638 df-4 10639 df-5 10640 df-6 10641 df-7 10642 df-8 10643 df-9 10644 df-n0 10839 df-z 10908 df-uz 11130 df-fz 11729 df-fzo 11857 df-seq 12154 df-hash 12455 df-struct 14845 df-ndx 14846 df-slot 14847 df-base 14848 df-sets 14849 df-ress 14850 df-plusg 14924 df-mulr 14925 df-sca 14927 df-vsca 14928 df-tset 14930 df-0g 15058 df-gsum 15059 df-mre 15202 df-mrc 15203 df-acs 15205 df-mgm 16198 df-sgrp 16237 df-mnd 16247 df-mhm 16292 df-submnd 16293 df-grp 16383 df-minusg 16384 df-mulg 16386 df-subg 16524 df-ghm 16591 df-cntz 16681 df-cmn 17126 df-abl 17127 df-mgp 17464 df-ur 17476 df-srg 17480 df-ring 17522 df-subrg 17749 df-psr 18327 df-mvr 18328 df-mpl 18329

This theorem is referenced by: mplcoe2 18454 ply1coe 18659

W3C validator