Step | Hyp | Ref
| Expression |
1 | | mplsubg.s |
. . 3
 mPwSer   |
2 | | eqid 2462 |
. . 3
         |
3 | | eqid 2462 |
. . 3
         |
4 | | mpllss.r |
. . 3
   |
5 | | mplsubg.p |
. . . . 5
 mPoly   |
6 | | mplsubg.u |
. . . . 5
     |
7 | 5, 1, 6, 2 | mplbasss 18705 |
. . . 4
     |
8 | | mplsubrglem.x |
. . . 4
   |
9 | 7, 8 | sseldi 3442 |
. . 3
       |
10 | | mplsubrglem.y |
. . . 4
   |
11 | 7, 10 | sseldi 3442 |
. . 3
       |
12 | 1, 2, 3, 4, 9, 11 | psrmulcl 18661 |
. 2
               |
13 | | ovex 6343 |
. . . 4
         |
14 | 13 | a1i 11 |
. . 3
           |
15 | 1, 2 | psrelbasfun 18653 |
. . . 4
            
          |
16 | 12, 15 | syl 17 |
. . 3
           |
17 | | mplsubrglem.z |
. . . . 5
     |
18 | | fvex 5898 |
. . . . 5
     |
19 | 17, 18 | eqeltri 2536 |
. . . 4
 |
20 | 19 | a1i 11 |
. . 3
   |
21 | | mplsubrglem.p |
. . . . 5
    supp  supp    |
22 | | df-ima 4866 |
. . . . 5
    supp
 supp      supp
 supp    |
23 | 21, 22 | eqtri 2484 |
. . . 4

  supp  supp    |
24 | 5, 1, 2, 17, 6 | mplelbas 18703 |
. . . . . . . 8

    
finSupp   |
25 | 24 | simprbi 470 |
. . . . . . 7
 finSupp  |
26 | 8, 25 | syl 17 |
. . . . . 6
 finSupp
 |
27 | 5, 1, 2, 17, 6 | mplelbas 18703 |
. . . . . . . 8

    
finSupp   |
28 | 27 | simprbi 470 |
. . . . . . 7
 finSupp  |
29 | 10, 28 | syl 17 |
. . . . . 6
 finSupp
 |
30 | | fsuppxpfi 7926 |
. . . . . 6
  finSupp
finSupp   supp  supp    |
31 | 26, 29, 30 | syl2anc 671 |
. . . . 5
   supp  supp    |
32 | | ofmres 6816 |
. . . . . . 7
   supp
 supp     supp   supp      |
33 | | ovex 6343 |
. . . . . . 7
    |
34 | 32, 33 | fnmpt2i 6889 |
. . . . . 6
   supp
 supp     supp
 supp   |
35 | | dffn4 5822 |
. . . . . 6
    supp
 supp     supp
 supp  
  supp  supp       supp  supp       supp  supp     |
36 | 34, 35 | mpbi 213 |
. . . . 5
   supp
 supp       supp  supp    
  supp  supp    |
37 | | fofi 7886 |
. . . . 5
    supp  supp     supp  supp       supp  supp    
  supp
 supp   
   supp  supp     |
38 | 31, 36, 37 | sylancl 673 |
. . . 4
 
  supp  supp     |
39 | 23, 38 | syl5eqel 2544 |
. . 3
   |
40 | | eqid 2462 |
. . . . 5
         |
41 | | mplsubrglem.d |
. . . . 5
          |
42 | 1, 40, 41, 2, 12 | psrelbas 18652 |
. . . 4
                   |
43 | | mplsubrglem.t |
. . . . . 6
     |
44 | 9 | adantr 471 |
. . . . . 6
 

 
      |
45 | 11 | adantr 471 |
. . . . . 6
 

 
      |
46 | | eldifi 3567 |
. . . . . . 7
     |
47 | 46 | adantl 472 |
. . . . . 6
 

 
  |
48 | 1, 2, 43, 3, 41, 44, 45, 47 | psrmulval 18659 |
. . . . 5
 

 
             g                      |
49 | 4 | ad2antrr 737 |
. . . . . . . . . 10
      
  
  |
50 | 5, 40, 6, 41, 10 | mplelf 18706 |
. . . . . . . . . . . 12
           |
51 | 50 | ad2antrr 737 |
. . . . . . . . . . 11
      
             |
52 | | ssrab2 3526 |
. . . . . . . . . . . 12
    |
