Step | Hyp | Ref
| Expression |
1 | | 1on 7207 |
. . . . . . 7
 |
2 | 1 | a1i 11 |
. . . . . 6
   |
3 | | evls1sca.s |
. . . . . 6
   |
4 | | evls1sca.r |
. . . . . 6
 SubRing    |
5 | | eqid 2471 |
. . . . . . 7
  evalSub       evalSub      |
6 | | eqid 2471 |
. . . . . . 7
 mPoly   mPoly   |
7 | | evls1sca.u |
. . . . . . 7

↾s   |
8 | | eqid 2471 |
. . . . . . 7
 s     s     |
9 | | evls1sca.b |
. . . . . . 7
     |
10 | 5, 6, 7, 8, 9 | evlsrhm 18821 |
. . . . . 6
 
SubRing  
  evalSub       mPoly  RingHom  s       |
11 | 2, 3, 4, 10 | syl3anc 1292 |
. . . . 5
   evalSub       mPoly  RingHom  s       |
12 | | eqid 2471 |
. . . . . 6
    mPoly
      mPoly
   |
13 | | eqid 2471 |
. . . . . 6
    s         s      |
14 | 12, 13 | rhmf 18032 |
. . . . 5
   evalSub
      mPoly
 RingHom  s       evalSub           mPoly         s 
     |
15 | 11, 14 | syl 17 |
. . . 4
   evalSub           mPoly         s 
     |
16 | | evls1sca.a |
. . . . . . 7
algSc   |
17 | | eqid 2471 |
. . . . . . 7
Scalar  Scalar   |
18 | 7 | subrgring 18089 |
. . . . . . . . 9
 SubRing 
  |
19 | 4, 18 | syl 17 |
. . . . . . . 8
   |
20 | | evls1sca.w |
. . . . . . . . 9
Poly1   |
21 | 20 | ply1ring 18918 |
. . . . . . . 8

  |
22 | 19, 21 | syl 17 |
. . . . . . 7
   |
23 | 20 | ply1lmod 18922 |
. . . . . . . 8

  |
24 | 19, 23 | syl 17 |
. . . . . . 7
   |
25 | | eqid 2471 |
. . . . . . 7
   Scalar      Scalar    |
26 | | eqid 2471 |
. . . . . . 7
         |
27 | 16, 17, 22, 24, 25, 26 | asclf 18638 |
. . . . . 6
      Scalar           |
28 | 9 | subrgss 18087 |
. . . . . . . . . 10
 SubRing 
  |
29 | 4, 28 | syl 17 |
. . . . . . . . 9

  |
30 | 7, 9 | ressbas2 15258 |
. . . . . . . . 9
       |
31 | 29, 30 | syl 17 |
. . . . . . . 8
       |
32 | 20 | ply1sca 18923 |
. . . . . . . . . 10

Scalar    |
33 | 19, 32 | syl 17 |
. . . . . . . . 9
 Scalar    |
34 | 33 | fveq2d 5883 |
. . . . . . . 8
        Scalar     |
35 | 31, 34 | eqtrd 2505 |
. . . . . . 7
    Scalar     |
36 | | eqid 2471 |
. . . . . . . . . 10
PwSer1  PwSer1   |
37 | 20, 36, 26 | ply1bas 18865 |
. . . . . . . . 9
        mPoly    |
38 | 37 | a1i 11 |
. . . . . . . 8
         mPoly
    |
39 | 38 | eqcomd 2477 |
. . . . . . 7
     mPoly         |
40 | 35, 39 | feq23d 5734 |
. . . . . 6
          mPoly  
     Scalar            |
41 | 27, 40 | mpbird 240 |
. . . . 5
         mPoly
    |
42 | | evls1sca.x |
. . . . 5
   |
43 | 41, 42 | ffvelrnd 6038 |
. . . 4
         mPoly
    |
44 | | fvco3 5957 |
. . . 4
    evalSub           mPoly         s 
           mPoly                      evalSub                                 evalSub
              |
45 | 15, 43, 44 | syl2anc 673 |
. . 3
     
            
evalSub                                 evalSub               |
46 | 16 | a1i 11 |
. . . . . . . 8
 algSc    |
47 | | eqid 2471 |
. . . . . . . . 9
algSc  algSc   |
48 | 20, 47 | ply1ascl 18928 |
. . . . . . . 8
algSc  algSc  mPoly
   |
