Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
mPoly mPoly |
2 | | psr1baslem 19555 |
. . 3
|
3 | | eqid 2622 |
. . 3
|
4 | | eqid 2622 |
. . 3
|
5 | | 1onn 7719 |
. . . 4
|
6 | 5 | a1i 11 |
. . 3
|
7 | | ply1coe.p |
. . . 4
Poly1 |
8 | | eqid 2622 |
. . . 4
PwSer1 PwSer1 |
9 | | ply1coe.b |
. . . 4
|
10 | 7, 8, 9 | ply1bas 19565 |
. . 3
mPoly |
11 | | ply1coe.n |
. . . 4
|
12 | 7, 1, 11 | ply1vsca 19596 |
. . 3
mPoly |
13 | | simpl 473 |
. . 3
|
14 | | simpr 477 |
. . 3
|
15 | 1, 2, 3, 4, 6, 10,
12, 13, 14 | mplcoe1 19465 |
. 2
mPoly g |
16 | | ply1coe.a |
. . . . . . 7
coe1 |
17 | 16 | fvcoe1 19577 |
. . . . . 6
|
18 | 17 | adantll 750 |
. . . . 5
|
19 | 5 | a1i 11 |
. . . . . . 7
|
20 | | eqid 2622 |
. . . . . . 7
mulGrp
mPoly mulGrp mPoly |
21 | | eqid 2622 |
. . . . . . 7
.gmulGrp mPoly
.gmulGrp mPoly |
22 | | eqid 2622 |
. . . . . . 7
mVar mVar |
23 | | simpll 790 |
. . . . . . 7
|
24 | | simpr 477 |
. . . . . . 7
|
25 | | eqidd 2623 |
. . . . . . . . . 10
mVar
mulGrp mPoly mVar mVar mulGrp
mPoly mVar |
26 | | 0ex 4790 |
. . . . . . . . . . 11
|
27 | | fveq2 6191 |
. . . . . . . . . . . . 13
mVar mVar |
28 | 27 | oveq1d 6665 |
. . . . . . . . . . . 12
mVar mulGrp
mPoly mVar mVar mulGrp mPoly
mVar |
29 | 27 | oveq2d 6666 |
. . . . . . . . . . . 12
mVar mulGrp mPoly mVar mVar mulGrp mPoly
mVar |
30 | 28, 29 | eqeq12d 2637 |
. . . . . . . . . . 11
mVar
mulGrp
mPoly mVar mVar mulGrp mPoly
mVar
mVar
mulGrp mPoly mVar mVar mulGrp
mPoly mVar |
31 | 26, 30 | ralsn 4222 |
. . . . . . . . . 10
mVar
mulGrp
mPoly mVar mVar mulGrp mPoly
mVar
mVar
mulGrp mPoly mVar mVar mulGrp
mPoly mVar |
32 | 25, 31 | sylibr 224 |
. . . . . . . . 9
mVar mulGrp
mPoly mVar mVar mulGrp mPoly
mVar |
33 | | fveq2 6191 |
. . . . . . . . . . . . 13
mVar mVar |
34 | 33 | oveq2d 6666 |
. . . . . . . . . . . 12
mVar mulGrp
mPoly mVar mVar
mulGrp
mPoly mVar |
35 | 33 | oveq1d 6665 |
. . . . . . . . . . . 12
mVar mulGrp
mPoly mVar mVar mulGrp
mPoly mVar |
36 | 34, 35 | eqeq12d 2637 |
. . . . . . . . . . 11
mVar
mulGrp
mPoly mVar mVar
mulGrp
mPoly mVar
mVar
mulGrp mPoly mVar mVar mulGrp
mPoly mVar |
37 | 36 | ralbidv 2986 |
. . . . . . . . . 10
mVar
mulGrp
mPoly mVar mVar
mulGrp
mPoly mVar
mVar mulGrp
mPoly mVar mVar mulGrp mPoly
mVar |
38 | 26, 37 | ralsn 4222 |
. . . . . . . . 9
mVar
mulGrp
mPoly mVar mVar
mulGrp
mPoly mVar
mVar mulGrp
mPoly mVar mVar mulGrp mPoly
mVar |
39 | 32, 38 | sylibr 224 |
. . . . . . . 8
mVar mulGrp
mPoly mVar mVar
mulGrp
mPoly mVar |
40 | | df1o2 7572 |
. . . . . . . . 9
|
41 | 40 | raleqi 3142 |
. . . . . . . . 9
mVar
mulGrp
mPoly mVar mVar
mulGrp
mPoly mVar
mVar mulGrp
mPoly mVar mVar
mulGrp
mPoly mVar |
42 | 40, 41 | raleqbii 2990 |
. . . . . . . 8
mVar mulGrp mPoly mVar mVar mulGrp mPoly mVar
mVar mulGrp mPoly mVar mVar mulGrp mPoly mVar |
43 | 39, 42 | sylibr 224 |
. . . . . . 7
mVar mulGrp mPoly mVar mVar mulGrp mPoly mVar |
44 | 1, 2, 3, 4, 19, 20, 21, 22, 23, 24, 43 | mplcoe5 19468 |
. . . . . 6
mulGrp
mPoly g .gmulGrp mPoly
mVar |
45 | | mpteq1 4737 |
. . . . . . . . 9
.gmulGrp mPoly mVar .gmulGrp mPoly
mVar |
46 | 40, 45 | ax-mp 5 |
. . . . . . . 8
.gmulGrp mPoly mVar .gmulGrp mPoly
mVar |
47 | 46 | oveq2i 6661 |
. . . . . . 7
mulGrp mPoly
g .gmulGrp mPoly
mVar mulGrp mPoly
g .gmulGrp mPoly mVar |
48 | 1 | mplring 19452 |
. . . . . . . . . . 11
mPoly
|
49 | 5, 48 | mpan 706 |
. . . . . . . . . 10
mPoly |
50 | 20 | ringmgp 18553 |
. . . . . . . . . 10
mPoly mulGrp mPoly |
51 | 49, 50 | syl 17 |
. . . . . . . . 9
mulGrp
mPoly |
52 | 51 | ad2antrr 762 |
. . . . . . . 8
mulGrp mPoly |
53 | 26 | a1i 11 |
. . . . . . . 8
|
54 | | ply1coe.e |
. . . . . . . . . . . 12
.g |
55 | 20, 10 | mgpbas 18495 |
. . . . . . . . . . . . 13
mulGrp mPoly
|
56 | 55 | a1i 11 |
. . . . . . . . . . . 12
mulGrp mPoly
|
57 | | ply1coe.m |
. . . . . . . . . . . . . 14
mulGrp |
58 | 57, 9 | mgpbas 18495 |
. . . . . . . . . . . . 13
|
59 | 58 | a1i 11 |
. . . . . . . . . . . 12
|
60 | | ssv 3625 |
. . . . . . . . . . . . 13
|
61 | 60 | a1i 11 |
. . . . . . . . . . . 12
|
62 | | ovexd 6680 |
. . . . . . . . . . . 12
mulGrp mPoly
|
63 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
64 | 7, 1, 63 | ply1mulr 19597 |
. . . . . . . . . . . . . . . 16
mPoly |
65 | 20, 64 | mgpplusg 18493 |
. . . . . . . . . . . . . . 15
mulGrp mPoly
|
66 | 57, 63 | mgpplusg 18493 |
. . . . . . . . . . . . . . 15
|
67 | 65, 66 | eqtr3i 2646 |
. . . . . . . . . . . . . 14
mulGrp mPoly |
68 | 67 | oveqi 6663 |
. . . . . . . . . . . . 13
mulGrp mPoly
|
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
mulGrp mPoly
|
70 | 21, 54, 56, 59, 61, 62, 69 | mulgpropd 17584 |
. . . . . . . . . . 11
.gmulGrp mPoly |
71 | 70 | oveqd 6667 |
. . . . . . . . . 10
.gmulGrp mPoly |
72 | 71 | adantr 481 |
. . . . . . . . 9
.gmulGrp mPoly |
73 | 7 | ply1ring 19618 |
. . . . . . . . . . . 12
|
74 | 57 | ringmgp 18553 |
. . . . . . . . . . . 12
|
75 | 73, 74 | syl 17 |
. . . . . . . . . . 11
|
76 | 75 | ad2antrr 762 |
. . . . . . . . . 10
|
77 | | elmapi 7879 |
. . . . . . . . . . . 12
|
78 | | 0lt1o 7584 |
. . . . . . . . . . . 12
|
79 | | ffvelrn 6357 |
. . . . . . . . . . . 12
|
80 | 77, 78, 79 | sylancl 694 |
. . . . . . . . . . 11
|
81 | 80 | adantl 482 |
. . . . . . . . . 10
|
82 | | ply1coe.x |
. . . . . . . . . . . 12
var1 |
83 | 82, 7, 9 | vr1cl 19587 |
. . . . . . . . . . 11
|
84 | 83 | ad2antrr 762 |
. . . . . . . . . 10
|
85 | 58, 54 | mulgnn0cl 17558 |
. . . . . . . . . 10
|
86 | 76, 81, 84, 85 | syl3anc 1326 |
. . . . . . . . 9
|
87 | 72, 86 | eqeltrd 2701 |
. . . . . . . 8
.gmulGrp mPoly |
88 | | fveq2 6191 |
. . . . . . . . . 10
|
89 | | fveq2 6191 |
. . . . . . . . . . 11
mVar mVar |
90 | 82 | vr1val 19562 |
. . . . . . . . . . 11
mVar |
91 | 89, 90 | syl6eqr 2674 |
. . . . . . . . . 10
mVar |
92 | 88, 91 | oveq12d 6668 |
. . . . . . . . 9
.gmulGrp mPoly mVar .gmulGrp mPoly |
93 | 55, 92 | gsumsn 18354 |
. . . . . . . 8
mulGrp mPoly .gmulGrp mPoly mulGrp
mPoly g .gmulGrp mPoly mVar .gmulGrp mPoly |
94 | 52, 53, 87, 93 | syl3anc 1326 |
. . . . . . 7
mulGrp mPoly
g .gmulGrp mPoly mVar .gmulGrp mPoly |
95 | 47, 94 | syl5eq 2668 |
. . . . . 6
mulGrp mPoly
g .gmulGrp mPoly
mVar .gmulGrp mPoly |
96 | 44, 95, 72 | 3eqtrd 2660 |
. . . . 5
|
97 | 18, 96 | oveq12d 6668 |
. . . 4
|
98 | 97 | mpteq2dva 4744 |
. . 3
|
99 | 98 | oveq2d 6666 |
. 2
mPoly
g
mPoly g |
100 | | nn0ex 11298 |
. . . . . 6
|
101 | 100 | mptex 6486 |
. . . . 5
|
102 | 101 | a1i 11 |
. . . 4
|
103 | | fvex 6201 |
. . . . . 6
Poly1 |
104 | 7, 103 | eqeltri 2697 |
. . . . 5
|
105 | 104 | a1i 11 |
. . . 4
|
106 | | ovexd 6680 |
. . . 4
mPoly |
107 | 9, 10 | eqtr3i 2646 |
. . . . 5
mPoly |
108 | 107 | a1i 11 |
. . . 4
mPoly |
109 | | eqid 2622 |
. . . . . 6
|
110 | 7, 1, 109 | ply1plusg 19595 |
. . . . 5
mPoly |
111 | 110 | a1i 11 |
. . . 4
mPoly |
112 | 102, 105,
106, 108, 111 | gsumpropd 17272 |
. . 3
g
mPoly g
|
113 | | eqid 2622 |
. . . . 5
|
114 | 1, 7, 113 | ply1mpl0 19625 |
. . . 4
mPoly |
115 | 1 | mpllmod 19451 |
. . . . . 6
mPoly
|
116 | 5, 13, 115 | sylancr 695 |
. . . . 5
mPoly |
117 | | lmodcmn 18911 |
. . . . 5
mPoly mPoly
CMnd |
118 | 116, 117 | syl 17 |
. . . 4
mPoly CMnd |
119 | 100 | a1i 11 |
. . . 4
|
120 | 7 | ply1lmod 19622 |
. . . . . . 7
|
121 | 120 | ad2antrr 762 |
. . . . . 6
|
122 | | eqid 2622 |
. . . . . . . . . 10
|
123 | 16, 9, 7, 122 | coe1f 19581 |
. . . . . . . . 9
|
124 | 123 | adantl 482 |
. . . . . . . 8
|
125 | 124 | ffvelrnda 6359 |
. . . . . . 7
|
126 | 7 | ply1sca 19623 |
. . . . . . . . . 10
Scalar |
127 | 126 | eqcomd 2628 |
. . . . . . . . 9
Scalar |
128 | 127 | ad2antrr 762 |
. . . . . . . 8
Scalar |
129 | 128 | fveq2d 6195 |
. . . . . . 7
Scalar |
130 | 125, 129 | eleqtrrd 2704 |
. . . . . 6
Scalar |
131 | 75 | ad2antrr 762 |
. . . . . . 7
|
132 | | simpr 477 |
. . . . . . 7
|
133 | 83 | ad2antrr 762 |
. . . . . . 7
|
134 | 58, 54 | mulgnn0cl 17558 |
. . . . . . 7
|
135 | 131, 132,
133, 134 | syl3anc 1326 |
. . . . . 6
|
136 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
137 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
138 | 9, 136, 11, 137 | lmodvscl 18880 |
. . . . . 6
Scalar |
139 | 121, 130,
135, 138 | syl3anc 1326 |
. . . . 5
|
140 | | eqid 2622 |
. . . . 5
|
141 | 139, 140 | fmptd 6385 |
. . . 4
|
142 | 7, 82, 9, 11, 57, 54, 16 | ply1coefsupp 19665 |
. . . 4
finSupp |
143 | | eqid 2622 |
. . . . . 6
|
144 | 40, 100, 26, 143 | mapsnf1o2 7905 |
. . . . 5
|
145 | 144 | a1i 11 |
. . . 4
|
146 | 10, 114, 118, 119, 141, 142, 145 | gsumf1o 18317 |
. . 3
mPoly
g mPoly g |
147 | | eqidd 2623 |
. . . . 5
|
148 | | eqidd 2623 |
. . . . 5
|
149 | | fveq2 6191 |
. . . . . 6
|
150 | | oveq1 6657 |
. . . . . 6
|
151 | 149, 150 | oveq12d 6668 |
. . . . 5
|
152 | 81, 147, 148, 151 | fmptco 6396 |
. . . 4
|
153 | 152 | oveq2d 6666 |
. . 3
mPoly
g
mPoly
g |
154 | 112, 146,
153 | 3eqtrrd 2661 |
. 2
mPoly
g g
|
155 | 15, 99, 154 | 3eqtrd 2660 |
1
g
|