Step | Hyp | Ref
| Expression |
1 | | dpjidcl.3 |
. . . 4
  DProd    |
2 | | dpjfval.2 |
. . . . 5
   |
3 | | dpjidcl.0 |
. . . . . 6
     |
4 | | dpjidcl.w |
. . . . . 6
 
   
finSupp  |
5 | 3, 4 | eldprd 17684 |
. . . . 5
   DProd 
  DProd 

g      |
6 | 2, 5 | syl 17 |
. . . 4
   DProd 
  DProd 

g      |
7 | 1, 6 | mpbid 215 |
. . 3
   DProd   g     |
8 | 7 | simprd 469 |
. 2
 
 g    |
9 | | dpjfval.1 |
. . . . 5
  DProd
  |
10 | 9 | adantr 471 |
. . . 4
 

 g     DProd   |
11 | 2 | adantr 471 |
. . . 4
 

 g   
  |
12 | 9 | ad2antrr 737 |
. . . . . 6
   
 g   
  DProd
  |
13 | 2 | ad2antrr 737 |
. . . . . 6
   
 g   
   |
14 | | dpjfval.p |
. . . . . 6
 dProj  |
15 | | simpr 467 |
. . . . . 6
   
 g   
   |
16 | 12, 13, 14, 15 | dpjf 17738 |
. . . . 5
   
 g   
        DProd          |
17 | 1 | ad2antrr 737 |
. . . . 5
   
 g   
  DProd    |
18 | 16, 17 | ffvelrnd 6045 |
. . . 4
   
 g   
               |
19 | 9, 2 | dprddomcld 17681 |
. . . . . . 7
   |
20 | | mptexg 6159 |
. . . . . . 7
             |
21 | 19, 20 | syl 17 |
. . . . . 6
             |
22 | 21 | adantr 471 |
. . . . 5
 

 g                |
23 | | funmpt 5636 |
. . . . . 6
           |
24 | 23 | a1i 11 |
. . . . 5
 

 g   

           |
25 | | simprl 769 |
. . . . . 6
 

 g      |
26 | 4, 10, 11, 25 | dprdffsupp 17695 |
. . . . 5
 

 g    finSupp
 |
27 | | eldifi 3566 |
. . . . . . . 8
   supp 
  |
28 | | eqid 2461 |
. . . . . . . . . 10
           |
29 | 12, 13, 14, 28, 15 | dpjval 17737 |
. . . . . . . . 9
   
 g   
                  DProd  
        |
30 | 29 | fveq1d 5889 |
. . . . . . . 8
   
 g   
                       DProd  
           |
31 | 27, 30 | sylan2 481 |
. . . . . . 7
   
 g   
  supp                         DProd  
           |
32 | | simplrr 776 |
. . . . . . . . . 10
   
 g   
  supp  
 g    |
33 | | eqid 2461 |
. . . . . . . . . . 11
         |
34 | | eqid 2461 |
. . . . . . . . . . 11
Cntz  Cntz   |
35 | | dprdgrp 17685 |
. . . . . . . . . . . . 13
  DProd
  |
36 | | grpmnd 16726 |
. . . . . . . . . . . . 13
   |
37 | 10, 35, 36 | 3syl 18 |
. . . . . . . . . . . 12
 

 g      |
38 | 37 | adantr 471 |
. . . . . . . . . . 11
   
 g   
  supp  
  |
39 | 19 | ad2antrr 737 |
. . . . . . . . . . 11
   
 g   
  supp  
  |
40 | 4, 10, 11, 25, 33 | dprdff 17693 |
. . . . . . . . . . . 12
 

 g              |
41 | 40 | adantr 471 |
. . . . . . . . . . 11
   
 g   
  supp             |
42 | 25 | adantr 471 |
. . . . . . . . . . . . 13
   
 g   
   |
43 | 4, 12, 13, 42, 34 | dprdfcntz 17696 |
. . . . . . . . . . . 12
   
 g   
  Cntz       |
44 | 27, 43 | sylan2 481 |
. . . . . . . . . . 11
   
 g   
  supp  
 Cntz       |
45 | | snssi 4128 |
. . . . . . . . . . . . 13
   supp 
    supp    |
