Metamath Proof Explorer


Theorem evlslem3

Description: Lemma for evlseu . Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem3.p P = I mPoly R
evlslem3.b B = Base P
evlslem3.c C = Base S
evlslem3.k K = Base R
evlslem3.d D = h 0 I | h -1 Fin
evlslem3.t T = mulGrp S
evlslem3.x × ˙ = T
evlslem3.m · ˙ = S
evlslem3.v V = I mVar R
evlslem3.e E = p B S b D F p b · ˙ T b × ˙ f G
evlslem3.i φ I W
evlslem3.r φ R CRing
evlslem3.s φ S CRing
evlslem3.f φ F R RingHom S
evlslem3.g φ G : I C
evlslem3.z 0 ˙ = 0 R
evlslem3.a φ A D
evlslem3.q φ H K
Assertion evlslem3 φ E x D if x = A H 0 ˙ = F H · ˙ T A × ˙ f G

Proof

Step Hyp Ref Expression
1 evlslem3.p P = I mPoly R
2 evlslem3.b B = Base P
3 evlslem3.c C = Base S
4 evlslem3.k K = Base R
5 evlslem3.d D = h 0 I | h -1 Fin
6 evlslem3.t T = mulGrp S
7 evlslem3.x × ˙ = T
8 evlslem3.m · ˙ = S
9 evlslem3.v V = I mVar R
10 evlslem3.e E = p B S b D F p b · ˙ T b × ˙ f G
11 evlslem3.i φ I W
12 evlslem3.r φ R CRing
13 evlslem3.s φ S CRing
14 evlslem3.f φ F R RingHom S
15 evlslem3.g φ G : I C
16 evlslem3.z 0 ˙ = 0 R
17 evlslem3.a φ A D
18 evlslem3.q φ H K
19 crngring R CRing R Ring
20 12 19 syl φ R Ring
21 1 5 16 4 11 20 2 18 17 mplmon2cl φ x D if x = A H 0 ˙ B
22 fveq1 p = x D if x = A H 0 ˙ p b = x D if x = A H 0 ˙ b
23 22 fveq2d p = x D if x = A H 0 ˙ F p b = F x D if x = A H 0 ˙ b
24 23 oveq1d p = x D if x = A H 0 ˙ F p b · ˙ T b × ˙ f G = F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G
25 24 mpteq2dv p = x D if x = A H 0 ˙ b D F p b · ˙ T b × ˙ f G = b D F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G
26 25 oveq2d p = x D if x = A H 0 ˙ S b D F p b · ˙ T b × ˙ f G = S b D F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G
27 ovex S b D F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G V
28 26 10 27 fvmpt x D if x = A H 0 ˙ B E x D if x = A H 0 ˙ = S b D F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G
29 21 28 syl φ E x D if x = A H 0 ˙ = S b D F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G
30 eqid x D if x = A H 0 ˙ = x D if x = A H 0 ˙
31 eqeq1 x = b x = A b = A
32 31 ifbid x = b if x = A H 0 ˙ = if b = A H 0 ˙
33 simpr φ b D b D
34 16 fvexi 0 ˙ V
35 34 a1i φ 0 ˙ V
36 18 35 ifexd φ if b = A H 0 ˙ V
37 36 adantr φ b D if b = A H 0 ˙ V
38 30 32 33 37 fvmptd3 φ b D x D if x = A H 0 ˙ b = if b = A H 0 ˙
39 38 fveq2d φ b D F x D if x = A H 0 ˙ b = F if b = A H 0 ˙
40 39 oveq1d φ b D F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G = F if b = A H 0 ˙ · ˙ T b × ˙ f G
41 40 mpteq2dva φ b D F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G = b D F if b = A H 0 ˙ · ˙ T b × ˙ f G
42 41 oveq2d φ S b D F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G = S b D F if b = A H 0 ˙ · ˙ T b × ˙ f G
43 eqid 0 S = 0 S
44 crngring S CRing S Ring
45 13 44 syl φ S Ring
46 ringmnd S Ring S Mnd
47 45 46 syl φ S Mnd
48 ovex 0 I V
49 5 48 rabex2 D V
50 49 a1i φ D V
51 45 adantr φ b D S Ring
52 4 3 rhmf F R RingHom S F : K C
53 14 52 syl φ F : K C
54 4 16 ring0cl R Ring 0 ˙ K
55 20 54 syl φ 0 ˙ K
56 18 55 ifcld φ if b = A H 0 ˙ K
57 53 56 ffvelcdmd φ F if b = A H 0 ˙ C
58 57 adantr φ b D F if b = A H 0 ˙ C
59 6 3 mgpbas C = Base T
60 eqid 0 T = 0 T
61 6 crngmgp S CRing T CMnd
62 13 61 syl φ T CMnd
63 62 adantr φ b D T CMnd
64 11 adantr φ b D I W
65 cmnmnd T CMnd T Mnd
66 62 65 syl φ T Mnd
67 66 ad2antrr φ b D y 0 z C T Mnd
68 simprl φ b D y 0 z C y 0
69 simprr φ b D y 0 z C z C
70 59 7 67 68 69 mulgnn0cld φ b D y 0 z C y × ˙ z C
71 5 psrbagf b D b : I 0
72 71 adantl φ b D b : I 0
73 15 adantr φ b D G : I C
74 inidm I I = I
75 70 72 73 64 64 74 off φ b D b × ˙ f G : I C
76 ovex b × ˙ f G V
77 76 a1i φ b D b × ˙ f G V
78 75 ffund φ b D Fun b × ˙ f G
79 fvexd φ b D 0 T V
80 5 psrbag I W b D b : I 0 b -1 Fin
81 11 80 syl φ b D b : I 0 b -1 Fin
82 81 simplbda φ b D b -1 Fin
83 72 ffnd φ b D b Fn I
84 83 adantr φ b D y I b -1 b Fn I
85 15 ffnd φ G Fn I
86 85 ad2antrr φ b D y I b -1 G Fn I
87 11 ad2antrr φ b D y I b -1 I W
88 eldifi y I b -1 y I
89 88 adantl φ b D y I b -1 y I
90 fnfvof b Fn I G Fn I I W y I b × ˙ f G y = b y × ˙ G y
91 84 86 87 89 90 syl22anc φ b D y I b -1 b × ˙ f G y = b y × ˙ G y
92 ffvelcdm b : I 0 y I b y 0
93 72 88 92 syl2an φ b D y I b -1 b y 0
94 elnn0 b y 0 b y b y = 0
95 93 94 sylib φ b D y I b -1 b y b y = 0
96 eldifn y I b -1 ¬ y b -1
97 96 adantl φ b D y I b -1 ¬ y b -1
98 83 ad2antrr φ b D y I b -1 b y b Fn I
99 88 ad2antlr φ b D y I b -1 b y y I
100 simpr φ b D y I b -1 b y b y
101 98 99 100 elpreimad φ b D y I b -1 b y y b -1
102 97 101 mtand φ b D y I b -1 ¬ b y
103 95 102 orcnd φ b D y I b -1 b y = 0
104 103 oveq1d φ b D y I b -1 b y × ˙ G y = 0 × ˙ G y
105 ffvelcdm G : I C y I G y C
106 73 88 105 syl2an φ b D y I b -1 G y C
107 59 60 7 mulg0 G y C 0 × ˙ G y = 0 T
108 106 107 syl φ b D y I b -1 0 × ˙ G y = 0 T
109 91 104 108 3eqtrd φ b D y I b -1 b × ˙ f G y = 0 T
110 75 109 suppss φ b D b × ˙ f G supp 0 T b -1
111 suppssfifsupp b × ˙ f G V Fun b × ˙ f G 0 T V b -1 Fin b × ˙ f G supp 0 T b -1 finSupp 0 T b × ˙ f G
112 77 78 79 82 110 111 syl32anc φ b D finSupp 0 T b × ˙ f G
113 59 60 63 64 75 112 gsumcl φ b D T b × ˙ f G C
114 3 8 ringcl S Ring F if b = A H 0 ˙ C T b × ˙ f G C F if b = A H 0 ˙ · ˙ T b × ˙ f G C
115 51 58 113 114 syl3anc φ b D F if b = A H 0 ˙ · ˙ T b × ˙ f G C
116 115 fmpttd φ b D F if b = A H 0 ˙ · ˙ T b × ˙ f G : D C
117 eldifsnneq b D A ¬ b = A
118 117 iffalsed b D A if b = A H 0 ˙ = 0 ˙
119 118 adantl φ b D A if b = A H 0 ˙ = 0 ˙
120 119 fveq2d φ b D A F if b = A H 0 ˙ = F 0 ˙
121 rhmghm F R RingHom S F R GrpHom S
122 14 121 syl φ F R GrpHom S
123 16 43 ghmid F R GrpHom S F 0 ˙ = 0 S
124 122 123 syl φ F 0 ˙ = 0 S
125 124 adantr φ b D A F 0 ˙ = 0 S
126 120 125 eqtrd φ b D A F if b = A H 0 ˙ = 0 S
127 126 oveq1d φ b D A F if b = A H 0 ˙ · ˙ T b × ˙ f G = 0 S · ˙ T b × ˙ f G
128 45 adantr φ b D A S Ring
129 eldifi b D A b D
130 129 113 sylan2 φ b D A T b × ˙ f G C
131 3 8 43 ringlz S Ring T b × ˙ f G C 0 S · ˙ T b × ˙ f G = 0 S
132 128 130 131 syl2anc φ b D A 0 S · ˙ T b × ˙ f G = 0 S
133 127 132 eqtrd φ b D A F if b = A H 0 ˙ · ˙ T b × ˙ f G = 0 S
134 133 50 suppss2 φ b D F if b = A H 0 ˙ · ˙ T b × ˙ f G supp 0 S A
135 3 43 47 50 17 116 134 gsumpt φ S b D F if b = A H 0 ˙ · ˙ T b × ˙ f G = b D F if b = A H 0 ˙ · ˙ T b × ˙ f G A
136 42 135 eqtrd φ S b D F x D if x = A H 0 ˙ b · ˙ T b × ˙ f G = b D F if b = A H 0 ˙ · ˙ T b × ˙ f G A
137 iftrue b = A if b = A H 0 ˙ = H
138 137 fveq2d b = A F if b = A H 0 ˙ = F H
139 oveq1 b = A b × ˙ f G = A × ˙ f G
140 139 oveq2d b = A T b × ˙ f G = T A × ˙ f G
141 138 140 oveq12d b = A F if b = A H 0 ˙ · ˙ T b × ˙ f G = F H · ˙ T A × ˙ f G
142 eqid b D F if b = A H 0 ˙ · ˙ T b × ˙ f G = b D F if b = A H 0 ˙ · ˙ T b × ˙ f G
143 ovex F H · ˙ T A × ˙ f G V
144 141 142 143 fvmpt A D b D F if b = A H 0 ˙ · ˙ T b × ˙ f G A = F H · ˙ T A × ˙ f G
145 17 144 syl φ b D F if b = A H 0 ˙ · ˙ T b × ˙ f G A = F H · ˙ T A × ˙ f G
146 29 136 145 3eqtrd φ E x D if x = A H 0 ˙ = F H · ˙ T A × ˙ f G