Step | Hyp | Ref
| Expression |
1 | | mpfind.a |
. . . . 5
   |
2 | | mpfind.cq |
. . . . 5
  evalSub      |
3 | 1, 2 | syl6eleq 2550 |
. . . 4
   evalSub
      |
4 | 2 | mpfrcl 18790 |
. . . . . . . . 9
 
SubRing     |
5 | 1, 4 | syl 17 |
. . . . . . . 8
  SubRing     |
6 | | eqid 2462 |
. . . . . . . . 9
  evalSub       evalSub      |
7 | | eqid 2462 |
. . . . . . . . 9
 mPoly 
↾s    mPoly  ↾s    |
8 | | eqid 2462 |
. . . . . . . . 9
 ↾s   ↾s   |
9 | | eqid 2462 |
. . . . . . . . 9
 s     s     |
10 | | mpfind.cb |
. . . . . . . . 9
     |
11 | 6, 7, 8, 9, 10 | evlsrhm 18793 |
. . . . . . . 8
 
SubRing  
  evalSub       mPoly  ↾s   RingHom  s       |
12 | 5, 11 | syl 17 |
. . . . . . 7
   evalSub       mPoly  ↾s   RingHom  s       |
13 | | eqid 2462 |
. . . . . . . 8
    mPoly  ↾s        mPoly  ↾s     |
14 | | eqid 2462 |
. . . . . . . 8
    s         s      |
15 | 13, 14 | rhmf 18003 |
. . . . . . 7
   evalSub       mPoly  ↾s   RingHom  s       evalSub           mPoly  ↾s          s       |
16 | 12, 15 | syl 17 |
. . . . . 6
   evalSub           mPoly  ↾s          s       |
17 | | ffn 5751 |
. . . . . 6
   evalSub           mPoly  ↾s          s    
  evalSub         mPoly  ↾s      |
18 | 16, 17 | syl 17 |
. . . . 5
   evalSub         mPoly  ↾s      |
19 | | fvelrnb 5935 |
. . . . 5
   evalSub         mPoly  ↾s    
  evalSub          mPoly 
↾s        evalSub           |
20 | 18, 19 | syl 17 |
. . . 4
    evalSub          mPoly  ↾s        evalSub           |
21 | 3, 20 | mpbid 215 |
. . 3
      mPoly 
↾s        evalSub          |
22 | | ffun 5754 |
. . . . . . . 8
   evalSub           mPoly  ↾s          s    
  evalSub       |
23 | 16, 22 | syl 17 |
. . . . . . 7
   evalSub       |
24 | 23 | adantr 471 |
. . . . . 6
 
    mPoly 
↾s    
  evalSub       |
25 | | eqid 2462 |
. . . . . . 7
   
↾s       ↾s    |
26 | | eqid 2462 |
. . . . . . 7
 mVar 
↾s    mVar  ↾s    |
27 | | eqid 2462 |
. . . . . . 7
   mPoly  ↾s       mPoly  ↾s     |
28 | | eqid 2462 |
. . . . . . 7
    mPoly  ↾s       
mPoly  ↾s     |
29 | | eqid 2462 |
. . . . . . 7
algSc 
mPoly  ↾s    algSc  mPoly 
↾s     |
30 | 5 | simp1d 1026 |
. . . . . . . . . . . 12
   |
31 | 5 | simp2d 1027 |
. . . . . . . . . . . . . 14
   |
32 | 5 | simp3d 1028 |
. . . . . . . . . . . . . 14
 SubRing    |
33 | 8 | subrgcrng 18061 |
. . . . . . . . . . . . . 14
  SubRing  
 ↾s    |
34 | 31, 32, 33 | syl2anc 671 |
. . . . . . . . . . . . 13
 
↾s    |
35 | | crngring 17840 |
. . . . . . . . . . . . 13
  ↾s  
↾s    |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . 12
 
↾s    |
37 | 7 | mplring 18725 |
. . . . . . . . . . . 12
  
↾s    mPoly  ↾s     |
38 | 30, 36, 37 | syl2anc 671 |
. . . . . . . . . . 11
  mPoly  ↾s     |
39 | 38 | adantr 471 |
. . . . . . . . . 10
 
     evalSub         
    evalSub             mPoly  ↾s     |
