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