46 | 45 | adantl 472 |
. . . . . . . . . . . 12
   
 g   
  supp     
 supp
   |
47 | 46 | difss2d 3574 |
. . . . . . . . . . . . 13
   
 g   
  supp       |
48 | | suppssdm 6953 |
. . . . . . . . . . . . . . 15
 supp  |
49 | | fdm 5755 |
. . . . . . . . . . . . . . . 16
        
  |
50 | 40, 49 | syl 17 |
. . . . . . . . . . . . . . 15
 

 g   
  |
51 | 48, 50 | syl5sseq 3491 |
. . . . . . . . . . . . . 14
 

 g     supp   |
52 | 51 | adantr 471 |
. . . . . . . . . . . . 13
   
 g   
  supp    supp   |
53 | | ssconb 3577 |
. . . . . . . . . . . . 13
     supp       supp
  supp

      |
54 | 47, 52, 53 | syl2anc 671 |
. . . . . . . . . . . 12
   
 g   
  supp        supp
  supp

      |
55 | 46, 54 | mpbid 215 |
. . . . . . . . . . 11
   
 g   
  supp    supp       |
56 | 26 | adantr 471 |
. . . . . . . . . . 11
   
 g   
  supp   finSupp  |
57 | 33, 3, 34, 38, 39, 41, 44, 55, 56 | gsumzres 17591 |
. . . . . . . . . 10
   
 g   
  supp    g  
      g    |
58 | 32, 57 | eqtr4d 2498 |
. . . . . . . . 9
   
 g   
  supp  
 g 
        |
59 | | eqid 2461 |
. . . . . . . . . . 11
        
        finSupp

        
       finSupp  |
60 | | difss 3571 |
. . . . . . . . . . . . . 14
   
 |
61 | 60 | a1i 11 |
. . . . . . . . . . . . 13
   
 g   
       |
62 | 12, 13, 61 | dprdres 17709 |
. . . . . . . . . . . 12
   
 g   
   DProd        DProd         DProd     |
63 | 62 | simpld 465 |
. . . . . . . . . . 11
   
 g   
  DProd
        |
64 | 12, 13 | dprdf2 17687 |
. . . . . . . . . . . . 13
   
 g   
     SubGrp    |
65 | | fssres 5771 |
. . . . . . . . . . . . 13
      SubGrp  
   
              SubGrp    |
66 | 64, 60, 65 | sylancl 673 |
. . . . . . . . . . . 12
   
 g   
  
            SubGrp    |
67 | | fdm 5755 |
. . . . . . . . . . . 12
 
             SubGrp   
          |
68 | 66, 67 | syl 17 |
. . . . . . . . . . 11
   
 g   
  
          |
69 | 40 | adantr 471 |
. . . . . . . . . . . . . . 15
   
 g   
           |
70 | 69 | feqmptd 5940 |
. . . . . . . . . . . . . 14
   
 g   
         |
71 | 70 | reseq1d 5122 |
. . . . . . . . . . . . 13
   
 g   
  
           
      |
72 | | resmpt 5172 |
. . . . . . . . . . . . . 14
            
                |
73 | 60, 72 | ax-mp 5 |
. . . . . . . . . . . . 13
      
                |
74 | 71, 73 | syl6eq 2511 |
. . . . . . . . . . . 12
   
 g   
  
                |
75 | | eldifi 3566 |
. . . . . . . . . . . . . . 15
       |
76 | 4, 12, 13, 42 | dprdfcl 17694 |
. . . . . . . . . . . . . . 15
    
 g    
           |
77 | 75, 76 | sylan2 481 |
. . . . . . . . . . . . . 14
    
 g    

              |
78 | | fvres 5901 |
. . . . . . . . . . . . . . 15
                     |
79 | 78 | adantl 472 |
. . . . . . . . . . . . . 14
    
 g    

      
             |
80 | 77, 79 | eleqtrrd 2542 |
. . . . . . . . . . . . 13
    
 g    

         
          |
81 | | difexg 4564 |
. . . . . . . . . . . . . . . . 17
 
     |
82 | 19, 81 | syl 17 |
. . . . . . . . . . . . . . . 16
       |