40 | | simprl 769 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub                evalSub            |
41 | | elpreima 6025 |
. . . . . . . . . . . . . 14
   evalSub         mPoly  ↾s         evalSub         
     mPoly  ↾s       evalSub              |
42 | 18, 41 | syl 17 |
. . . . . . . . . . . . 13
      evalSub         
     mPoly  ↾s       evalSub              |
43 | 42 | adantr 471 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub                 evalSub         
     mPoly  ↾s       evalSub              |
44 | 40, 43 | mpbid 215 |
. . . . . . . . . . 11
 
     evalSub         
    evalSub                 mPoly  ↾s       evalSub             |
45 | 44 | simpld 465 |
. . . . . . . . . 10
 
     evalSub         
    evalSub                mPoly 
↾s      |
46 | | simprr 771 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub                evalSub            |
47 | | elpreima 6025 |
. . . . . . . . . . . . . 14
   evalSub         mPoly  ↾s         evalSub         
     mPoly  ↾s       evalSub              |
48 | 18, 47 | syl 17 |
. . . . . . . . . . . . 13
      evalSub         
     mPoly  ↾s       evalSub              |
49 | 48 | adantr 471 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub                 evalSub         
     mPoly  ↾s       evalSub              |
50 | 46, 49 | mpbid 215 |
. . . . . . . . . . 11
 
     evalSub         
    evalSub                 mPoly  ↾s       evalSub             |
51 | 50 | simpld 465 |
. . . . . . . . . 10
 
     evalSub         
    evalSub                mPoly 
↾s      |
52 | 13, 27 | ringacl 17857 |
. . . . . . . . . 10
   mPoly  ↾s       mPoly  ↾s   
    mPoly  ↾s          mPoly 
↾s          mPoly 
↾s      |
53 | 39, 45, 51, 52 | syl3anc 1276 |
. . . . . . . . 9
 
     evalSub         
    evalSub                 mPoly 
↾s          mPoly 
↾s      |
54 | | rhmghm 18002 |
. . . . . . . . . . . . . 14
   evalSub       mPoly  ↾s   RingHom  s       evalSub       mPoly  ↾s    s       |
55 | 12, 54 | syl 17 |
. . . . . . . . . . . . 13
   evalSub       mPoly  ↾s    s       |
56 | 55 | adantr 471 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub              evalSub       mPoly  ↾s    s       |
57 | | eqid 2462 |
. . . . . . . . . . . . 13
   s        s      |
58 | 13, 27, 57 | ghmlin 16937 |
. . . . . . . . . . . 12
    evalSub       mPoly  ↾s    s    
    mPoly  ↾s   
    mPoly  ↾s        evalSub         
  mPoly 
↾s           evalSub         
  s         evalSub           |
59 | 56, 45, 51, 58 | syl3anc 1276 |
. . . . . . . . . . 11
 
     evalSub         
    evalSub               evalSub         
  mPoly 
↾s           evalSub         
  s         evalSub           |
60 | 31 | adantr 471 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub              |
61 | | ovex 6343 |
. . . . . . . . . . . . 13
   |
62 | 61 | a1i 11 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub                |
63 | 16 | adantr 471 |
. . . . . . . . . . . . 13
 
     evalSub         
    evalSub              evalSub           mPoly  ↾s          s 
     |
64 | 63, 45 | ffvelrnd 6046 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub               evalSub            s       |
65 | 63, 51 | ffvelrnd 6046 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub               evalSub            s       |
66 | | mpfind.cp |
. . . . . . . . . . . 12
    |
67 | 9, 14, 60, 62, 64, 65, 66, 57 | pwsplusgval 15437 |
. . . . . . . . . . 11
 
     evalSub         
    evalSub                evalSub            s         evalSub             evalSub            evalSub           |
68 | 59, 67 | eqtrd 2496 |
. . . . . . . . . 10
 
     evalSub         
    evalSub               evalSub         
  mPoly 
↾s           evalSub        
   evalSub           |
69 | | simpl 463 |
. . . . . . . . . . 11
 
     evalSub         
    evalSub              |
70 | 18 | adantr 471 |
. . . . . . . . . . . . . 14
 
     evalSub         
    evalSub              evalSub         mPoly  ↾s      |
