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

Theorem mplcoe2 17353
 Description: Decompose a monomial into a finite product of powers of variables. (The assumption that is a commutative ring is not strictly necessary, because the submonoid of monomials is in the center of the multiplicative monoid of polynomials, but it simplifies the proof.) (Contributed by Mario Carneiro, 10-Jan-2015.)
Hypotheses
Ref Expression
mplcoe1.p
mplcoe1.d
mplcoe1.z
mplcoe1.o
mplcoe1.i
mplcoe2.g
mplcoe2.m
mplcoe2.v
mplcoe2.r
mplcoe2.y
Assertion
Ref Expression
mplcoe2
Distinct variable groups:   ,   ,,   ,   ,,,I   ,,   ,,   ,,   P,   ,   ,   ,,,   ,,,

Proof of Theorem mplcoe2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplcoe2.y . . . . . . . . 9
2 mplcoe1.i . . . . . . . . . 10
3 mplcoe1.d . . . . . . . . . . 11
43psrbag 17251 . . . . . . . . . 10
52, 4syl 16 . . . . . . . . 9
61, 5mpbid 204 . . . . . . . 8
76simpld 449 . . . . . . 7
87feqmptd 5714 . . . . . 6
9 iftrue 3774 . . . . . . . . 9
109adantl 456 . . . . . . . 8
11 eldif 3315 . . . . . . . . . 10
12 ifid 3803 . . . . . . . . . . 11
13 nn0supp 10580 . . . . . . . . . . . . . . 15
147, 13syl 16 . . . . . . . . . . . . . 14
15 eqimss 3385 . . . . . . . . . . . . . 14
1614, 15syl 16 . . . . . . . . . . . . 13
177, 16suppssrOLD 5807 . . . . . . . . . . . 12
1817ifeq2d 3785 . . . . . . . . . . 11
1912, 18syl5reqr 2469 . . . . . . . . . 10
2011, 19sylan2br 466 . . . . . . . . 9
2120anassrs 633 . . . . . . . 8
2210, 21pm2.61dan 774 . . . . . . 7
2322mpteq2dva 4353 . . . . . 6
248, 23eqtr4d 2457 . . . . 5
2524eqeq2d 2433 . . . 4
2625ifbid 3788 . . 3
2726mpteq2dv 4354 . 2
28 cnvimass 5161 . . . . 5
29 fdm 5533 . . . . . 6
307, 29syl 16 . . . . 5
3128, 30syl5sseq 3381 . . . 4
326simprd 453 . . . . 5
33 sseq1 3354 . . . . . . . 8
34 noel 3618 . . . . . . . . . . . . . . . 16
35 eleq2 2483 . . . . . . . . . . . . . . . 16
3634, 35mtbiri 297 . . . . . . . . . . . . . . 15
37 iffalse 3776 . . . . . . . . . . . . . . 15
3836, 37syl 16 . . . . . . . . . . . . . 14
3938mpteq2dv 4354 . . . . . . . . . . . . 13
40 fconstmpt 4853 . . . . . . . . . . . . 13
4139, 40syl6eqr 2472 . . . . . . . . . . . 12
4241eqeq2d 2433 . . . . . . . . . . 11
4342ifbid 3788 . . . . . . . . . 10
4443mpteq2dv 4354 . . . . . . . . 9
45 mpteq1 4347 . . . . . . . . . . . 12
46 mpt0 5508 . . . . . . . . . . . 12
4745, 46syl6eq 2470 . . . . . . . . . . 11
4847oveq2d 6077 . . . . . . . . . 10
49 mplcoe2.g . . . . . . . . . . . 12
50 eqid 2422 . . . . . . . . . . . 12
5149, 50rngidval 16475 . . . . . . . . . . 11
5251gsum0 15447 . . . . . . . . . 10
5348, 52syl6eq 2470 . . . . . . . . 9
5444, 53eqeq12d 2436 . . . . . . . 8
5533, 54imbi12d 314 . . . . . . 7
5655imbi2d 310 . . . . . 6
57 sseq1 3354 . . . . . . . 8
58 eleq2 2483 . . . . . . . . . . . . . 14
5958ifbid 3788 . . . . . . . . . . . . 13
6059mpteq2dv 4354 . . . . . . . . . . . 12
6160eqeq2d 2433 . . . . . . . . . . 11
6261ifbid 3788 . . . . . . . . . 10
6362mpteq2dv 4354 . . . . . . . . 9
64 mpteq1 4347 . . . . . . . . . 10
6564oveq2d 6077 . . . . . . . . 9
6663, 65eqeq12d 2436 . . . . . . . 8
6757, 66imbi12d 314 . . . . . . 7
6867imbi2d 310 . . . . . 6
69 sseq1 3354 . . . . . . . 8
70 eleq2 2483 . . . . . . . . . . . . . 14
7170ifbid 3788 . . . . . . . . . . . . 13
7271mpteq2dv 4354 . . . . . . . . . . . 12
7372eqeq2d 2433 . . . . . . . . . . 11
7473ifbid 3788 . . . . . . . . . 10
7574mpteq2dv 4354 . . . . . . . . 9
76 mpteq1 4347 . . . . . . . . . 10
7776oveq2d 6077 . . . . . . . . 9
7875, 77eqeq12d 2436 . . . . . . . 8
7969, 78imbi12d 314 . . . . . . 7
8079imbi2d 310 . . . . . 6
81 sseq1 3354 . . . . . . . 8
82 eleq2 2483 . . . . . . . . . . . . . 14
8382ifbid 3788 . . . . . . . . . . . . 13
8483mpteq2dv 4354 . . . . . . . . . . . 12
8584eqeq2d 2433 . . . . . . . . . . 11
8685ifbid 3788 . . . . . . . . . 10
8786mpteq2dv 4354 . . . . . . . . 9
88 mpteq1 4347 . . . . . . . . . 10
8988oveq2d 6077 . . . . . . . . 9
9087, 89eqeq12d 2436 . . . . . . . 8
9181, 90imbi12d 314 . . . . . . 7
9291imbi2d 310 . . . . . 6
93 mplcoe1.p . . . . . . . . 9
94 mplcoe1.z . . . . . . . . 9
95 mplcoe1.o . . . . . . . . 9
96 mplcoe2.r . . . . . . . . . 10
97 crngrng 16483 . . . . . . . . . 10
9896, 97syl 16 . . . . . . . . 9
9993, 3, 94, 95, 50, 2, 98mpl1 17330 . . . . . . . 8
10099eqcomd 2427 . . . . . . 7
101100a1d 24 . . . . . 6
102 ssun1 3496 . . . . . . . . . . 11
103 sstr2 3340 . . . . . . . . . . 11
104102, 103ax-mp 5 . . . . . . . . . 10
105104imim1i 57 . . . . . . . . 9
106 oveq1 6068 . . . . . . . . . . . 12
107 eqid 2422 . . . . . . . . . . . . . . 15
1082adantr 455 . . . . . . . . . . . . . . 15
10998adantr 455 . . . . . . . . . . . . . . 15
1107adantr 455 . . . . . . . . . . . . . . . . . . 19
111110ffvelrnda 5813 . . . . . . . . . . . . . . . . . 18
112 0nn0 10540 . . . . . . . . . . . . . . . . . 18
113 ifcl 3808 . . . . . . . . . . . . . . . . . 18
114111, 112, 113sylancl 647 . . . . . . . . . . . . . . . . 17
115 eqid 2422 . . . . . . . . . . . . . . . . 17
116114, 115fmptd 5837 . . . . . . . . . . . . . . . 16
117 nn0supp 10580 . . . . . . . . . . . . . . . . . 18
118116, 117syl 16 . . . . . . . . . . . . . . . . 17
119 simprll 746 . . . . . . . . . . . . . . . . . 18
120 eldifn 3456 . . . . . . . . . . . . . . . . . . . . 21
121120adantl 456 . . . . . . . . . . . . . . . . . . . 20
122 iffalse 3776 . . . . . . . . . . . . . . . . . . . 20
123121, 122syl 16 . . . . . . . . . . . . . . . . . . 19
124123suppss2OLD 6285 . . . . . . . . . . . . . . . . . 18
125 ssfi 7492 . . . . . . . . . . . . . . . . . 18
126119, 124, 125syl2anc 646 . . . . . . . . . . . . . . . . 17
127118, 126eqeltrrd 2497 . . . . . . . . . . . . . . . 16
1283psrbag 17251 . . . . . . . . . . . . . . . . 17
129108, 128syl 16 . . . . . . . . . . . . . . . 16
130116, 127, 129mpbir2and 898 . . . . . . . . . . . . . . 15
131 eqid 2422 . . . . . . . . . . . . . . 15
132 ssun2 3497 . . . . . . . . . . . . . . . . . . . . . 22
133 simprr 741 . . . . . . . . . . . . . . . . . . . . . 22
134132, 133syl5ss 3344 . . . . . . . . . . . . . . . . . . . . 21
135 vex 2954 . . . . . . . . . . . . . . . . . . . . . 22
136135snss 3974 . . . . . . . . . . . . . . . . . . . . 21
137134, 136sylibr 206 . . . . . . . . . . . . . . . . . . . 20
138110, 137ffvelrnd 5814 . . . . . . . . . . . . . . . . . . 19
139138adantr 455 . . . . . . . . . . . . . . . . . 18
140 ifcl 3808 . . . . . . . . . . . . . . . . . 18
141139, 112, 140sylancl 647 . . . . . . . . . . . . . . . . 17
142 eqid 2422 . . . . . . . . . . . . . . . . 17
143141, 142fmptd 5837 . . . . . . . . . . . . . . . 16
144 nn0supp 10580 . . . . . . . . . . . . . . . . . 18
145143, 144syl 16 . . . . . . . . . . . . . . . . 17
146 snfi 7349 . . . . . . . . . . . . . . . . . 18
147 eldifsni 3976 . . . . . . . . . . . . . . . . . . . . . 22
148147adantl 456 . . . . . . . . . . . . . . . . . . . . 21
149148neneqd 2603 . . . . . . . . . . . . . . . . . . . 20
150 iffalse 3776 . . . . . . . . . . . . . . . . . . . 20
151149, 150syl 16 . . . . . . . . . . . . . . . . . . 19
152151suppss2OLD 6285 . . . . . . . . . . . . . . . . . 18
153 ssfi 7492 . . . . . . . . . . . . . . . . . 18
154146, 152, 153sylancr 648 . . . . . . . . . . . . . . . . 17
155145, 154eqeltrrd 2497 . . . . . . . . . . . . . . . 16
1563psrbag 17251 . . . . . . . . . . . . . . . . 17
157108, 156syl 16 . . . . . . . . . . . . . . . 16
158143, 155, 157mpbir2and 898 . . . . . . . . . . . . . . 15