Metamath Proof Explorer


Theorem mpfind

Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses mpfind.cb B = Base S
mpfind.cp + ˙ = + S
mpfind.ct · ˙ = S
mpfind.cq Q = ran I evalSub S R
mpfind.ad φ f Q τ g Q η ζ
mpfind.mu φ f Q τ g Q η σ
mpfind.wa x = B I × f ψ χ
mpfind.wb x = g B I g f ψ θ
mpfind.wc x = f ψ τ
mpfind.wd x = g ψ η
mpfind.we x = f + ˙ f g ψ ζ
mpfind.wf x = f · ˙ f g ψ σ
mpfind.wg x = A ψ ρ
mpfind.co φ f R χ
mpfind.pr φ f I θ
mpfind.a φ A Q
Assertion mpfind φ ρ

Proof

Step Hyp Ref Expression
1 mpfind.cb B = Base S
2 mpfind.cp + ˙ = + S
3 mpfind.ct · ˙ = S
4 mpfind.cq Q = ran I evalSub S R
5 mpfind.ad φ f Q τ g Q η ζ
6 mpfind.mu φ f Q τ g Q η σ
7 mpfind.wa x = B I × f ψ χ
8 mpfind.wb x = g B I g f ψ θ
9 mpfind.wc x = f ψ τ
10 mpfind.wd x = g ψ η
11 mpfind.we x = f + ˙ f g ψ ζ
12 mpfind.wf x = f · ˙ f g ψ σ
13 mpfind.wg x = A ψ ρ
14 mpfind.co φ f R χ
15 mpfind.pr φ f I θ
16 mpfind.a φ A Q
17 16 4 eleqtrdi φ A ran I evalSub S R
18 4 mpfrcl A Q I V S CRing R SubRing S
19 16 18 syl φ I V S CRing R SubRing S
20 eqid I evalSub S R = I evalSub S R
21 eqid I mPoly S 𝑠 R = I mPoly S 𝑠 R
22 eqid S 𝑠 R = S 𝑠 R
23 eqid S 𝑠 B I = S 𝑠 B I
24 20 21 22 23 1 evlsrhm I V S CRing R SubRing S I evalSub S R I mPoly S 𝑠 R RingHom S 𝑠 B I
25 eqid Base I mPoly S 𝑠 R = Base I mPoly S 𝑠 R
26 eqid Base S 𝑠 B I = Base S 𝑠 B I
27 25 26 rhmf I evalSub S R I mPoly S 𝑠 R RingHom S 𝑠 B I I evalSub S R : Base I mPoly S 𝑠 R Base S 𝑠 B I
28 19 24 27 3syl φ I evalSub S R : Base I mPoly S 𝑠 R Base S 𝑠 B I
29 28 ffnd φ I evalSub S R Fn Base I mPoly S 𝑠 R
30 fvelrnb I evalSub S R Fn Base I mPoly S 𝑠 R A ran I evalSub S R y Base I mPoly S 𝑠 R I evalSub S R y = A
31 29 30 syl φ A ran I evalSub S R y Base I mPoly S 𝑠 R I evalSub S R y = A
32 17 31 mpbid φ y Base I mPoly S 𝑠 R I evalSub S R y = A
33 28 ffund φ Fun I evalSub S R
34 eqid Base S 𝑠 R = Base S 𝑠 R
35 eqid I mVar S 𝑠 R = I mVar S 𝑠 R
36 eqid + I mPoly S 𝑠 R = + I mPoly S 𝑠 R
37 eqid I mPoly S 𝑠 R = I mPoly S 𝑠 R
38 eqid algSc I mPoly S 𝑠 R = algSc I mPoly S 𝑠 R
39 19 simp1d φ I V
40 19 simp2d φ S CRing
41 19 simp3d φ R SubRing S
42 22 subrgcrng S CRing R SubRing S S 𝑠 R CRing
43 40 41 42 syl2anc φ S 𝑠 R CRing
44 crngring S 𝑠 R CRing S 𝑠 R Ring
45 43 44 syl φ S 𝑠 R Ring
46 21 mplring I V S 𝑠 R Ring I mPoly S 𝑠 R Ring
47 39 45 46 syl2anc φ I mPoly S 𝑠 R Ring
48 47 adantr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I mPoly S 𝑠 R Ring
49 simprl φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i I evalSub S R -1 x | ψ
50 elpreima I evalSub S R Fn Base I mPoly S 𝑠 R i I evalSub S R -1 x | ψ i Base I mPoly S 𝑠 R I evalSub S R i x | ψ
51 29 50 syl φ i I evalSub S R -1 x | ψ i Base I mPoly S 𝑠 R I evalSub S R i x | ψ
52 51 adantr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i I evalSub S R -1 x | ψ i Base I mPoly S 𝑠 R I evalSub S R i x | ψ
53 49 52 mpbid φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i Base I mPoly S 𝑠 R I evalSub S R i x | ψ
54 53 simpld φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i Base I mPoly S 𝑠 R
55 simprr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ
56 elpreima I evalSub S R Fn Base I mPoly S 𝑠 R j I evalSub S R -1 x | ψ j Base I mPoly S 𝑠 R I evalSub S R j x | ψ
57 29 56 syl φ j I evalSub S R -1 x | ψ j Base I mPoly S 𝑠 R I evalSub S R j x | ψ
58 57 adantr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ j Base I mPoly S 𝑠 R I evalSub S R j x | ψ
59 55 58 mpbid φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ j Base I mPoly S 𝑠 R I evalSub S R j x | ψ
60 59 simpld φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ j Base I mPoly S 𝑠 R
61 25 36 ringacl I mPoly S 𝑠 R Ring i Base I mPoly S 𝑠 R j Base I mPoly S 𝑠 R i + I mPoly S 𝑠 R j Base I mPoly S 𝑠 R
62 48 54 60 61 syl3anc φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i + I mPoly S 𝑠 R j Base I mPoly S 𝑠 R
63 rhmghm I evalSub S R I mPoly S 𝑠 R RingHom S 𝑠 B I I evalSub S R I mPoly S 𝑠 R GrpHom S 𝑠 B I
64 19 24 63 3syl φ I evalSub S R I mPoly S 𝑠 R GrpHom S 𝑠 B I
65 64 adantr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R I mPoly S 𝑠 R GrpHom S 𝑠 B I
66 eqid + S 𝑠 B I = + S 𝑠 B I
67 25 36 66 ghmlin I evalSub S R I mPoly S 𝑠 R GrpHom S 𝑠 B I i Base I mPoly S 𝑠 R j Base I mPoly S 𝑠 R I evalSub S R i + I mPoly S 𝑠 R j = I evalSub S R i + S 𝑠 B I I evalSub S R j
68 65 54 60 67 syl3anc φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i + I mPoly S 𝑠 R j = I evalSub S R i + S 𝑠 B I I evalSub S R j
69 40 adantr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ S CRing
70 ovexd φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ B I V
71 28 adantr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R : Base I mPoly S 𝑠 R Base S 𝑠 B I
72 71 54 ffvelrnd φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i Base S 𝑠 B I
73 71 60 ffvelrnd φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R j Base S 𝑠 B I
74 23 26 69 70 72 73 2 66 pwsplusgval φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i + S 𝑠 B I I evalSub S R j = I evalSub S R i + ˙ f I evalSub S R j
75 68 74 eqtrd φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i + I mPoly S 𝑠 R j = I evalSub S R i + ˙ f I evalSub S R j
76 simpl φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ φ
77 fnfvelrn I evalSub S R Fn Base I mPoly S 𝑠 R i Base I mPoly S 𝑠 R I evalSub S R i ran I evalSub S R
78 29 54 77 syl2an2r φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i ran I evalSub S R
79 78 4 eleqtrrdi φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i Q
80 fvimacnvi Fun I evalSub S R i I evalSub S R -1 x | ψ I evalSub S R i x | ψ
81 33 49 80 syl2an2r φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i x | ψ
82 79 81 jca φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i Q I evalSub S R i x | ψ
83 fnfvelrn I evalSub S R Fn Base I mPoly S 𝑠 R j Base I mPoly S 𝑠 R I evalSub S R j ran I evalSub S R
84 29 60 83 syl2an2r φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R j ran I evalSub S R
85 84 4 eleqtrrdi φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R j Q
86 fvimacnvi Fun I evalSub S R j I evalSub S R -1 x | ψ I evalSub S R j x | ψ
87 33 55 86 syl2an2r φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R j x | ψ
88 85 87 jca φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R j Q I evalSub S R j x | ψ
89 fvex I evalSub S R i V
90 fvex I evalSub S R j V
91 eleq1 f = I evalSub S R i f Q I evalSub S R i Q
92 vex f V
93 92 9 elab f x | ψ τ
94 eleq1 f = I evalSub S R i f x | ψ I evalSub S R i x | ψ
95 93 94 bitr3id f = I evalSub S R i τ I evalSub S R i x | ψ
96 91 95 anbi12d f = I evalSub S R i f Q τ I evalSub S R i Q I evalSub S R i x | ψ
97 eleq1 g = I evalSub S R j g Q I evalSub S R j Q
98 vex g V
99 98 10 elab g x | ψ η
100 eleq1 g = I evalSub S R j g x | ψ I evalSub S R j x | ψ
101 99 100 bitr3id g = I evalSub S R j η I evalSub S R j x | ψ
102 97 101 anbi12d g = I evalSub S R j g Q η I evalSub S R j Q I evalSub S R j x | ψ
103 96 102 bi2anan9 f = I evalSub S R i g = I evalSub S R j f Q τ g Q η I evalSub S R i Q I evalSub S R i x | ψ I evalSub S R j Q I evalSub S R j x | ψ
104 103 anbi2d f = I evalSub S R i g = I evalSub S R j φ f Q τ g Q η φ I evalSub S R i Q I evalSub S R i x | ψ I evalSub S R j Q I evalSub S R j x | ψ
105 ovex f + ˙ f g V
106 105 11 elab f + ˙ f g x | ψ ζ
107 oveq12 f = I evalSub S R i g = I evalSub S R j f + ˙ f g = I evalSub S R i + ˙ f I evalSub S R j
108 107 eleq1d f = I evalSub S R i g = I evalSub S R j f + ˙ f g x | ψ I evalSub S R i + ˙ f I evalSub S R j x | ψ
109 106 108 bitr3id f = I evalSub S R i g = I evalSub S R j ζ I evalSub S R i + ˙ f I evalSub S R j x | ψ
110 104 109 imbi12d f = I evalSub S R i g = I evalSub S R j φ f Q τ g Q η ζ φ I evalSub S R i Q I evalSub S R i x | ψ I evalSub S R j Q I evalSub S R j x | ψ I evalSub S R i + ˙ f I evalSub S R j x | ψ
111 89 90 110 5 vtocl2 φ I evalSub S R i Q I evalSub S R i x | ψ I evalSub S R j Q I evalSub S R j x | ψ I evalSub S R i + ˙ f I evalSub S R j x | ψ
112 76 82 88 111 syl12anc φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i + ˙ f I evalSub S R j x | ψ
113 75 112 eqeltrd φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i + I mPoly S 𝑠 R j x | ψ
114 elpreima I evalSub S R Fn Base I mPoly S 𝑠 R i + I mPoly S 𝑠 R j I evalSub S R -1 x | ψ i + I mPoly S 𝑠 R j Base I mPoly S 𝑠 R I evalSub S R i + I mPoly S 𝑠 R j x | ψ
115 29 114 syl φ i + I mPoly S 𝑠 R j I evalSub S R -1 x | ψ i + I mPoly S 𝑠 R j Base I mPoly S 𝑠 R I evalSub S R i + I mPoly S 𝑠 R j x | ψ
116 115 adantr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i + I mPoly S 𝑠 R j I evalSub S R -1 x | ψ i + I mPoly S 𝑠 R j Base I mPoly S 𝑠 R I evalSub S R i + I mPoly S 𝑠 R j x | ψ
117 62 113 116 mpbir2and φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i + I mPoly S 𝑠 R j I evalSub S R -1 x | ψ
118 117 adantlr φ y Base I mPoly S 𝑠 R i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i + I mPoly S 𝑠 R j I evalSub S R -1 x | ψ
119 25 37 ringcl I mPoly S 𝑠 R Ring i Base I mPoly S 𝑠 R j Base I mPoly S 𝑠 R i I mPoly S 𝑠 R j Base I mPoly S 𝑠 R
120 48 54 60 119 syl3anc φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i I mPoly S 𝑠 R j Base I mPoly S 𝑠 R
121 eqid mulGrp I mPoly S 𝑠 R = mulGrp I mPoly S 𝑠 R
122 eqid mulGrp S 𝑠 B I = mulGrp S 𝑠 B I
123 121 122 rhmmhm I evalSub S R I mPoly S 𝑠 R RingHom S 𝑠 B I I evalSub S R mulGrp I mPoly S 𝑠 R MndHom mulGrp S 𝑠 B I
124 19 24 123 3syl φ I evalSub S R mulGrp I mPoly S 𝑠 R MndHom mulGrp S 𝑠 B I
125 124 adantr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R mulGrp I mPoly S 𝑠 R MndHom mulGrp S 𝑠 B I
126 121 25 mgpbas Base I mPoly S 𝑠 R = Base mulGrp I mPoly S 𝑠 R
127 121 37 mgpplusg I mPoly S 𝑠 R = + mulGrp I mPoly S 𝑠 R
128 eqid S 𝑠 B I = S 𝑠 B I
129 122 128 mgpplusg S 𝑠 B I = + mulGrp S 𝑠 B I
130 126 127 129 mhmlin I evalSub S R mulGrp I mPoly S 𝑠 R MndHom mulGrp S 𝑠 B I i Base I mPoly S 𝑠 R j Base I mPoly S 𝑠 R I evalSub S R i I mPoly S 𝑠 R j = I evalSub S R i S 𝑠 B I I evalSub S R j
131 125 54 60 130 syl3anc φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i I mPoly S 𝑠 R j = I evalSub S R i S 𝑠 B I I evalSub S R j
132 23 26 69 70 72 73 3 128 pwsmulrval φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i S 𝑠 B I I evalSub S R j = I evalSub S R i · ˙ f I evalSub S R j
133 131 132 eqtrd φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i I mPoly S 𝑠 R j = I evalSub S R i · ˙ f I evalSub S R j
134 ovex f · ˙ f g V
135 134 12 elab f · ˙ f g x | ψ σ
136 oveq12 f = I evalSub S R i g = I evalSub S R j f · ˙ f g = I evalSub S R i · ˙ f I evalSub S R j
137 136 eleq1d f = I evalSub S R i g = I evalSub S R j f · ˙ f g x | ψ I evalSub S R i · ˙ f I evalSub S R j x | ψ
138 135 137 bitr3id f = I evalSub S R i g = I evalSub S R j σ I evalSub S R i · ˙ f I evalSub S R j x | ψ
139 104 138 imbi12d f = I evalSub S R i g = I evalSub S R j φ f Q τ g Q η σ φ I evalSub S R i Q I evalSub S R i x | ψ I evalSub S R j Q I evalSub S R j x | ψ I evalSub S R i · ˙ f I evalSub S R j x | ψ
140 89 90 139 6 vtocl2 φ I evalSub S R i Q I evalSub S R i x | ψ I evalSub S R j Q I evalSub S R j x | ψ I evalSub S R i · ˙ f I evalSub S R j x | ψ
141 76 82 88 140 syl12anc φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i · ˙ f I evalSub S R j x | ψ
142 133 141 eqeltrd φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ I evalSub S R i I mPoly S 𝑠 R j x | ψ
143 elpreima I evalSub S R Fn Base I mPoly S 𝑠 R i I mPoly S 𝑠 R j I evalSub S R -1 x | ψ i I mPoly S 𝑠 R j Base I mPoly S 𝑠 R I evalSub S R i I mPoly S 𝑠 R j x | ψ
144 29 143 syl φ i I mPoly S 𝑠 R j I evalSub S R -1 x | ψ i I mPoly S 𝑠 R j Base I mPoly S 𝑠 R I evalSub S R i I mPoly S 𝑠 R j x | ψ
145 144 adantr φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i I mPoly S 𝑠 R j I evalSub S R -1 x | ψ i I mPoly S 𝑠 R j Base I mPoly S 𝑠 R I evalSub S R i I mPoly S 𝑠 R j x | ψ
146 120 142 145 mpbir2and φ i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i I mPoly S 𝑠 R j I evalSub S R -1 x | ψ
147 146 adantlr φ y Base I mPoly S 𝑠 R i I evalSub S R -1 x | ψ j I evalSub S R -1 x | ψ i I mPoly S 𝑠 R j I evalSub S R -1 x | ψ
148 21 mplassa I V S 𝑠 R CRing I mPoly S 𝑠 R AssAlg
149 39 43 148 syl2anc φ I mPoly S 𝑠 R AssAlg
150 eqid Scalar I mPoly S 𝑠 R = Scalar I mPoly S 𝑠 R
151 38 150 asclrhm I mPoly S 𝑠 R AssAlg algSc I mPoly S 𝑠 R Scalar I mPoly S 𝑠 R RingHom I mPoly S 𝑠 R
152 eqid Base Scalar I mPoly S 𝑠 R = Base Scalar I mPoly S 𝑠 R
153 152 25 rhmf algSc I mPoly S 𝑠 R Scalar I mPoly S 𝑠 R RingHom I mPoly S 𝑠 R algSc I mPoly S 𝑠 R : Base Scalar I mPoly S 𝑠 R Base I mPoly S 𝑠 R
154 149 151 153 3syl φ algSc I mPoly S 𝑠 R : Base Scalar I mPoly S 𝑠 R Base I mPoly S 𝑠 R
155 154 adantr φ i Base S 𝑠 R algSc I mPoly S 𝑠 R : Base Scalar I mPoly S 𝑠 R Base I mPoly S 𝑠 R
156 21 39 43 mplsca φ S 𝑠 R = Scalar I mPoly S 𝑠 R
157 156 fveq2d φ Base S 𝑠 R = Base Scalar I mPoly S 𝑠 R
158 157 eleq2d φ i Base S 𝑠 R i Base Scalar I mPoly S 𝑠 R
159 158 biimpa φ i Base S 𝑠 R i Base Scalar I mPoly S 𝑠 R
160 155 159 ffvelrnd φ i Base S 𝑠 R algSc I mPoly S 𝑠 R i Base I mPoly S 𝑠 R
161 39 adantr φ i Base S 𝑠 R I V
162 40 adantr φ i Base S 𝑠 R S CRing
163 41 adantr φ i Base S 𝑠 R R SubRing S
164 1 subrgss R SubRing S R B
165 22 1 ressbas2 R B R = Base S 𝑠 R
166 41 164 165 3syl φ R = Base S 𝑠 R
167 166 eleq2d φ i R i Base S 𝑠 R
168 167 biimpar φ i Base S 𝑠 R i R
169 20 21 22 1 38 161 162 163 168 evlssca φ i Base S 𝑠 R I evalSub S R algSc I mPoly S 𝑠 R i = B I × i
170 14 ralrimiva φ f R χ
171 ovex B I V
172 snex f V
173 171 172 xpex B I × f V
174 173 7 elab B I × f x | ψ χ
175 sneq f = i f = i
176 175 xpeq2d f = i B I × f = B I × i
177 176 eleq1d f = i B I × f x | ψ B I × i x | ψ
178 174 177 bitr3id f = i χ B I × i x | ψ
179 178 cbvralvw f R χ i R B I × i x | ψ
180 170 179 sylib φ i R B I × i x | ψ
181 180 r19.21bi φ i R B I × i x | ψ
182 168 181 syldan φ i Base S 𝑠 R B I × i x | ψ
183 169 182 eqeltrd φ i Base S 𝑠 R I evalSub S R algSc I mPoly S 𝑠 R i x | ψ
184 elpreima I evalSub S R Fn Base I mPoly S 𝑠 R algSc I mPoly S 𝑠 R i I evalSub S R -1 x | ψ algSc I mPoly S 𝑠 R i Base I mPoly S 𝑠 R I evalSub S R algSc I mPoly S 𝑠 R i x | ψ
185 29 184 syl φ algSc I mPoly S 𝑠 R i I evalSub S R -1 x | ψ algSc I mPoly S 𝑠 R i Base I mPoly S 𝑠 R I evalSub S R algSc I mPoly S 𝑠 R i x | ψ
186 185 adantr φ i Base S 𝑠 R algSc I mPoly S 𝑠 R i I evalSub S R -1 x | ψ algSc I mPoly S 𝑠 R i Base I mPoly S 𝑠 R I evalSub S R algSc I mPoly S 𝑠 R i x | ψ
187 160 183 186 mpbir2and φ i Base S 𝑠 R algSc I mPoly S 𝑠 R i I evalSub S R -1 x | ψ
188 187 adantlr φ y Base I mPoly S 𝑠 R i Base S 𝑠 R algSc I mPoly S 𝑠 R i I evalSub S R -1 x | ψ
189 39 adantr φ i I I V
190 45 adantr φ i I S 𝑠 R Ring
191 simpr φ i I i I
192 21 35 25 189 190 191 mvrcl φ i I I mVar S 𝑠 R i Base I mPoly S 𝑠 R
193 40 adantr φ i I S CRing
194 41 adantr φ i I R SubRing S
195 20 35 22 1 189 193 194 191 evlsvar φ i I I evalSub S R I mVar S 𝑠 R i = g B I g i
196 171 mptex g B I g f V
197 196 8 elab g B I g f x | ψ θ
198 15 197 sylibr φ f I g B I g f x | ψ
199 198 ralrimiva φ f I g B I g f x | ψ
200 fveq2 f = i g f = g i
201 200 mpteq2dv f = i g B I g f = g B I g i
202 201 eleq1d f = i g B I g f x | ψ g B I g i x | ψ
203 202 cbvralvw f I g B I g f x | ψ i I g B I g i x | ψ
204 199 203 sylib φ i I g B I g i x | ψ
205 204 r19.21bi φ i I g B I g i x | ψ
206 195 205 eqeltrd φ i I I evalSub S R I mVar S 𝑠 R i x | ψ
207 elpreima I evalSub S R Fn Base I mPoly S 𝑠 R I mVar S 𝑠 R i I evalSub S R -1 x | ψ I mVar S 𝑠 R i Base I mPoly S 𝑠 R I evalSub S R I mVar S 𝑠 R i x | ψ
208 29 207 syl φ I mVar S 𝑠 R i I evalSub S R -1 x | ψ I mVar S 𝑠 R i Base I mPoly S 𝑠 R I evalSub S R I mVar S 𝑠 R i x | ψ
209 208 adantr φ i I I mVar S 𝑠 R i I evalSub S R -1 x | ψ I mVar S 𝑠 R i Base I mPoly S 𝑠 R I evalSub S R I mVar S 𝑠 R i x | ψ
210 192 206 209 mpbir2and φ i I I mVar S 𝑠 R i I evalSub S R -1 x | ψ
211 210 adantlr φ y Base I mPoly S 𝑠 R i I I mVar S 𝑠 R i I evalSub S R -1 x | ψ
212 simpr φ y Base I mPoly S 𝑠 R y Base I mPoly S 𝑠 R
213 39 adantr φ y Base I mPoly S 𝑠 R I V
214 43 adantr φ y Base I mPoly S 𝑠 R S 𝑠 R CRing
215 34 35 21 36 37 38 25 118 147 188 211 212 213 214 mplind φ y Base I mPoly S 𝑠 R y I evalSub S R -1 x | ψ
216 fvimacnvi Fun I evalSub S R y I evalSub S R -1 x | ψ I evalSub S R y x | ψ
217 33 215 216 syl2an2r φ y Base I mPoly S 𝑠 R I evalSub S R y x | ψ
218 eleq1 I evalSub S R y = A I evalSub S R y x | ψ A x | ψ
219 217 218 syl5ibcom φ y Base I mPoly S 𝑠 R I evalSub S R y = A A x | ψ
220 219 rexlimdva φ y Base I mPoly S 𝑠 R I evalSub S R y = A A x | ψ
221 32 220 mpd φ A x | ψ
222 13 elabg A Q A x | ψ ρ
223 16 222 syl φ A x | ψ ρ
224 221 223 mpbid φ ρ