71 | | fnfvelrn 6042 |
. . . . . . . . . . . . . 14
    evalSub         mPoly  ↾s        mPoly  ↾s        evalSub          evalSub       |
72 | 70, 45, 71 | syl2anc 671 |
. . . . . . . . . . . . 13
 
     evalSub         
    evalSub               evalSub          evalSub       |
73 | 72, 2 | syl6eleqr 2551 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub               evalSub          |
74 | 23 | adantr 471 |
. . . . . . . . . . . . 13
 
     evalSub         
    evalSub           
  evalSub       |
75 | | fvimacnvi 6019 |
. . . . . . . . . . . . 13
    evalSub    
    evalSub              evalSub            |
76 | 74, 40, 75 | syl2anc 671 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub               evalSub            |
77 | 73, 76 | jca 539 |
. . . . . . . . . . 11
 
     evalSub         
    evalSub                evalSub           evalSub             |
78 | | fnfvelrn 6042 |
. . . . . . . . . . . . . 14
    evalSub         mPoly  ↾s        mPoly  ↾s        evalSub          evalSub       |
79 | 70, 51, 78 | syl2anc 671 |
. . . . . . . . . . . . 13
 
     evalSub         
    evalSub               evalSub          evalSub       |
80 | 79, 2 | syl6eleqr 2551 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub               evalSub          |
81 | | fvimacnvi 6019 |
. . . . . . . . . . . . 13
    evalSub    
    evalSub              evalSub            |
82 | 74, 46, 81 | syl2anc 671 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub               evalSub            |
83 | 80, 82 | jca 539 |
. . . . . . . . . . 11
 
     evalSub         
    evalSub                evalSub           evalSub             |
84 | | fvex 5898 |
. . . . . . . . . . . 12
   evalSub         |
85 | | fvex 5898 |
. . . . . . . . . . . 12
   evalSub         |
86 | | eleq1 2528 |
. . . . . . . . . . . . . . . 16
    evalSub            evalSub           |
87 | | vex 3060 |
. . . . . . . . . . . . . . . . . 18
 |
88 | | mpfind.wc |
. . . . . . . . . . . . . . . . . 18
     |
89 | 87, 88 | elab 3197 |
. . . . . . . . . . . . . . . . 17
  
  |
90 | | eleq1 2528 |
. . . . . . . . . . . . . . . . 17
    evalSub              evalSub             |
91 | 89, 90 | syl5bbr 267 |
. . . . . . . . . . . . . . . 16
    evalSub        
   evalSub
            |
92 | 86, 91 | anbi12d 722 |
. . . . . . . . . . . . . . 15
    evalSub               evalSub       
   evalSub              |
93 | | eleq1 2528 |
. . . . . . . . . . . . . . . 16
    evalSub            evalSub           |
94 | | vex 3060 |
. . . . . . . . . . . . . . . . . 18
 |
95 | | mpfind.wd |
. . . . . . . . . . . . . . . . . 18
     |
96 | 94, 95 | elab 3197 |
. . . . . . . . . . . . . . . . 17
  
  |
97 | | eleq1 2528 |
. . . . . . . . . . . . . . . . 17
    evalSub              evalSub             |
98 | 96, 97 | syl5bbr 267 |
. . . . . . . . . . . . . . . 16
    evalSub        
   evalSub
            |
99 | 93, 98 | anbi12d 722 |
. . . . . . . . . . . . . . 15
    evalSub               evalSub       
   evalSub              |
100 | 92, 99 | bi2anan9 889 |
. . . . . . . . . . . . . 14
     evalSub           evalSub        
      
     evalSub       
   evalSub          
    evalSub           evalSub               |
101 | 100 | anbi2d 715 |
. . . . . . . . . . . . 13
     evalSub           evalSub        
        
      evalSub           evalSub               evalSub       
   evalSub                |
102 | | ovex 6343 |
. . . . . . . . . . . . . . 15
    |
103 | | mpfind.we |
. . . . . . . . . . . . . . 15
    
   |
104 | 102, 103 | elab 3197 |
. . . . . . . . . . . . . 14
        |
105 | | oveq12 6324 |
. . . . . . . . . . . . . . 15
     evalSub           evalSub        
 
     evalSub            evalSub           |
106 | 105 | eleq1d 2524 |
. . . . . . . . . . . . . 14
     evalSub           evalSub        
          evalSub        
   evalSub              |
