Metamath Proof Explorer


Theorem evlslem2

Description: A linear function on the polynomial ring which is multiplicative on scaled monomials is generally multiplicative. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem2.p P = I mPoly R
evlslem2.b B = Base P
evlslem2.m · ˙ = S
evlslem2.z 0 ˙ = 0 R
evlslem2.d D = h 0 I | h -1 Fin
evlslem2.i φ I W
evlslem2.r φ R CRing
evlslem2.s φ S CRing
evlslem2.e1 φ E P GrpHom S
evlslem2.e2 φ x B y B j D i D E k D if k = j + f i x j R y i 0 ˙ = E k D if k = j x j 0 ˙ · ˙ E k D if k = i y i 0 ˙
Assertion evlslem2 φ x B y B E x P y = E x · ˙ E y

Proof

Step Hyp Ref Expression
1 evlslem2.p P = I mPoly R
2 evlslem2.b B = Base P
3 evlslem2.m · ˙ = S
4 evlslem2.z 0 ˙ = 0 R
5 evlslem2.d D = h 0 I | h -1 Fin
6 evlslem2.i φ I W
7 evlslem2.r φ R CRing
8 evlslem2.s φ S CRing
9 evlslem2.e1 φ E P GrpHom S
10 evlslem2.e2 φ x B y B j D i D E k D if k = j + f i x j R y i 0 ˙ = E k D if k = j x j 0 ˙ · ˙ E k D if k = i y i 0 ˙
11 eqid P = P
12 eqid 0 P = 0 P
13 ovex 0 I V
14 5 13 rabex2 D V
15 14 a1i φ x B y B D V
16 crngring R CRing R Ring
17 7 16 syl φ R Ring
18 1 6 17 mplringd φ P Ring
19 18 adantr φ x B y B P Ring
20 eqid Base R = Base R
21 6 ad2antrr φ x B y B j D I W
22 17 ad2antrr φ x B y B j D R Ring
23 simprl φ x B y B x B
24 1 20 2 5 23 mplelf φ x B y B x : D Base R
25 24 ffvelcdmda φ x B y B j D x j Base R
26 simpr φ x B y B j D j D
27 1 5 4 20 21 22 2 25 26 mplmon2cl φ x B y B j D k D if k = j x j 0 ˙ B
28 6 ad2antrr φ x B y B i D I W
29 17 ad2antrr φ x B y B i D R Ring
30 simprr φ x B y B y B
31 1 20 2 5 30 mplelf φ x B y B y : D Base R
32 31 ffvelcdmda φ x B y B i D y i Base R
33 simpr φ x B y B i D i D
34 1 5 4 20 28 29 2 32 33 mplmon2cl φ x B y B i D k D if k = i y i 0 ˙ B
35 14 mptex j D k D if k = j y j 0 ˙ V
36 funmpt Fun j D k D if k = j y j 0 ˙
37 fvex 0 P V
38 35 36 37 3pm3.2i j D k D if k = j y j 0 ˙ V Fun j D k D if k = j y j 0 ˙ 0 P V
39 38 a1i φ y B j D k D if k = j y j 0 ˙ V Fun j D k D if k = j y j 0 ˙ 0 P V
40 simpr φ y B y B
41 1 2 4 40 mplelsfi φ y B finSupp 0 ˙ y
42 41 fsuppimpd φ y B y supp 0 ˙ Fin
43 1 20 2 5 40 mplelf φ y B y : D Base R
44 ssidd φ y B y supp 0 ˙ y supp 0 ˙
45 14 a1i φ y B D V
46 4 fvexi 0 ˙ V
47 46 a1i φ y B 0 ˙ V
48 43 44 45 47 suppssr φ y B j D supp 0 ˙ y y j = 0 ˙
49 48 ifeq1d φ y B j D supp 0 ˙ y if k = j y j 0 ˙ = if k = j 0 ˙ 0 ˙
50 ifid if k = j 0 ˙ 0 ˙ = 0 ˙
51 49 50 eqtrdi φ y B j D supp 0 ˙ y if k = j y j 0 ˙ = 0 ˙
52 51 mpteq2dv φ y B j D supp 0 ˙ y k D if k = j y j 0 ˙ = k D 0 ˙
53 ringgrp R Ring R Grp
54 17 53 syl φ R Grp
55 1 5 4 12 6 54 mpl0 φ 0 P = D × 0 ˙
56 fconstmpt D × 0 ˙ = k D 0 ˙
57 55 56 eqtrdi φ 0 P = k D 0 ˙
58 57 ad2antrr φ y B j D supp 0 ˙ y 0 P = k D 0 ˙
59 52 58 eqtr4d φ y B j D supp 0 ˙ y k D if k = j y j 0 ˙ = 0 P
60 59 45 suppss2 φ y B j D k D if k = j y j 0 ˙ supp 0 P y supp 0 ˙
61 suppssfifsupp j D k D if k = j y j 0 ˙ V Fun j D k D if k = j y j 0 ˙ 0 P V y supp 0 ˙ Fin j D k D if k = j y j 0 ˙ supp 0 P y supp 0 ˙ finSupp 0 P j D k D if k = j y j 0 ˙
62 39 42 60 61 syl12anc φ y B finSupp 0 P j D k D if k = j y j 0 ˙
63 62 ralrimiva φ y B finSupp 0 P j D k D if k = j y j 0 ˙
64 fveq1 y = x y j = x j
65 64 ifeq1d y = x if k = j y j 0 ˙ = if k = j x j 0 ˙
66 65 mpteq2dv y = x k D if k = j y j 0 ˙ = k D if k = j x j 0 ˙
67 66 mpteq2dv y = x j D k D if k = j y j 0 ˙ = j D k D if k = j x j 0 ˙
68 67 breq1d y = x finSupp 0 P j D k D if k = j y j 0 ˙ finSupp 0 P j D k D if k = j x j 0 ˙
69 68 cbvralvw y B finSupp 0 P j D k D if k = j y j 0 ˙ x B finSupp 0 P j D k D if k = j x j 0 ˙
70 63 69 sylib φ x B finSupp 0 P j D k D if k = j x j 0 ˙
71 70 r19.21bi φ x B finSupp 0 P j D k D if k = j x j 0 ˙
72 71 adantrr φ x B y B finSupp 0 P j D k D if k = j x j 0 ˙
73 equequ2 i = j k = i k = j
74 fveq2 i = j y i = y j
75 73 74 ifbieq1d i = j if k = i y i 0 ˙ = if k = j y j 0 ˙
76 75 mpteq2dv i = j k D if k = i y i 0 ˙ = k D if k = j y j 0 ˙
77 76 cbvmptv i D k D if k = i y i 0 ˙ = j D k D if k = j y j 0 ˙
78 62 adantrl φ x B y B finSupp 0 P j D k D if k = j y j 0 ˙
79 77 78 eqbrtrid φ x B y B finSupp 0 P i D k D if k = i y i 0 ˙
80 2 11 12 15 15 19 27 34 72 79 gsumdixp φ x B y B P j D k D if k = j x j 0 ˙ P P i D k D if k = i y i 0 ˙ = P j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
81 80 fveq2d φ x B y B E P j D k D if k = j x j 0 ˙ P P i D k D if k = i y i 0 ˙ = E P j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
82 ringcmn P Ring P CMnd
83 18 82 syl φ P CMnd
84 83 adantr φ x B y B P CMnd
85 crngring S CRing S Ring
86 8 85 syl φ S Ring
87 86 adantr φ x B y B S Ring
88 ringmnd S Ring S Mnd
89 87 88 syl φ x B y B S Mnd
90 14 14 xpex D × D V
91 90 a1i φ x B y B D × D V
92 ghmmhm E P GrpHom S E P MndHom S
93 9 92 syl φ E P MndHom S
94 93 adantr φ x B y B E P MndHom S
95 18 ad2antrr φ x B y B j D i D P Ring
96 27 adantrr φ x B y B j D i D k D if k = j x j 0 ˙ B
97 34 adantrl φ x B y B j D i D k D if k = i y i 0 ˙ B
98 2 11 ringcl P Ring k D if k = j x j 0 ˙ B k D if k = i y i 0 ˙ B k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ B
99 95 96 97 98 syl3anc φ x B y B j D i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ B
100 99 ralrimivva φ x B y B j D i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ B
101 eqid j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
102 101 fmpo j D i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ B j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ : D × D B
103 100 102 sylib φ x B y B j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ : D × D B
104 14 14 mpoex j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ V
105 101 mpofun Fun j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
106 104 105 37 3pm3.2i j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ V Fun j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ 0 P V
107 106 a1i φ x B y B j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ V Fun j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ 0 P V
108 72 fsuppimpd φ x B y B j D k D if k = j x j 0 ˙ supp 0 P Fin
109 79 fsuppimpd φ x B y B i D k D if k = i y i 0 ˙ supp 0 P Fin
110 xpfi j D k D if k = j x j 0 ˙ supp 0 P Fin i D k D if k = i y i 0 ˙ supp 0 P Fin supp 0 P j D k D if k = j x j 0 ˙ × supp 0 P i D k D if k = i y i 0 ˙ Fin
111 108 109 110 syl2anc φ x B y B supp 0 P j D k D if k = j x j 0 ˙ × supp 0 P i D k D if k = i y i 0 ˙ Fin
112 2 12 11 19 27 34 15 15 evlslem4 φ x B y B j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ supp 0 P supp 0 P j D k D if k = j x j 0 ˙ × supp 0 P i D k D if k = i y i 0 ˙
113 suppssfifsupp j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ V Fun j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ 0 P V supp 0 P j D k D if k = j x j 0 ˙ × supp 0 P i D k D if k = i y i 0 ˙ Fin j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ supp 0 P supp 0 P j D k D if k = j x j 0 ˙ × supp 0 P i D k D if k = i y i 0 ˙ finSupp 0 P j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
114 107 111 112 113 syl12anc φ x B y B finSupp 0 P j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
115 2 12 84 89 91 94 103 114 gsummhm φ x B y B S E j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = E P j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
116 6 ad2antrr φ x B y B j D i D I W
117 7 ad2antrr φ x B y B j D i D R CRing
118 eqid R = R
119 simprl φ x B y B j D i D j D
120 simprr φ x B y B j D i D i D
121 25 adantrr φ x B y B j D i D x j Base R
122 32 adantrl φ x B y B j D i D y i Base R
123 1 5 4 20 116 117 11 118 119 120 121 122 mplmon2mul φ x B y B j D i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = k D if k = j + f i x j R y i 0 ˙
124 123 fveq2d φ x B y B j D i D E k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = E k D if k = j + f i x j R y i 0 ˙
125 10 anassrs φ x B y B j D i D E k D if k = j + f i x j R y i 0 ˙ = E k D if k = j x j 0 ˙ · ˙ E k D if k = i y i 0 ˙
126 124 125 eqtrd φ x B y B j D i D E k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = E k D if k = j x j 0 ˙ · ˙ E k D if k = i y i 0 ˙
127 126 3impb φ x B y B j D i D E k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = E k D if k = j x j 0 ˙ · ˙ E k D if k = i y i 0 ˙
128 127 mpoeq3dva φ x B y B j D , i D E k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = j D , i D E k D if k = j x j 0 ˙ · ˙ E k D if k = i y i 0 ˙
129 128 oveq2d φ x B y B S j D , i D E k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = S j D , i D E k D if k = j x j 0 ˙ · ˙ E k D if k = i y i 0 ˙
130 eqidd φ x B y B j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
131 eqid Base S = Base S
132 2 131 ghmf E P GrpHom S E : B Base S
133 9 132 syl φ E : B Base S
134 133 feqmptd φ E = z B E z
135 134 adantr φ x B y B E = z B E z
136 fveq2 z = k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ E z = E k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
137 99 130 135 136 fmpoco φ x B y B E j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = j D , i D E k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
138 137 oveq2d φ x B y B S E j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = S j D , i D E k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙
139 eqidd φ x B y B j D k D if k = j x j 0 ˙ = j D k D if k = j x j 0 ˙
140 fveq2 z = k D if k = j x j 0 ˙ E z = E k D if k = j x j 0 ˙
141 27 139 135 140 fmptco φ x B y B E j D k D if k = j x j 0 ˙ = j D E k D if k = j x j 0 ˙
142 141 oveq2d φ x B y B S E j D k D if k = j x j 0 ˙ = S j D E k D if k = j x j 0 ˙
143 eqidd φ x B y B i D k D if k = i y i 0 ˙ = i D k D if k = i y i 0 ˙
144 fveq2 z = k D if k = i y i 0 ˙ E z = E k D if k = i y i 0 ˙
145 34 143 135 144 fmptco φ x B y B E i D k D if k = i y i 0 ˙ = i D E k D if k = i y i 0 ˙
146 145 oveq2d φ x B y B S E i D k D if k = i y i 0 ˙ = S i D E k D if k = i y i 0 ˙
147 142 146 oveq12d φ x B y B S E j D k D if k = j x j 0 ˙ · ˙ S E i D k D if k = i y i 0 ˙ = S j D E k D if k = j x j 0 ˙ · ˙ S i D E k D if k = i y i 0 ˙
148 eqid 0 S = 0 S
149 133 ad2antrr φ x B y B j D E : B Base S
150 149 27 ffvelcdmd φ x B y B j D E k D if k = j x j 0 ˙ Base S
151 133 ad2antrr φ x B y B i D E : B Base S
152 151 34 ffvelcdmd φ x B y B i D E k D if k = i y i 0 ˙ Base S
153 14 mptex j D E k D if k = j x j 0 ˙ V
154 funmpt Fun j D E k D if k = j x j 0 ˙
155 fvex 0 S V
156 153 154 155 3pm3.2i j D E k D if k = j x j 0 ˙ V Fun j D E k D if k = j x j 0 ˙ 0 S V
157 156 a1i φ x B y B j D E k D if k = j x j 0 ˙ V Fun j D E k D if k = j x j 0 ˙ 0 S V
158 ssidd φ j D k D if k = j x j 0 ˙ supp 0 P j D k D if k = j x j 0 ˙ supp 0 P
159 12 148 ghmid E P GrpHom S E 0 P = 0 S
160 9 159 syl φ E 0 P = 0 S
161 14 mptex k D if k = j x j 0 ˙ V
162 161 a1i φ j D k D if k = j x j 0 ˙ V
163 37 a1i φ 0 P V
164 158 160 162 163 suppssfv φ j D E k D if k = j x j 0 ˙ supp 0 S j D k D if k = j x j 0 ˙ supp 0 P
165 164 adantr φ x B y B j D E k D if k = j x j 0 ˙ supp 0 S j D k D if k = j x j 0 ˙ supp 0 P
166 suppssfifsupp j D E k D if k = j x j 0 ˙ V Fun j D E k D if k = j x j 0 ˙ 0 S V j D k D if k = j x j 0 ˙ supp 0 P Fin j D E k D if k = j x j 0 ˙ supp 0 S j D k D if k = j x j 0 ˙ supp 0 P finSupp 0 S j D E k D if k = j x j 0 ˙
167 157 108 165 166 syl12anc φ x B y B finSupp 0 S j D E k D if k = j x j 0 ˙
168 14 mptex i D E k D if k = i y i 0 ˙ V
169 funmpt Fun i D E k D if k = i y i 0 ˙
170 168 169 155 3pm3.2i i D E k D if k = i y i 0 ˙ V Fun i D E k D if k = i y i 0 ˙ 0 S V
171 170 a1i φ x B y B i D E k D if k = i y i 0 ˙ V Fun i D E k D if k = i y i 0 ˙ 0 S V
172 ssidd φ i D k D if k = i y i 0 ˙ supp 0 P i D k D if k = i y i 0 ˙ supp 0 P
173 14 mptex k D if k = i y i 0 ˙ V
174 173 a1i φ i D k D if k = i y i 0 ˙ V
175 172 160 174 163 suppssfv φ i D E k D if k = i y i 0 ˙ supp 0 S i D k D if k = i y i 0 ˙ supp 0 P
176 175 adantr φ x B y B i D E k D if k = i y i 0 ˙ supp 0 S i D k D if k = i y i 0 ˙ supp 0 P
177 suppssfifsupp i D E k D if k = i y i 0 ˙ V Fun i D E k D if k = i y i 0 ˙ 0 S V i D k D if k = i y i 0 ˙ supp 0 P Fin i D E k D if k = i y i 0 ˙ supp 0 S i D k D if k = i y i 0 ˙ supp 0 P finSupp 0 S i D E k D if k = i y i 0 ˙
178 171 109 176 177 syl12anc φ x B y B finSupp 0 S i D E k D if k = i y i 0 ˙
179 131 3 148 15 15 87 150 152 167 178 gsumdixp φ x B y B S j D E k D if k = j x j 0 ˙ · ˙ S i D E k D if k = i y i 0 ˙ = S j D , i D E k D if k = j x j 0 ˙ · ˙ E k D if k = i y i 0 ˙
180 147 179 eqtrd φ x B y B S E j D k D if k = j x j 0 ˙ · ˙ S E i D k D if k = i y i 0 ˙ = S j D , i D E k D if k = j x j 0 ˙ · ˙ E k D if k = i y i 0 ˙
181 129 138 180 3eqtr4d φ x B y B S E j D , i D k D if k = j x j 0 ˙ P k D if k = i y i 0 ˙ = S E j D k D if k = j x j 0 ˙ · ˙ S E i D k D if k = i y i 0 ˙
182 81 115 181 3eqtr2d φ x B y B E P j D k D if k = j x j 0 ˙ P P i D k D if k = i y i 0 ˙ = S E j D k D if k = j x j 0 ˙ · ˙ S E i D k D if k = i y i 0 ˙
183 6 adantr φ x B y B I W
184 17 adantr φ x B y B R Ring
185 1 5 4 2 183 184 23 mplcoe4 φ x B y B x = P j D k D if k = j x j 0 ˙
186 1 5 4 2 183 184 30 mplcoe4 φ x B y B y = P i D k D if k = i y i 0 ˙
187 185 186 oveq12d φ x B y B x P y = P j D k D if k = j x j 0 ˙ P P i D k D if k = i y i 0 ˙
188 187 fveq2d φ x B y B E x P y = E P j D k D if k = j x j 0 ˙ P P i D k D if k = i y i 0 ˙
189 185 fveq2d φ x B y B E x = E P j D k D if k = j x j 0 ˙
190 27 fmpttd φ x B y B j D k D if k = j x j 0 ˙ : D B
191 2 12 84 89 15 94 190 72 gsummhm φ x B y B S E j D k D if k = j x j 0 ˙ = E P j D k D if k = j x j 0 ˙
192 189 191 eqtr4d φ x B y B E x = S E j D k D if k = j x j 0 ˙
193 186 fveq2d φ x B y B E y = E P i D k D if k = i y i 0 ˙
194 34 fmpttd φ x B y B i D k D if k = i y i 0 ˙ : D B
195 2 12 84 89 15 94 194 79 gsummhm φ x B y B S E i D k D if k = i y i 0 ˙ = E P i D k D if k = i y i 0 ˙
196 193 195 eqtr4d φ x B y B E y = S E i D k D if k = i y i 0 ˙
197 192 196 oveq12d φ x B y B E x · ˙ E y = S E j D k D if k = j x j 0 ˙ · ˙ S E i D k D if k = i y i 0 ˙
198 182 188 197 3eqtr4d φ x B y B E x P y = E x · ˙ E y