53 | | mplsubg.i |
. . . . . . . . . . . . . 14
   |
54 | 53 | ad2antrr 737 |
. . . . . . . . . . . . 13
      
  
  |
55 | 47 | adantr 471 |
. . . . . . . . . . . . 13
      
     |
56 | | simpr 467 |
. . . . . . . . . . . . 13
      
  


   |
57 | | eqid 2462 |
. . . . . . . . . . . . . 14
  


  |
58 | 41, 57 | psrbagconcl 18646 |
. . . . . . . . . . . . 13
 


 
 
      |
59 | 54, 55, 56, 58 | syl3anc 1276 |
. . . . . . . . . . . 12
      
      
    |
60 | 52, 59 | sseldi 3442 |
. . . . . . . . . . 11
      
        |
61 | 51, 60 | ffvelrnd 6046 |
. . . . . . . . . 10
      
                |
62 | 40, 43, 17 | ringlz 17866 |
. . . . . . . . . 10
      
      
         |
63 | 49, 61, 62 | syl2anc 671 |
. . . . . . . . 9
      
       
    |
64 | | oveq1 6322 |
. . . . . . . . . 10
         
                  |
65 | 64 | eqeq1d 2464 |
. . . . . . . . 9
               
             |
66 | 63, 65 | syl5ibrcom 230 |
. . . . . . . 8
      
                 
     |
67 | 5, 40, 6, 41, 8 | mplelf 18706 |
. . . . . . . . . . . 12
           |
68 | 67 | ad2antrr 737 |
. . . . . . . . . . 11
      
             |
69 | 52, 56 | sseldi 3442 |
. . . . . . . . . . 11
      
  
  |
70 | 68, 69 | ffvelrnd 6046 |
. . . . . . . . . 10
      
             |
71 | 40, 43, 17 | ringrz 17867 |
. . . . . . . . . 10
               
 |
72 | 49, 70, 71 | syl2anc 671 |
. . . . . . . . 9
      
       
 |
73 | | oveq2 6323 |
. . . . . . . . . 10
                 
          |
74 | 73 | eqeq1d 2464 |
. . . . . . . . 9
                          
  |
75 | 72, 74 | syl5ibrcom 230 |
. . . . . . . 8
      
               
          |
76 | 41 | psrbagf 18638 |
. . . . . . . . . . . . . . . . . 18
 
       |
77 | 54, 69, 76 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
      
         |
78 | 77 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . 16
   
  


         |
79 | 41 | psrbagf 18638 |
. . . . . . . . . . . . . . . . . 18
 
       |
80 | 54, 55, 79 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
      
         |
81 | 80 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . 16
   
  


         |
82 | | nn0cn 10908 |
. . . . . . . . . . . . . . . . 17
    
      |
83 | | nn0cn 10908 |
. . . . . . . . . . . . . . . . 17
    
      |
84 | | pncan3 9909 |
. . . . . . . . . . . . . . . . 17
                                 |
85 | 82, 83, 84 | syl2an 484 |
. . . . . . . . . . . . . . . 16
                                 |
86 | 78, 81, 85 | syl2anc 671 |
. . . . . . . . . . . . . . 15
   
  


                         |
87 | 86 | mpteq2dva 4503 |
. . . . . . . . . . . . . 14
      
                             |
88 | | ovex 6343 |
. . . . . . . . . . . . . . . 16
           |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . 15
   
  


               |
90 | 77 | feqmptd 5941 |
. . . . . . . . . . . . . . 15
      
  

       |
91 | 80 | feqmptd 5941 |
. . . . . . . . . . . . . . . 16
      
           |
92 | 54, 81, 78, 91, 90 | offval2 6575 |
. . . . . . . . . . . . . . 15
      
                    |
93 | 54, 78, 89, 90, 92 | offval2 6575 |
. . . . . . . . . . . . . 14
      
                             |
94 | 87, 93, 91 | 3eqtr4d 2506 |
. . . . . . . . . . . . 13
      
           |
95 | | simplr 767 |
. . . . . . . . . . . . 13
      
       |
96 | 94, 95 | eqeltrd 2540 |
. . . . . . . . . . . 12
      
             |
97 | 96 | eldifbd 3429 |
. . . . . . . . . . 11
      
           |
98 | | ovres 6463 |
. . . . . . . . . . . 12
   supp     supp
      supp
 supp                |
99 | | fnovrn 6471 |
. . . . . . . . . . . . . 14
     supp  supp     supp  supp   supp     supp 
     supp  supp        
  supp  supp     |