107 | 104, 106 | syl5bbr 267 |
. . . . . . . . . . . . 13
     evalSub           evalSub        
     evalSub        
   evalSub              |
108 | 101, 107 | imbi12d 326 |
. . . . . . . . . . . 12
     evalSub           evalSub        
  
       
       evalSub           evalSub               evalSub       
   evalSub                 evalSub        
   evalSub               |
109 | | mpfind.ad |
. . . . . . . . . . . 12
 
  
      |
110 | 84, 85, 108, 109 | vtocl2 3114 |
. . . . . . . . . . 11
 
     evalSub       
   evalSub          
    evalSub           evalSub                 evalSub            evalSub             |
111 | 69, 77, 83, 110 | syl12anc 1274 |
. . . . . . . . . 10
 
     evalSub         
    evalSub                evalSub            evalSub             |
112 | 68, 111 | eqeltrd 2540 |
. . . . . . . . 9
 
     evalSub         
    evalSub               evalSub         
  mPoly 
↾s           |
113 | | elpreima 6025 |
. . . . . . . . . . 11
   evalSub         mPoly  ↾s          mPoly  ↾s          evalSub         
      mPoly  ↾s          mPoly  ↾s       evalSub            mPoly  ↾s             |
114 | 18, 113 | syl 17 |
. . . . . . . . . 10
       mPoly 
↾s          evalSub         
      mPoly  ↾s          mPoly  ↾s       evalSub            mPoly  ↾s             |
115 | 114 | adantr 471 |
. . . . . . . . 9
 
     evalSub         
    evalSub                  mPoly  ↾s          evalSub       
 
      mPoly  ↾s          mPoly  ↾s       evalSub            mPoly  ↾s             |
116 | 53, 112, 115 | mpbir2and 938 |
. . . . . . . 8
 
     evalSub         
    evalSub                 mPoly 
↾s          evalSub            |
117 | 116 | adantlr 726 |
. . . . . . 7
       mPoly  ↾s          evalSub         
    evalSub                 mPoly 
↾s          evalSub            |
118 | 13, 28 | ringcl 17843 |
. . . . . . . . . 10
   mPoly  ↾s       mPoly  ↾s   
    mPoly  ↾s           mPoly 
↾s          mPoly 
↾s      |
119 | 39, 45, 51, 118 | syl3anc 1276 |
. . . . . . . . 9
 
     evalSub         
    evalSub                  mPoly 
↾s          mPoly 
↾s      |
120 | | eqid 2462 |
. . . . . . . . . . . . . . 15
mulGrp 
mPoly  ↾s    mulGrp  mPoly 
↾s     |
121 | | eqid 2462 |
. . . . . . . . . . . . . . 15
mulGrp 
s
    mulGrp  s      |
122 | 120, 121 | rhmmhm 17999 |
. . . . . . . . . . . . . 14
   evalSub       mPoly  ↾s   RingHom  s       evalSub      mulGrp  mPoly  ↾s    MndHom mulGrp 
s
       |
123 | 12, 122 | syl 17 |
. . . . . . . . . . . . 13
   evalSub      mulGrp  mPoly  ↾s    MndHom mulGrp 
s
       |
124 | 123 | adantr 471 |
. . . . . . . . . . . 12
 
     evalSub         
    evalSub              evalSub      mulGrp  mPoly  ↾s    MndHom mulGrp  s        |
125 | 120, 13 | mgpbas 17778 |
. . . . . . . . . . . . 13
    mPoly  ↾s       mulGrp  mPoly  ↾s      |
126 | 120, 28 | mgpplusg 17776 |
. . . . . . . . . . . . 13
    mPoly  ↾s      mulGrp  mPoly  ↾s      |
127 | | eqid 2462 |
. . . . . . . . . . . . . 14
    s         s      |
128 | 121, 127 | mgpplusg 17776 |
. . . . . . . . . . . . 13
    s       mulGrp  s 
     |
129 | 125, 126,
128 | mhmlin 16638 |
. . . . . . . . . . . 12
    evalSub      mulGrp  mPoly  ↾s    MndHom mulGrp 
s
         mPoly  ↾s        mPoly  ↾s        evalSub             mPoly  ↾s           evalSub             s         evalSub           |