83 | | mptexg 6159 |
. . . . . . . . . . . . . . . 16
                 |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . 15
             |
85 | 84 | ad2antrr 737 |
. . . . . . . . . . . . . 14
   
 g   
             |
86 | | funmpt 5636 |
. . . . . . . . . . . . . . 15
           |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . 14
   
 g   
             |
88 | 26 | adantr 471 |
. . . . . . . . . . . . . 14
   
 g   
 finSupp
 |
89 | | ssdif 3579 |
. . . . . . . . . . . . . . . . . 18
           supp  
 supp    |
90 | 60, 89 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
      supp
   supp
  |
91 | 90 | sseli 3439 |
. . . . . . . . . . . . . . . 16
     
 supp    supp
   |
92 | | ssid 3462 |
. . . . . . . . . . . . . . . . . 18
 supp  supp
 |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   
 g   
  supp  supp   |
94 | 19 | ad2antrr 737 |
. . . . . . . . . . . . . . . . 17
   
 g   
   |
95 | | fvex 5897 |
. . . . . . . . . . . . . . . . . . 19
     |
96 | 3, 95 | eqeltri 2535 |
. . . . . . . . . . . . . . . . . 18
 |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   
 g   
   |
98 | 69, 93, 94, 97 | suppssr 6972 |
. . . . . . . . . . . . . . . 16
    
 g    

 supp
 
     |
99 | 91, 98 | sylan2 481 |
. . . . . . . . . . . . . . 15
    
 g    
      supp        |
100 | 82 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
   
 g   
       |
101 | 99, 100 | suppss2 6975 |
. . . . . . . . . . . . . 14
   
 g   
            supp
 supp
  |
102 | | fsuppsssupp 7924 |
. . . . . . . . . . . . . 14
                         finSupp            supp  supp             finSupp  |
103 | 85, 87, 88, 101, 102 | syl22anc 1277 |
. . . . . . . . . . . . 13
   
 g   
           finSupp  |
104 | 59, 63, 68, 80, 103 | dprdwd 17691 |
. . . . . . . . . . . 12
   
 g   
            

     
        finSupp
  |
105 | 74, 104 | eqeltrd 2539 |
. . . . . . . . . . 11
   
 g   
  
     
       
       finSupp   |
106 | 3, 59, 63, 68, 105 | eldprdi 17699 |
. . . . . . . . . 10
   
 g   
  g  
      DProd          |
107 | 27, 106 | sylan2 481 |
. . . . . . . . 9
   
 g   
  supp    g  
      DProd          |
108 | 58, 107 | eqeltrd 2539 |
. . . . . . . 8
   
 g   
  supp  
 DProd 
        |
109 | | eqid 2461 |
. . . . . . . . . 10
       |
110 | | eqid 2461 |
. . . . . . . . . 10
         |
111 | 64, 15 | ffvelrnd 6045 |
. . . . . . . . . 10
   
 g   
     SubGrp    |
112 | | dprdsubg 17705 |
. . . . . . . . . . 11
  DProd  
     DProd
       SubGrp    |
113 | 63, 112 | syl 17 |
. . . . . . . . . 10
   
 g   
  DProd        SubGrp    |
114 | 12, 13, 15, 3 | dpjdisj 17734 |
. . . . . . . . . 10
   
 g   
       DProd  
        |
115 | 12, 13, 15, 34 | dpjcntz 17733 |
. . . . . . . . . 10
   
 g   
    
 Cntz     DProd  
        |
116 | 109, 110,
3, 34, 111, 113, 114, 115, 28 | pj1rid 17400 |
. . . . . . . . 9
    
 g    

DProd                       DProd
            |
117 | 27, 116 | sylanl2 661 |
. . . . . . . 8
    
 g      supp    DProd  
     
              DProd  
          |
118 | 108, 117 | mpdan 679 |
. . . . . . 7
   
 g   
  supp                 DProd             |
119 | 31, 118 | eqtrd 2495 |
. . . . . 6
   
 g   
  supp            |
120 | 19 | adantr 471 |
. . . . . 6
 

 g      |
121 | 119, 120 | suppss2 6975 |
. . . . 5
 

 g               supp  supp
  |
