Step | Hyp | Ref
| Expression |
1 | | mpfind.a |
. . . . 5
|
2 | | mpfind.cq |
. . . . 5
evalSub |
3 | 1, 2 | syl6eleq 2711 |
. . . 4
evalSub
|
4 | 2 | mpfrcl 19518 |
. . . . . . . . 9
SubRing |
5 | 1, 4 | syl 17 |
. . . . . . . 8
SubRing |
6 | | eqid 2622 |
. . . . . . . . 9
evalSub evalSub |
7 | | eqid 2622 |
. . . . . . . . 9
mPoly
↾s mPoly ↾s |
8 | | eqid 2622 |
. . . . . . . . 9
↾s ↾s |
9 | | eqid 2622 |
. . . . . . . . 9
s s |
10 | | mpfind.cb |
. . . . . . . . 9
|
11 | 6, 7, 8, 9, 10 | evlsrhm 19521 |
. . . . . . . 8
SubRing
evalSub mPoly ↾s RingHom s |
12 | 5, 11 | syl 17 |
. . . . . . 7
evalSub mPoly ↾s RingHom s |
13 | | eqid 2622 |
. . . . . . . 8
mPoly ↾s mPoly ↾s |
14 | | eqid 2622 |
. . . . . . . 8
s s |
15 | 13, 14 | rhmf 18726 |
. . . . . . 7
evalSub mPoly ↾s RingHom s evalSub mPoly ↾s s |
16 | 12, 15 | syl 17 |
. . . . . 6
evalSub mPoly ↾s s |
17 | | ffn 6045 |
. . . . . 6
evalSub mPoly ↾s s
evalSub mPoly ↾s |
18 | 16, 17 | syl 17 |
. . . . 5
evalSub mPoly ↾s |
19 | | fvelrnb 6243 |
. . . . 5
evalSub mPoly ↾s
evalSub mPoly
↾s evalSub |
20 | 18, 19 | syl 17 |
. . . 4
evalSub mPoly ↾s evalSub |
21 | 3, 20 | mpbid 222 |
. . 3
mPoly
↾s evalSub |
22 | | ffun 6048 |
. . . . . . . 8
evalSub mPoly ↾s s
evalSub |
23 | 16, 22 | syl 17 |
. . . . . . 7
evalSub |
24 | 23 | adantr 481 |
. . . . . 6
mPoly
↾s
evalSub |
25 | | eqid 2622 |
. . . . . . 7
↾s ↾s |
26 | | eqid 2622 |
. . . . . . 7
mVar
↾s mVar ↾s |
27 | | eqid 2622 |
. . . . . . 7
mPoly ↾s mPoly ↾s |
28 | | eqid 2622 |
. . . . . . 7
mPoly ↾s
mPoly ↾s |
29 | | eqid 2622 |
. . . . . . 7
algSc
mPoly ↾s algSc mPoly
↾s |
30 | 5 | simp1d 1073 |
. . . . . . . . . . . 12
|
31 | 5 | simp2d 1074 |
. . . . . . . . . . . . . 14
|
32 | 5 | simp3d 1075 |
. . . . . . . . . . . . . 14
SubRing |
33 | 8 | subrgcrng 18784 |
. . . . . . . . . . . . . 14
SubRing
↾s |
34 | 31, 32, 33 | syl2anc 693 |
. . . . . . . . . . . . 13
↾s |
35 | | crngring 18558 |
. . . . . . . . . . . . 13
↾s
↾s |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . 12
↾s |
37 | 7 | mplring 19452 |
. . . . . . . . . . . 12
↾s mPoly ↾s |
38 | 30, 36, 37 | syl2anc 693 |
. . . . . . . . . . 11
mPoly ↾s |
39 | 38 | adantr 481 |
. . . . . . . . . 10
evalSub
evalSub mPoly ↾s |
40 | | simprl 794 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub |
41 | | elpreima 6337 |
. . . . . . . . . . . . . 14
evalSub mPoly ↾s evalSub
mPoly ↾s evalSub |
42 | 18, 41 | syl 17 |
. . . . . . . . . . . . 13
evalSub
mPoly ↾s evalSub |
43 | 42 | adantr 481 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub
mPoly ↾s evalSub |
44 | 40, 43 | mpbid 222 |
. . . . . . . . . . 11
evalSub
evalSub mPoly ↾s evalSub |
45 | 44 | simpld 475 |
. . . . . . . . . 10
evalSub
evalSub mPoly
↾s |
46 | | simprr 796 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub |
47 | | elpreima 6337 |
. . . . . . . . . . . . . 14
evalSub mPoly ↾s evalSub
mPoly ↾s evalSub |
48 | 18, 47 | syl 17 |
. . . . . . . . . . . . 13
evalSub
mPoly ↾s evalSub |
49 | 48 | adantr 481 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub
mPoly ↾s evalSub |
50 | 46, 49 | mpbid 222 |
. . . . . . . . . . 11
evalSub
evalSub mPoly ↾s evalSub |
51 | 50 | simpld 475 |
. . . . . . . . . 10
evalSub
evalSub mPoly
↾s |
52 | 13, 27 | ringacl 18578 |
. . . . . . . . . 10
mPoly ↾s mPoly ↾s
mPoly ↾s mPoly
↾s mPoly
↾s |
53 | 39, 45, 51, 52 | syl3anc 1326 |
. . . . . . . . 9
evalSub
evalSub mPoly
↾s mPoly
↾s |
54 | | rhmghm 18725 |
. . . . . . . . . . . . . 14
evalSub mPoly ↾s RingHom s evalSub mPoly ↾s s |
55 | 12, 54 | syl 17 |
. . . . . . . . . . . . 13
evalSub mPoly ↾s s |
56 | 55 | adantr 481 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub mPoly ↾s s |
57 | | eqid 2622 |
. . . . . . . . . . . . 13
s s |
58 | 13, 27, 57 | ghmlin 17665 |
. . . . . . . . . . . 12
evalSub mPoly ↾s s
mPoly ↾s
mPoly ↾s evalSub
mPoly
↾s evalSub
s evalSub |
59 | 56, 45, 51, 58 | syl3anc 1326 |
. . . . . . . . . . 11
evalSub
evalSub evalSub
mPoly
↾s evalSub
s evalSub |
60 | 31 | adantr 481 |
. . . . . . . . . . . 12
evalSub
evalSub |
61 | | ovexd 6680 |
. . . . . . . . . . . 12
evalSub
evalSub |
62 | 16 | adantr 481 |
. . . . . . . . . . . . 13
evalSub
evalSub evalSub mPoly ↾s s
|
63 | 62, 45 | ffvelrnd 6360 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub s |
64 | 62, 51 | ffvelrnd 6360 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub s |
65 | | mpfind.cp |
. . . . . . . . . . . 12
|
66 | 9, 14, 60, 61, 63, 64, 65, 57 | pwsplusgval 16150 |
. . . . . . . . . . 11
evalSub
evalSub evalSub s evalSub evalSub evalSub |
67 | 59, 66 | eqtrd 2656 |
. . . . . . . . . 10
evalSub
evalSub evalSub
mPoly
↾s evalSub
evalSub |
68 | | simpl 473 |
. . . . . . . . . . 11
evalSub
evalSub |
69 | 18 | adantr 481 |
. . . . . . . . . . . . . 14
evalSub
evalSub evalSub mPoly ↾s |
70 | | fnfvelrn 6356 |
. . . . . . . . . . . . . 14
evalSub mPoly ↾s mPoly ↾s evalSub evalSub |
71 | 69, 45, 70 | syl2anc 693 |
. . . . . . . . . . . . 13
evalSub
evalSub evalSub evalSub |
72 | 71, 2 | syl6eleqr 2712 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub |
73 | 23 | adantr 481 |
. . . . . . . . . . . . 13
evalSub
evalSub
evalSub |
74 | | fvimacnvi 6331 |
. . . . . . . . . . . . 13
evalSub
evalSub evalSub |
75 | 73, 40, 74 | syl2anc 693 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub |
76 | 72, 75 | jca 554 |
. . . . . . . . . . 11
evalSub
evalSub evalSub evalSub |
77 | | fnfvelrn 6356 |
. . . . . . . . . . . . . 14
evalSub mPoly ↾s mPoly ↾s evalSub evalSub |
78 | 69, 51, 77 | syl2anc 693 |
. . . . . . . . . . . . 13
evalSub
evalSub evalSub evalSub |
79 | 78, 2 | syl6eleqr 2712 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub |
80 | | fvimacnvi 6331 |
. . . . . . . . . . . . 13
evalSub
evalSub evalSub |
81 | 73, 46, 80 | syl2anc 693 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub |
82 | 79, 81 | jca 554 |
. . . . . . . . . . 11
evalSub
evalSub evalSub evalSub |
83 | | fvex 6201 |
. . . . . . . . . . . 12
evalSub |
84 | | fvex 6201 |
. . . . . . . . . . . 12
evalSub |
85 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
evalSub evalSub |
86 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
87 | | mpfind.wc |
. . . . . . . . . . . . . . . . . 18
|
88 | 86, 87 | elab 3350 |
. . . . . . . . . . . . . . . . 17
|
89 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
evalSub evalSub |
90 | 88, 89 | syl5bbr 274 |
. . . . . . . . . . . . . . . 16
evalSub
evalSub
|
91 | 85, 90 | anbi12d 747 |
. . . . . . . . . . . . . . 15
evalSub evalSub
evalSub |
92 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
evalSub evalSub |
93 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
94 | | mpfind.wd |
. . . . . . . . . . . . . . . . . 18
|
95 | 93, 94 | elab 3350 |
. . . . . . . . . . . . . . . . 17
|
96 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
evalSub evalSub |
97 | 95, 96 | syl5bbr 274 |
. . . . . . . . . . . . . . . 16
evalSub
evalSub
|
98 | 92, 97 | anbi12d 747 |
. . . . . . . . . . . . . . 15
evalSub evalSub
evalSub |
99 | 91, 98 | bi2anan9 917 |
. . . . . . . . . . . . . 14
evalSub evalSub
evalSub
evalSub
evalSub evalSub |
100 | 99 | anbi2d 740 |
. . . . . . . . . . . . 13
evalSub evalSub
evalSub evalSub evalSub
evalSub |
101 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
102 | | mpfind.we |
. . . . . . . . . . . . . . 15
|
103 | 101, 102 | elab 3350 |
. . . . . . . . . . . . . 14
|
104 | | oveq12 6659 |
. . . . . . . . . . . . . . 15
evalSub evalSub
evalSub evalSub |
105 | 104 | eleq1d 2686 |
. . . . . . . . . . . . . 14
evalSub evalSub
evalSub
evalSub |
106 | 103, 105 | syl5bbr 274 |
. . . . . . . . . . . . 13
evalSub evalSub
evalSub
evalSub |
107 | 100, 106 | imbi12d 334 |
. . . . . . . . . . . 12
evalSub evalSub
evalSub evalSub evalSub
evalSub evalSub
evalSub |
108 | | mpfind.ad |
. . . . . . . . . . . 12
|
109 | 83, 84, 107, 108 | vtocl2 3261 |
. . . . . . . . . . 11
evalSub
evalSub
evalSub evalSub evalSub evalSub |
110 | 68, 76, 82, 109 | syl12anc 1324 |
. . . . . . . . . 10
evalSub
evalSub evalSub evalSub |
111 | 67, 110 | eqeltrd 2701 |
. . . . . . . . 9
evalSub
evalSub evalSub
mPoly
↾s |
112 | | elpreima 6337 |
. . . . . . . . . . 11
evalSub mPoly ↾s mPoly ↾s evalSub
mPoly ↾s mPoly ↾s evalSub mPoly ↾s |
113 | 18, 112 | syl 17 |
. . . . . . . . . 10
mPoly
↾s evalSub
mPoly ↾s mPoly ↾s evalSub mPoly ↾s |
114 | 113 | adantr 481 |
. . . . . . . . 9
evalSub
evalSub mPoly ↾s evalSub
mPoly ↾s mPoly ↾s evalSub mPoly ↾s |
115 | 53, 111, 114 | mpbir2and 957 |
. . . . . . . 8
evalSub
evalSub mPoly
↾s evalSub |
116 | 115 | adantlr 751 |
. . . . . . 7
mPoly ↾s evalSub
evalSub mPoly
↾s evalSub |
117 | 13, 28 | ringcl 18561 |
. . . . . . . . . 10
mPoly ↾s mPoly ↾s
mPoly ↾s mPoly
↾s mPoly
↾s |
118 | 39, 45, 51, 117 | syl3anc 1326 |
. . . . . . . . 9
evalSub
evalSub mPoly
↾s mPoly
↾s |
119 | | eqid 2622 |
. . . . . . . . . . . . . . 15
mulGrp
mPoly ↾s mulGrp mPoly
↾s |
120 | | eqid 2622 |
. . . . . . . . . . . . . . 15
mulGrp
s
mulGrp s |
121 | 119, 120 | rhmmhm 18722 |
. . . . . . . . . . . . . 14
evalSub mPoly ↾s RingHom s evalSub mulGrp mPoly ↾s MndHom mulGrp
s
|
122 | 12, 121 | syl 17 |
. . . . . . . . . . . . 13
evalSub mulGrp mPoly ↾s MndHom mulGrp
s
|
123 | 122 | adantr 481 |
. . . . . . . . . . . 12
evalSub
evalSub evalSub mulGrp mPoly ↾s MndHom mulGrp s |
124 | 119, 13 | mgpbas 18495 |
. . . . . . . . . . . . 13
mPoly ↾s mulGrp mPoly ↾s |
125 | 119, 28 | mgpplusg 18493 |
. . . . . . . . . . . . 13
mPoly ↾s mulGrp mPoly ↾s |
126 | | eqid 2622 |
. . . . . . . . . . . . . 14
s s |
127 | 120, 126 | mgpplusg 18493 |
. . . . . . . . . . . . 13
s mulGrp s
|
128 | 124, 125,
127 | mhmlin 17342 |
. . . . . . . . . . . 12
evalSub mulGrp mPoly ↾s MndHom mulGrp
s
mPoly ↾s mPoly ↾s evalSub mPoly ↾s evalSub s evalSub |
129 | 123, 45, 51, 128 | syl3anc 1326 |
. . . . . . . . . . 11
evalSub
evalSub evalSub mPoly ↾s evalSub s evalSub |
130 | | mpfind.ct |
. . . . . . . . . . . 12
|
131 | 9, 14, 60, 61, 63, 64, 130, 126 | pwsmulrval 16151 |
. . . . . . . . . . 11
evalSub
evalSub evalSub s evalSub evalSub evalSub |
132 | 129, 131 | eqtrd 2656 |
. . . . . . . . . 10
evalSub
evalSub evalSub mPoly ↾s evalSub evalSub |
133 | | ovex 6678 |
. . . . . . . . . . . . . . 15
|
134 | | mpfind.wf |
. . . . . . . . . . . . . . 15
|
135 | 133, 134 | elab 3350 |
. . . . . . . . . . . . . 14
|
136 | | oveq12 6659 |
. . . . . . . . . . . . . . 15
evalSub evalSub
evalSub evalSub |
137 | 136 | eleq1d 2686 |
. . . . . . . . . . . . . 14
evalSub evalSub
evalSub
evalSub |
138 | 135, 137 | syl5bbr 274 |
. . . . . . . . . . . . 13
evalSub evalSub
evalSub
evalSub |
139 | 100, 138 | imbi12d 334 |
. . . . . . . . . . . 12
evalSub evalSub
evalSub evalSub evalSub
evalSub evalSub
evalSub |
140 | | mpfind.mu |
. . . . . . . . . . . 12
|
141 | 83, 84, 139, 140 | vtocl2 3261 |
. . . . . . . . . . 11
evalSub
evalSub
evalSub evalSub evalSub evalSub |
142 | 68, 76, 82, 141 | syl12anc 1324 |
. . . . . . . . . 10
evalSub
evalSub evalSub evalSub |
143 | 132, 142 | eqeltrd 2701 |
. . . . . . . . 9
evalSub
evalSub evalSub mPoly ↾s |
144 | | elpreima 6337 |
. . . . . . . . . . 11
evalSub mPoly ↾s mPoly ↾s evalSub
mPoly ↾s mPoly ↾s evalSub mPoly ↾s |
145 | 18, 144 | syl 17 |
. . . . . . . . . 10
mPoly
↾s evalSub
mPoly ↾s mPoly ↾s evalSub mPoly ↾s |
146 | 145 | adantr 481 |
. . . . . . . . 9
evalSub
evalSub mPoly ↾s evalSub
mPoly ↾s mPoly ↾s evalSub mPoly ↾s |
147 | 118, 143,
146 | mpbir2and 957 |
. . . . . . . 8
evalSub
evalSub mPoly
↾s evalSub |
148 | 147 | adantlr 751 |
. . . . . . 7
mPoly ↾s evalSub
evalSub mPoly
↾s evalSub |
149 | 7 | mplassa 19454 |
. . . . . . . . . . . . . 14
↾s mPoly ↾s AssAlg |
150 | 30, 34, 149 | syl2anc 693 |
. . . . . . . . . . . . 13
mPoly ↾s AssAlg |
151 | | eqid 2622 |
. . . . . . . . . . . . . 14
Scalar
mPoly ↾s Scalar mPoly
↾s |
152 | 29, 151 | asclrhm 19342 |
. . . . . . . . . . . . 13
mPoly ↾s AssAlg
algSc
mPoly ↾s Scalar mPoly ↾s RingHom mPoly
↾s |
153 | 150, 152 | syl 17 |
. . . . . . . . . . . 12
algSc mPoly
↾s Scalar
mPoly ↾s RingHom mPoly ↾s |
154 | | eqid 2622 |
. . . . . . . . . . . . 13
Scalar mPoly
↾s Scalar mPoly
↾s |
155 | 154, 13 | rhmf 18726 |
. . . . . . . . . . . 12
algSc mPoly ↾s Scalar mPoly ↾s RingHom mPoly
↾s algSc mPoly ↾s Scalar mPoly ↾s mPoly
↾s |
156 | 153, 155 | syl 17 |
. . . . . . . . . . 11
algSc mPoly
↾s Scalar mPoly ↾s mPoly ↾s |
157 | 156 | adantr 481 |
. . . . . . . . . 10
↾s algSc mPoly
↾s Scalar mPoly ↾s mPoly ↾s |
158 | 7, 30, 34 | mplsca 19445 |
. . . . . . . . . . . . 13
↾s Scalar mPoly ↾s |
159 | 158 | fveq2d 6195 |
. . . . . . . . . . . 12
↾s Scalar mPoly ↾s |
160 | 159 | eleq2d 2687 |
. . . . . . . . . . 11
↾s
Scalar mPoly ↾s |
161 | 160 | biimpa 501 |
. . . . . . . . . 10
↾s Scalar mPoly
↾s |
162 | 157, 161 | ffvelrnd 6360 |
. . . . . . . . 9
↾s algSc mPoly ↾s mPoly ↾s |
163 | 30 | adantr 481 |
. . . . . . . . . . 11
↾s
|
164 | 31 | adantr 481 |
. . . . . . . . . . 11
↾s
|
165 | 32 | adantr 481 |
. . . . . . . . . . 11
↾s
SubRing |
166 | 10 | subrgss 18781 |
. . . . . . . . . . . . . . 15
SubRing
|
167 | 32, 166 | syl 17 |
. . . . . . . . . . . . . 14
|
168 | 8, 10 | ressbas2 15931 |
. . . . . . . . . . . . . 14
↾s |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . 13
↾s |
170 | 169 | eleq2d 2687 |
. . . . . . . . . . . 12
↾s |
171 | 170 | biimpar 502 |
. . . . . . . . . . 11
↾s |
172 | 6, 7, 8, 10, 29, 163, 164, 165, 171 | evlssca 19522 |
. . . . . . . . . 10
↾s evalSub algSc mPoly ↾s |
173 | | mpfind.co |
. . . . . . . . . . . . . 14
|
174 | 173 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
175 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
|
176 | | snex 4908 |
. . . . . . . . . . . . . . . . 17
|
177 | 175, 176 | xpex 6962 |
. . . . . . . . . . . . . . . 16
|
178 | | mpfind.wa |
. . . . . . . . . . . . . . . 16
|
179 | 177, 178 | elab 3350 |
. . . . . . . . . . . . . . 15
|
180 | | sneq 4187 |
. . . . . . . . . . . . . . . . 17
|
181 | 180 | xpeq2d 5139 |
. . . . . . . . . . . . . . . 16
|
182 | 181 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
|
183 | 179, 182 | syl5bbr 274 |
. . . . . . . . . . . . . 14
|
184 | 183 | cbvralv 3171 |
. . . . . . . . . . . . 13
|
185 | 174, 184 | sylib 208 |
. . . . . . . . . . . 12
|
186 | 185 | r19.21bi 2932 |
. . . . . . . . . . 11
|
187 | 171, 186 | syldan 487 |
. . . . . . . . . 10
↾s |
188 | 172, 187 | eqeltrd 2701 |
. . . . . . . . 9
↾s evalSub algSc mPoly ↾s |
189 | | elpreima 6337 |
. . . . . . . . . . 11
evalSub mPoly ↾s algSc mPoly ↾s evalSub
algSc mPoly
↾s mPoly ↾s evalSub algSc mPoly ↾s |
190 | 18, 189 | syl 17 |
. . . . . . . . . 10
algSc
mPoly ↾s evalSub
algSc mPoly
↾s mPoly ↾s evalSub algSc mPoly ↾s |
191 | 190 | adantr 481 |
. . . . . . . . 9
↾s algSc
mPoly ↾s evalSub
algSc mPoly
↾s mPoly ↾s evalSub algSc mPoly ↾s |
192 | 162, 188,
191 | mpbir2and 957 |
. . . . . . . 8
↾s algSc mPoly ↾s evalSub |
193 | 192 | adantlr 751 |
. . . . . . 7
mPoly ↾s
↾s algSc
mPoly ↾s evalSub |
194 | 30 | adantr 481 |
. . . . . . . . . 10
|
195 | 36 | adantr 481 |
. . . . . . . . . 10
↾s |
196 | | simpr 477 |
. . . . . . . . . 10
|
197 | 7, 26, 13, 194, 195, 196 | mvrcl 19449 |
. . . . . . . . 9
mVar ↾s mPoly ↾s |
198 | 31 | adantr 481 |
. . . . . . . . . . 11
|
199 | 32 | adantr 481 |
. . . . . . . . . . 11
SubRing |
200 | 6, 26, 8, 10, 194, 198, 199, 196 | evlsvar 19523 |
. . . . . . . . . 10
evalSub mVar ↾s |
201 | | mpfind.pr |
. . . . . . . . . . . . . 14
|
202 | 175 | mptex 6486 |
. . . . . . . . . . . . . . 15
|
203 | | mpfind.wb |
. . . . . . . . . . . . . . 15
|
204 | 202, 203 | elab 3350 |
. . . . . . . . . . . . . 14
|
205 | 201, 204 | sylibr 224 |
. . . . . . . . . . . . 13
|
206 | 205 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
207 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
208 | 207 | mpteq2dv 4745 |
. . . . . . . . . . . . . 14
|
209 | 208 | eleq1d 2686 |
. . . . . . . . . . . . 13
|
210 | 209 | cbvralv 3171 |
. . . . . . . . . . . 12
|
211 | 206, 210 | sylib 208 |
. . . . . . . . . . 11
|
212 | 211 | r19.21bi 2932 |
. . . . . . . . . 10
|
213 | 200, 212 | eqeltrd 2701 |
. . . . . . . . 9
evalSub mVar ↾s |
214 | | elpreima 6337 |
. . . . . . . . . . 11
evalSub mPoly ↾s mVar ↾s evalSub
mVar ↾s mPoly ↾s evalSub mVar ↾s |
215 | 18, 214 | syl 17 |
. . . . . . . . . 10
mVar
↾s evalSub
mVar ↾s mPoly ↾s evalSub mVar ↾s |
216 | 215 | adantr 481 |
. . . . . . . . 9
mVar ↾s evalSub
mVar ↾s mPoly ↾s evalSub mVar ↾s |
217 | 197, 213,
216 | mpbir2and 957 |
. . . . . . . 8
mVar ↾s evalSub |
218 | 217 | adantlr 751 |
. . . . . . 7
mPoly ↾s
mVar ↾s evalSub |
219 | | simpr 477 |
. . . . . . 7
mPoly
↾s
mPoly
↾s |
220 | 30 | adantr 481 |
. . . . . . 7
mPoly
↾s
|
221 | 34 | adantr 481 |
. . . . . . 7
mPoly
↾s
↾s |
222 | 25, 26, 7, 27, 28, 29, 13, 116, 148, 193, 218, 219, 220, 221 | mplind 19502 |
. . . . . 6
mPoly
↾s
evalSub |
223 | | fvimacnvi 6331 |
. . . . . 6
evalSub
evalSub evalSub |
224 | 24, 222, 223 | syl2anc 693 |
. . . . 5
mPoly
↾s
evalSub
|
225 | | eleq1 2689 |
. . . . 5
evalSub evalSub |
226 | 224, 225 | syl5ibcom 235 |
. . . 4
mPoly
↾s
evalSub |
227 | 226 | rexlimdva 3031 |
. . 3
mPoly ↾s evalSub |
228 | 21, 227 | mpd 15 |
. 2
|
229 | | mpfind.wg |
. . . 4
|
230 | 229 | elabg 3351 |
. . 3
|
231 | 1, 230 | syl 17 |
. 2
|
232 | 228, 231 | mpbid 222 |
1
|