130 | 124, 45, 51, 129 | syl3anc 1276 |
. . . . . . . . . . 11
 
     evalSub         
    evalSub               evalSub             mPoly  ↾s           evalSub             s         evalSub           |
131 | | mpfind.ct |
. . . . . . . . . . . 12
     |
132 | 9, 14, 60, 62, 64, 65, 131, 127 | pwsmulrval 15438 |
. . . . . . . . . . 11
 
     evalSub         
    evalSub                evalSub             s         evalSub             evalSub            evalSub           |
133 | 130, 132 | eqtrd 2496 |
. . . . . . . . . 10
 
     evalSub         
    evalSub               evalSub             mPoly  ↾s           evalSub            evalSub           |
134 | | ovex 6343 |
. . . . . . . . . . . . . . 15
    |
135 | | mpfind.wf |
. . . . . . . . . . . . . . 15
    
   |
136 | 134, 135 | elab 3197 |
. . . . . . . . . . . . . 14
        |
137 | | oveq12 6324 |
. . . . . . . . . . . . . . 15
     evalSub           evalSub        
 
     evalSub            evalSub           |
138 | 137 | eleq1d 2524 |
. . . . . . . . . . . . . 14
     evalSub           evalSub        
          evalSub        
   evalSub              |
139 | 136, 138 | syl5bbr 267 |
. . . . . . . . . . . . 13
     evalSub           evalSub        
     evalSub        
   evalSub              |
140 | 101, 139 | imbi12d 326 |
. . . . . . . . . . . 12
     evalSub           evalSub        
  
       
       evalSub           evalSub               evalSub       
   evalSub                 evalSub        
   evalSub               |
141 | | mpfind.mu |
. . . . . . . . . . . 12
 
  
      |
142 | 84, 85, 140, 141 | vtocl2 3114 |
. . . . . . . . . . 11
 
     evalSub       
   evalSub          
    evalSub           evalSub                 evalSub            evalSub             |
143 | 69, 77, 83, 142 | syl12anc 1274 |
. . . . . . . . . 10
 
     evalSub         
    evalSub                evalSub            evalSub             |
144 | 133, 143 | eqeltrd 2540 |
. . . . . . . . 9
 
     evalSub         
    evalSub               evalSub             mPoly  ↾s           |
145 | | elpreima 6025 |
. . . . . . . . . . 11
   evalSub         mPoly  ↾s           mPoly  ↾s          evalSub         
      
mPoly  ↾s          mPoly  ↾s       evalSub             mPoly  ↾s             |
146 | 18, 145 | syl 17 |
. . . . . . . . . 10
        mPoly 
↾s          evalSub         
      
mPoly  ↾s          mPoly  ↾s       evalSub             mPoly  ↾s             |
147 | 146 | adantr 471 |
. . . . . . . . 9
 
     evalSub         
    evalSub                   mPoly  ↾s          evalSub       
 
      
mPoly  ↾s          mPoly  ↾s       evalSub             mPoly  ↾s             |
148 | 119, 144,
147 | mpbir2and 938 |
. . . . . . . 8
 
     evalSub         
    evalSub                  mPoly 
↾s          evalSub            |
149 | 148 | adantlr 726 |
. . . . . . 7
       mPoly  ↾s          evalSub         
    evalSub                  mPoly 
↾s          evalSub            |
150 | 7 | mplassa 18727 |
. . . . . . . . . . . . . 14
  
↾s    mPoly  ↾s   AssAlg |
151 | 30, 34, 150 | syl2anc 671 |
. . . . . . . . . . . . 13
  mPoly  ↾s   AssAlg |
152 | | eqid 2462 |
. . . . . . . . . . . . . 14
Scalar 
mPoly  ↾s    Scalar  mPoly 
↾s     |
153 | 29, 152 | asclrhm 18615 |
. . . . . . . . . . . . 13
  mPoly  ↾s   AssAlg
algSc 
mPoly  ↾s     Scalar  mPoly  ↾s    RingHom  mPoly 
↾s      |
154 | 151, 153 | syl 17 |
. . . . . . . . . . . 12
 algSc  mPoly 
↾s     Scalar 
mPoly  ↾s    RingHom  mPoly  ↾s      |
155 | | eqid 2462 |
. . . . . . . . . . . . 13
   Scalar  mPoly 