49 | 46, 48 | syl6eq 2521 |
. . . . . . 7
 algSc 
mPoly     |
50 | 49 | fveq1d 5881 |
. . . . . 6
      algSc  mPoly
       |
51 | 50 | fveq2d 5883 |
. . . . 5
    evalSub               evalSub        algSc  mPoly
        |
52 | | eqid 2471 |
. . . . . 6
algSc 
mPoly   algSc  mPoly    |
53 | 5, 6, 7, 9, 52, 2,
3, 4, 42 | evlssca 18822 |
. . . . 5
    evalSub        algSc  mPoly
              |
54 | 51, 53 | eqtrd 2505 |
. . . 4
    evalSub              
     |
55 | 54 | fveq2d 5883 |
. . 3
                     evalSub
                                      |
56 | | eqidd 2472 |
. . . . 5
                 
             |
57 | | coeq1 4997 |
. . . . . 6
                               |
58 | 57 | adantl 473 |
. . . . 5
 
  
                            |
59 | 29, 42 | sseldd 3419 |
. . . . . . 7
   |
60 | | fconst6g 5785 |
. . . . . . 7
               |
61 | 59, 60 | syl 17 |
. . . . . 6
   
           |
62 | | fvex 5889 |
. . . . . . . . 9
     |
63 | 9, 62 | eqeltri 2545 |
. . . . . . . 8
 |
64 | 63 | a1i 11 |
. . . . . . 7
   |
65 | | ovex 6336 |
. . . . . . . 8
   |
66 | 65 | a1i 11 |
. . . . . . 7
  
  |
67 | 64, 66 | elmapd 7504 |
. . . . . 6
         
                 |
68 | 61, 67 | mpbird 240 |
. . . . 5
   
         |
69 | | snex 4641 |
. . . . . . . 8
 
 |
70 | 65, 69 | xpex 6614 |
. . . . . . 7
       |
71 | 70 | a1i 11 |
. . . . . 6
   
     |
72 | | mptexg 6151 |
. . . . . . 7
         |
73 | 64, 72 | syl 17 |
. . . . . 6
         |
74 | | coexg 6763 |
. . . . . 6
    
                          |
75 | 71, 73, 74 | syl2anc 673 |
. . . . 5
                 |
76 | 56, 58, 68, 75 | fvmptd 5969 |
. . . 4
                            
            |
77 | | fconst6g 5785 |
. . . . . . 7
           |
78 | 77 | adantl 473 |
. . . . . 6
 
           |
79 | 63, 1 | pm3.2i 462 |
. . . . . . . 8
   |
80 | 79 | a1i 11 |
. . . . . . 7
 
 
   |
81 | | elmapg 7503 |
. . . . . . 7
         
           |
82 | 80, 81 | syl 17 |
. . . . . 6
 
                   |
83 | 78, 82 | mpbird 240 |
. . . . 5
 
         |
84 | | eqidd 2472 |
. . . . 5
               |
85 | | fconstmpt 4883 |
. . . . . 6
        
  |
86 | 85 | a1i 11 |
. . . . 5
   
         |
87 | | eqidd 2472 |
. . . . 5
       |
88 | 83, 84, 86, 87 | fmptco 6072 |
. . . 4
                   |
89 | 76, 88 | eqtrd 2505 |
. . 3
                             |
90 | 45, 55, 89 | 3eqtrd 2509 |
. 2
     
            
evalSub                 |
91 | | elpwg 3950 |
. . . . . 6
 SubRing 
 
   |
92 | 28, 91 | mpbird 240 |
. . . . 5
 SubRing 
   |
93 | 4, 92 | syl 17 |
. . . 4
    |
94 | | evls1sca.q |
. . . . 5

evalSub1   |
95 | | eqid 2471 |
. . . . 5
 evalSub   evalSub   |
96 | 94, 95, 9 | evls1fval 18985 |
. . . 4
   
                 evalSub        |
97 | 3, 93, 96 | syl2anc 673 |
. . 3
                  evalSub        |
98 | 97 | fveq1d 5881 |
. 2
                           evalSub               |
99 | | fconstmpt 4883 |
. . 3
       |
100 | 99 | a1i 11 |
. 2
         |
101 | 90, 98, 100 | 3eqtr4d 2515 |
1
               |