122 | | fsuppsssupp 7924 |
. . . . 5
            
            finSupp            supp  supp
 

         finSupp  |
123 | 22, 24, 26, 121, 122 | syl22anc 1277 |
. . . 4
 

 g              finSupp  |
124 | 4, 10, 11, 18, 123 | dprdwd 17691 |
. . 3
 

 g                |
125 | | simprr 771 |
. . . 4
 

 g     g    |
126 | 40 | feqmptd 5940 |
. . . . . 6
 

 g            |
127 | | simplrr 776 |
. . . . . . . . . . 11
   
 g   
  g    |
128 | 12, 35, 36 | 3syl 18 |
. . . . . . . . . . . 12
   
 g   
   |
129 | 4, 12, 13, 42 | dprdffsupp 17695 |
. . . . . . . . . . . 12
   
 g   
 finSupp
 |
130 | | disjdif 3850 |
. . . . . . . . . . . . 13
   
     |
131 | 130 | a1i 11 |
. . . . . . . . . . . 12
   
 g   
           |
132 | | undif2 3854 |
. . . . . . . . . . . . 13
   
         |
133 | 15 | snssd 4129 |
. . . . . . . . . . . . . 14
   
 g   
     |
134 | | ssequn1 3615 |
. . . . . . . . . . . . . 14
         |
135 | 133, 134 | sylib 201 |
. . . . . . . . . . . . 13
   
 g   
       |
136 | 132, 135 | syl5req 2508 |
. . . . . . . . . . . 12
   
 g   
    
      |
137 | 33, 3, 109, 34, 128, 94, 69, 43, 129, 131, 136 | gsumzsplit 17608 |
. . . . . . . . . . 11
   
 g   
  g    g            g  
        |
138 | 69, 133 | feqresmpt 5941 |
. . . . . . . . . . . . . 14
   
 g   
               |
139 | 138 | oveq2d 6330 |
. . . . . . . . . . . . 13
   
 g   
  g       g            |
140 | 69, 15 | ffvelrnd 6045 |
. . . . . . . . . . . . . 14
   
 g   
           |
141 | | fveq2 5887 |
. . . . . . . . . . . . . . 15
           |
142 | 33, 141 | gsumsn 17635 |
. . . . . . . . . . . . . 14
 
          g                |
143 | 128, 15, 140, 142 | syl3anc 1276 |
. . . . . . . . . . . . 13
   
 g   
  g                |
144 | 139, 143 | eqtrd 2495 |
. . . . . . . . . . . 12
   
 g   
  g            |
145 | 144 | oveq1d 6329 |
. . . . . . . . . . 11
   
 g   
   g            g                    g           |
146 | 127, 137,
145 | 3eqtrd 2499 |
. . . . . . . . . 10
   
 g   
            g           |
147 | 12, 13, 15, 110 | dpjlsm 17735 |
. . . . . . . . . . . 12
   
 g   
  DProd              DProd  
        |
148 | 17, 147 | eleqtrd 2541 |
. . . . . . . . . . 11
   
 g   
             DProd
          |
149 | 4, 10, 11, 25 | dprdfcl 17694 |
. . . . . . . . . . 11
   
 g   
           |
150 | 109, 110,
3, 34, 111, 113, 114, 115, 28, 148, 149, 106 | pj1eq 17398 |
. . . . . . . . . 10
   
 g   
             g        
               DProd
                  DProd  
                     g  
         |
151 | 146, 150 | mpbid 215 |
. . . . . . . . 9
   
 g   
                DProd  
                DProd                        g  
        |
152 | 151 | simpld 465 |
. . . . . . . 8
   
 g   
               DProd                  |
153 | 30, 152 | eqtrd 2495 |
. . . . . . 7
   
 g   
               |
154 | 153 | mpteq2dva 4502 |
. . . . . 6
 

 g                      |
155 | 126, 154 | eqtr4d 2498 |
. . . . 5
 

 g                |
156 | 155 | oveq2d 6330 |
. . . 4
 

 g     g   g              |
157 | 125, 156 | eqtrd 2495 |
. . 3
 

 g     g              |
158 | 124, 157 | jca 539 |
. 2
 

 g                g               |
159 | 8, 158 | rexlimddv 2894 |
1
             g               |