↾s        Scalar  mPoly 
↾s      |
156 | 155, 13 | rhmf 18003 |
. . . . . . . . . . . 12
 algSc  mPoly  ↾s     Scalar  mPoly  ↾s    RingHom  mPoly 
↾s    algSc  mPoly  ↾s         Scalar  mPoly  ↾s           mPoly 
↾s      |
157 | 154, 156 | syl 17 |
. . . . . . . . . . 11
 algSc  mPoly 
↾s         Scalar  mPoly  ↾s           mPoly  ↾s      |
158 | 157 | adantr 471 |
. . . . . . . . . 10
 
    ↾s    algSc  mPoly 
↾s         Scalar  mPoly  ↾s           mPoly  ↾s      |
159 | 7, 30, 34 | mplsca 18718 |
. . . . . . . . . . . . 13
 
↾s  Scalar  mPoly  ↾s      |
160 | 159 | fveq2d 5892 |
. . . . . . . . . . . 12
     ↾s      Scalar  mPoly  ↾s       |
161 | 160 | eleq2d 2525 |
. . . . . . . . . . 11
      ↾s  
   Scalar  mPoly  ↾s        |
162 | 161 | biimpa 491 |
. . . . . . . . . 10
 
    ↾s       Scalar  mPoly 
↾s       |
163 | 158, 162 | ffvelrnd 6046 |
. . . . . . . . 9
 
    ↾s     algSc  mPoly  ↾s           mPoly  ↾s      |
164 | 30 | adantr 471 |
. . . . . . . . . . 11
 
    ↾s   
  |
165 | 31 | adantr 471 |
. . . . . . . . . . 11
 
    ↾s   
  |
166 | 32 | adantr 471 |
. . . . . . . . . . 11
 
    ↾s   
SubRing    |
167 | 10 | subrgss 18058 |
. . . . . . . . . . . . . . 15
 SubRing 
  |
168 | 32, 167 | syl 17 |
. . . . . . . . . . . . . 14

  |
169 | 8, 10 | ressbas2 15229 |
. . . . . . . . . . . . . 14
     ↾s     |
170 | 168, 169 | syl 17 |
. . . . . . . . . . . . 13
    
↾s     |
171 | 170 | eleq2d 2525 |
. . . . . . . . . . . 12
      ↾s      |
172 | 171 | biimpar 492 |
. . . . . . . . . . 11
 
    ↾s      |
173 | 6, 7, 8, 10, 29, 164, 165, 166, 172 | evlssca 18794 |
. . . . . . . . . 10
 
    ↾s       evalSub        algSc  mPoly  ↾s                |
174 | | mpfind.co |
. . . . . . . . . . . . . 14
 
   |
175 | 174 | ralrimiva 2814 |
. . . . . . . . . . . . 13
    |
176 | | snex 4655 |
. . . . . . . . . . . . . . . . 17
   |
177 | 61, 176 | xpex 6622 |
. . . . . . . . . . . . . . . 16
       |
178 | | mpfind.wa |
. . . . . . . . . . . . . . . 16
       
   |
179 | 177, 178 | elab 3197 |
. . . . . . . . . . . . . . 15
           |
180 | | sneq 3990 |
. . . . . . . . . . . . . . . . 17
       |
181 | 180 | xpeq2d 4877 |
. . . . . . . . . . . . . . . 16
               |
182 | 181 | eleq1d 2524 |
. . . . . . . . . . . . . . 15
                     |
183 | 179, 182 | syl5bbr 267 |
. . . . . . . . . . . . . 14
             |
184 | 183 | cbvralv 3031 |
. . . . . . . . . . . . 13
 
           |
185 | 175, 184 | sylib 201 |
. . . . . . . . . . . 12
            |
186 | 185 | r19.21bi 2769 |
. . . . . . . . . . 11
 
           |
187 | 172, 186 | syldan 477 |
. . . . . . . . . 10
 
    ↾s              |
188 | 173, 187 | eqeltrd 2540 |
. . . . . . . . 9
 
    ↾s       evalSub        algSc  mPoly  ↾s            |
189 | | elpreima 6025 |
. . . . . . . . . . 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 471 |
. . . . . . . . 9
 
    ↾s      algSc 
mPoly  ↾s           evalSub         
  algSc  mPoly 