100 | 99, 23 | syl6eleqr 2551 |
. . . . . . . . . . . . 13
     supp  supp     supp  supp   supp     supp 
     supp  supp          |
101 | 34, 100 | mp3an1 1360 |
. . . . . . . . . . . 12
   supp     supp
      supp
 supp          |
102 | 98, 101 | eqeltrrd 2541 |
. . . . . . . . . . 11
   supp     supp
         |
103 | 97, 102 | nsyl 126 |
. . . . . . . . . 10
      
     supp
    supp    |
104 | | ianor 495 |
. . . . . . . . . 10
   supp
    supp    supp     supp    |
105 | 103, 104 | sylib 201 |
. . . . . . . . 9
      
     supp     supp    |
106 | | eldif 3426 |
. . . . . . . . . . . . 13
   supp
   supp    |
107 | 106 | baib 919 |
. . . . . . . . . . . 12
    supp 
 supp    |
108 | 69, 107 | syl 17 |
. . . . . . . . . . 11
      
      supp 
 supp    |
109 | | ssid 3463 |
. . . . . . . . . . . . . 14
 supp  supp  |
110 | 109 | a1i 11 |
. . . . . . . . . . . . 13
      
    supp
 supp   |
111 | | ovex 6343 |
. . . . . . . . . . . . . . 15
   |
112 | 41, 111 | rabex2 4570 |
. . . . . . . . . . . . . 14
 |
113 | 112 | a1i 11 |
. . . . . . . . . . . . 13
      
  
  |
114 | 19 | a1i 11 |
. . . . . . . . . . . . 13
      
     |
115 | 68, 110, 113, 114 | suppssr 6973 |
. . . . . . . . . . . 12
   
  


    supp        |
116 | 115 | ex 440 |
. . . . . . . . . . 11
      
      supp        |
117 | 108, 116 | sylbird 243 |
. . . . . . . . . 10
      
     supp       |
118 | | eldif 3426 |
. . . . . . . . . . . . 13
      supp 
        supp    |
119 | 118 | baib 919 |
. . . . . . . . . . . 12
          supp

 
  supp    |
120 | 60, 119 | syl 17 |
. . . . . . . . . . 11
      
         supp

 
  supp    |
121 | | ssid 3463 |
. . . . . . . . . . . . . 14
 supp  supp  |
122 | 121 | a1i 11 |
. . . . . . . . . . . . 13
      
    supp
 supp   |
123 | 51, 122, 113, 114 | suppssr 6973 |
. . . . . . . . . . . 12
   
  


       supp           |
124 | 123 | ex 440 |
. . . . . . . . . . 11
      
         supp

         |
125 | 120, 124 | sylbird 243 |
. . . . . . . . . 10
      
        supp     
    |
126 | 117, 125 | orim12d 854 |
. . . . . . . . 9
      
      supp     supp                 |
127 | 105, 126 | mpd 15 |
. . . . . . . 8
      
                 |
128 | 66, 75, 127 | mpjaod 387 |
. . . . . . 7
      
            
    |
129 | 128 | mpteq2dva 4503 |
. . . . . 6
 

 
 
                   
  |
130 | 129 | oveq2d 6331 |
. . . . 5
 

 
 g                     g 
  
   |
131 | 4 | adantr 471 |
. . . . . . 7
 

 
  |
132 | | ringmnd 17838 |
. . . . . . 7

  |
133 | 131, 132 | syl 17 |
. . . . . 6
 

 
  |
134 | 41 | psrbaglefi 18645 |
. . . . . . 7
 
 
    |
135 | 53, 46, 134 | syl2an 484 |
. . . . . 6
 

 


   |
136 | 17 | gsumz 16670 |
. . . . . 6
       g   
   |
137 | 133, 135,
136 | syl2anc 671 |
. . . . 5
 

 
 g    
  |
138 | 48, 130, 137 | 3eqtrd 2500 |
. . . 4
 

 
             |
139 | 42, 138 | suppss 6972 |
. . 3
          supp   |
140 | | suppssfifsupp 7924 |
. . 3
                    
         supp
          finSupp
 |
141 | 14, 16, 20, 39, 139, 140 | syl32anc 1284 |
. 2
         finSupp
 |
142 | 5, 1, 2, 17, 6 | mplelbas 18703 |
. 2
        
            
        finSupp   |
143 | 12, 141, 142 | sylanbrc 675 |
1
           |