Step | Hyp | Ref
| Expression |
1 | | mplcoe3.n |
. 2
|
2 | | ifeq1 4090 |
. . . . . . . . . . 11
|
3 | | ifid 4125 |
. . . . . . . . . . 11
|
4 | 2, 3 | syl6eq 2672 |
. . . . . . . . . 10
|
5 | 4 | mpteq2dv 4745 |
. . . . . . . . 9
|
6 | | fconstmpt 5163 |
. . . . . . . . 9
|
7 | 5, 6 | syl6eqr 2674 |
. . . . . . . 8
|
8 | 7 | eqeq2d 2632 |
. . . . . . 7
|
9 | 8 | ifbid 4108 |
. . . . . 6
|
10 | 9 | mpteq2dv 4745 |
. . . . 5
|
11 | | oveq1 6657 |
. . . . 5
|
12 | 10, 11 | eqeq12d 2637 |
. . . 4
|
13 | 12 | imbi2d 330 |
. . 3
|
14 | | ifeq1 4090 |
. . . . . . . . 9
|
15 | 14 | mpteq2dv 4745 |
. . . . . . . 8
|
16 | 15 | eqeq2d 2632 |
. . . . . . 7
|
17 | 16 | ifbid 4108 |
. . . . . 6
|
18 | 17 | mpteq2dv 4745 |
. . . . 5
|
19 | | oveq1 6657 |
. . . . 5
|
20 | 18, 19 | eqeq12d 2637 |
. . . 4
|
21 | 20 | imbi2d 330 |
. . 3
|
22 | | ifeq1 4090 |
. . . . . . . . 9
|
23 | 22 | mpteq2dv 4745 |
. . . . . . . 8
|
24 | 23 | eqeq2d 2632 |
. . . . . . 7
|
25 | 24 | ifbid 4108 |
. . . . . 6
|
26 | 25 | mpteq2dv 4745 |
. . . . 5
|
27 | | oveq1 6657 |
. . . . 5
|
28 | 26, 27 | eqeq12d 2637 |
. . . 4
|
29 | 28 | imbi2d 330 |
. . 3
|
30 | | ifeq1 4090 |
. . . . . . . . 9
|
31 | 30 | mpteq2dv 4745 |
. . . . . . . 8
|
32 | 31 | eqeq2d 2632 |
. . . . . . 7
|
33 | 32 | ifbid 4108 |
. . . . . 6
|
34 | 33 | mpteq2dv 4745 |
. . . . 5
|
35 | | oveq1 6657 |
. . . . 5
|
36 | 34, 35 | eqeq12d 2637 |
. . . 4
|
37 | 36 | imbi2d 330 |
. . 3
|
38 | | mplcoe1.p |
. . . . . 6
mPoly |
39 | | mplcoe2.v |
. . . . . 6
mVar |
40 | | eqid 2622 |
. . . . . 6
|
41 | | mplcoe1.i |
. . . . . 6
|
42 | | mplcoe3.r |
. . . . . 6
|
43 | | mplcoe3.x |
. . . . . 6
|
44 | 38, 39, 40, 41, 42, 43 | mvrcl 19449 |
. . . . 5
|
45 | | mplcoe2.g |
. . . . . . 7
mulGrp |
46 | 45, 40 | mgpbas 18495 |
. . . . . 6
|
47 | | eqid 2622 |
. . . . . . 7
|
48 | 45, 47 | ringidval 18503 |
. . . . . 6
|
49 | | mplcoe2.m |
. . . . . 6
.g |
50 | 46, 48, 49 | mulg0 17546 |
. . . . 5
|
51 | 44, 50 | syl 17 |
. . . 4
|
52 | | mplcoe1.d |
. . . . 5
|
53 | | mplcoe1.z |
. . . . 5
|
54 | | mplcoe1.o |
. . . . 5
|
55 | 38, 52, 53, 54, 47, 41, 42 | mpl1 19444 |
. . . 4
|
56 | 51, 55 | eqtr2d 2657 |
. . 3
|
57 | | oveq1 6657 |
. . . . . 6
|
58 | 41 | adantr 481 |
. . . . . . . . 9
|
59 | 42 | adantr 481 |
. . . . . . . . 9
|
60 | 52 | snifpsrbag 19366 |
. . . . . . . . . 10
|
61 | 41, 60 | sylan 488 |
. . . . . . . . 9
|
62 | | eqid 2622 |
. . . . . . . . 9
|
63 | | 1nn0 11308 |
. . . . . . . . . . 11
|
64 | 63 | a1i 11 |
. . . . . . . . . 10
|
65 | 52 | snifpsrbag 19366 |
. . . . . . . . . 10
|
66 | 41, 64, 65 | syl2an 494 |
. . . . . . . . 9
|
67 | 38, 40, 53, 54, 52, 58, 59, 61, 62, 66 | mplmonmul 19464 |
. . . . . . . 8
|
68 | 43 | adantr 481 |
. . . . . . . . . . 11
|
69 | 39, 52, 53, 54, 58, 59, 68 | mvrval 19421 |
. . . . . . . . . 10
|
70 | 69 | eqcomd 2628 |
. . . . . . . . 9
|
71 | 70 | oveq2d 6666 |
. . . . . . . 8
|
72 | | simplr 792 |
. . . . . . . . . . . . . 14
|
73 | | 0nn0 11307 |
. . . . . . . . . . . . . 14
|
74 | | ifcl 4130 |
. . . . . . . . . . . . . 14
|
75 | 72, 73, 74 | sylancl 694 |
. . . . . . . . . . . . 13
|
76 | 63, 73 | keepel 4155 |
. . . . . . . . . . . . . 14
|
77 | 76 | a1i 11 |
. . . . . . . . . . . . 13
|
78 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
79 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
80 | 58, 75, 77, 78, 79 | offval2 6914 |
. . . . . . . . . . . 12
|
81 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
|
82 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
|
83 | 81, 82 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
84 | | iftrue 4092 |
. . . . . . . . . . . . . . 15
|
85 | 83, 84 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
86 | | 00id 10211 |
. . . . . . . . . . . . . . 15
|
87 | | iffalse 4095 |
. . . . . . . . . . . . . . . 16
|
88 | | iffalse 4095 |
. . . . . . . . . . . . . . . 16
|
89 | 87, 88 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
90 | | iffalse 4095 |
. . . . . . . . . . . . . . 15
|
91 | 86, 89, 90 | 3eqtr4a 2682 |
. . . . . . . . . . . . . 14
|
92 | 85, 91 | pm2.61i 176 |
. . . . . . . . . . . . 13
|
93 | 92 | mpteq2i 4741 |
. . . . . . . . . . . 12
|
94 | 80, 93 | syl6eq 2672 |
. . . . . . . . . . 11
|
95 | 94 | eqeq2d 2632 |
. . . . . . . . . 10
|
96 | 95 | ifbid 4108 |
. . . . . . . . 9
|
97 | 96 | mpteq2dv 4745 |
. . . . . . . 8
|
98 | 67, 71, 97 | 3eqtr3rd 2665 |
. . . . . . 7
|
99 | 38 | mplring 19452 |
. . . . . . . . . . 11
|
100 | 41, 42, 99 | syl2anc 693 |
. . . . . . . . . 10
|
101 | 45 | ringmgp 18553 |
. . . . . . . . . 10
|
102 | 100, 101 | syl 17 |
. . . . . . . . 9
|
103 | 102 | adantr 481 |
. . . . . . . 8
|
104 | | simpr 477 |
. . . . . . . 8
|
105 | 44 | adantr 481 |
. . . . . . . 8
|
106 | 45, 62 | mgpplusg 18493 |
. . . . . . . . 9
|
107 | 46, 49, 106 | mulgnn0p1 17552 |
. . . . . . . 8
|
108 | 103, 104,
105, 107 | syl3anc 1326 |
. . . . . . 7
|
109 | 98, 108 | eqeq12d 2637 |
. . . . . 6
|
110 | 57, 109 | syl5ibr 236 |
. . . . 5
|
111 | 110 | expcom 451 |
. . . 4
|
112 | 111 | a2d 29 |
. . 3
|
113 | 13, 21, 29, 37, 56, 112 | nn0ind 11472 |
. 2
|
114 | 1, 113 | mpcom 38 |
1
|