↾s           mPoly  ↾s       evalSub        algSc  mPoly  ↾s              |
192 | 163, 188,
191 | mpbir2and 938 |
. . . . . . . 8
 
    ↾s     algSc  mPoly  ↾s           evalSub            |
193 | 192 | adantlr 726 |
. . . . . . 7
       mPoly  ↾s    
   
↾s     algSc 
mPoly  ↾s           evalSub            |
194 | 30 | adantr 471 |
. . . . . . . . . 10
 
   |
195 | 36 | adantr 471 |
. . . . . . . . . 10
 
  ↾s    |
196 | | simpr 467 |
. . . . . . . . . 10
 
   |
197 | 7, 26, 13, 194, 195, 196 | mvrcl 18722 |
. . . . . . . . 9
 
   mVar  ↾s          mPoly  ↾s      |
198 | 31 | adantr 471 |
. . . . . . . . . . 11
 
   |
199 | 32 | adantr 471 |
. . . . . . . . . . 11
 
 SubRing    |
200 | 6, 26, 8, 10, 194, 198, 199, 196 | evlsvar 18795 |
. . . . . . . . . 10
 
    evalSub         mVar  ↾s                 |
201 | | mpfind.pr |
. . . . . . . . . . . . . 14
 
   |
202 | 61 | mptex 6161 |
. . . . . . . . . . . . . . 15
         |
203 | | mpfind.wb |
. . . . . . . . . . . . . . 15
         
   |
204 | 202, 203 | elab 3197 |
. . . . . . . . . . . . . 14
          
  |
205 | 201, 204 | sylibr 217 |
. . . . . . . . . . . . 13
 
             |
206 | 205 | ralrimiva 2814 |
. . . . . . . . . . . 12
              |
207 | | fveq2 5888 |
. . . . . . . . . . . . . . 15
           |
208 | 207 | mpteq2dv 4504 |
. . . . . . . . . . . . . 14
                   |
209 | 208 | eleq1d 2524 |
. . . . . . . . . . . . 13
                         |
210 | 209 | cbvralv 3031 |
. . . . . . . . . . . 12
 
         

            |
211 | 206, 210 | sylib 201 |
. . . . . . . . . . 11
              |
212 | 211 | r19.21bi 2769 |
. . . . . . . . . 10
 
             |
213 | 200, 212 | eqeltrd 2540 |
. . . . . . . . 9
 
    evalSub         mVar  ↾s           |
214 | | elpreima 6025 |
. . . . . . . . . . 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 471 |
. . . . . . . . 9
 
    mVar  ↾s          evalSub         
   mVar  ↾s          mPoly  ↾s       evalSub         mVar  ↾s             |
217 | 197, 213,
216 | mpbir2and 938 |
. . . . . . . 8
 
   mVar  ↾s          evalSub            |
218 | 217 | adantlr 726 |
. . . . . . 7
       mPoly  ↾s    
   mVar  ↾s          evalSub            |
219 | | simpr 467 |
. . . . . . 7
 
    mPoly 
↾s    
    mPoly 
↾s      |
220 | 30 | adantr 471 |
. . . . . . 7
 
    mPoly 
↾s    
  |
221 | 34 | adantr 471 |
. . . . . . 7
 
    mPoly 
↾s    
 ↾s    |
222 | 25, 26, 7, 27, 28, 29, 13, 117, 149, 193, 218, 219, 220, 221 | mplind 18774 |
. . . . . 6
 
    mPoly 
↾s    
    evalSub            |
223 | | fvimacnvi 6019 |
. . . . . 6
    evalSub    
    evalSub              evalSub            |
224 | 24, 222, 223 | syl2anc 671 |
. . . . 5
 
    mPoly 
↾s    
   evalSub
           |
225 | | eleq1 2528 |
. . . . 5
    evalSub            evalSub               |
226 | 224, 225 | syl5ibcom 228 |
. . . 4
 
    mPoly 
↾s    
    evalSub             |
227 | 226 | rexlimdva 2891 |
. . 3
       mPoly  ↾s        evalSub             |
228 | 21, 227 | mpd 15 |
. 2
     |
229 | | mpfind.wg |
. . . 4
     |
230 | 229 | elabg 3198 |
. . 3
 
 
   |
231 | 1, 230 | syl 17 |
. 2
       |
232 | 228, 231 | mpbid 215 |
1
   |