Step | Hyp | Ref
| Expression |
1 | | dprdsplit.u |
. . . . . 6
     |
2 | 1 | adantr 472 |
. . . . 5
 
     |
3 | 2 | eleq2d 2534 |
. . . 4
 
 

    |
4 | | elun 3565 |
. . . 4
  

   |
5 | 3, 4 | syl6bb 269 |
. . 3
 
 

    |
6 | | dmdprdsplit2.1 |
. . . . . . . 8
  DProd
    |
7 | 6 | ad2antrr 740 |
. . . . . . 7
    
   DProd     |
8 | | dprdsplit.2 |
. . . . . . . . . 10
     SubGrp    |
9 | | ssun1 3588 |
. . . . . . . . . . 11

  |
10 | 9, 1 | syl5sseqr 3467 |
. . . . . . . . . 10

  |
11 | 8, 10 | fssresd 5762 |
. . . . . . . . 9
       SubGrp    |
12 | | fdm 5745 |
. . . . . . . . 9
 
     SubGrp      |
13 | 11, 12 | syl 17 |
. . . . . . . 8
     |
14 | 13 | ad2antrr 740 |
. . . . . . 7
    
 
    |
15 | | simplr 770 |
. . . . . . 7
    
    |
16 | | simprl 772 |
. . . . . . 7
    
    |
17 | | simprr 774 |
. . . . . . 7
    
    |
18 | | dmdprdsplit.z |
. . . . . . 7
Cntz   |
19 | 7, 14, 15, 16, 17, 18 | dprdcntz 17718 |
. . . . . 6
    
       
            |
20 | | fvres 5893 |
. . . . . . 7
             |
21 | 20 | ad2antlr 741 |
. . . . . 6
    
              |
22 | | fvres 5893 |
. . . . . . . 8
             |
23 | 22 | ad2antrl 742 |
. . . . . . 7
    
              |
24 | 23 | fveq2d 5883 |
. . . . . 6
    
                      |
25 | 19, 21, 24 | 3sstr3d 3460 |
. . . . 5
    
                |
26 | 25 | exp32 616 |
. . . 4
 
 
    
            |
27 | 20 | ad2antlr 741 |
. . . . . . 7
    
              |
28 | 6 | ad2antrr 740 |
. . . . . . . 8
    
   DProd     |
29 | 13 | ad2antrr 740 |
. . . . . . . 8
    
 
    |
30 | | simplr 770 |
. . . . . . . 8
    
    |
31 | 28, 29, 30 | dprdub 17736 |
. . . . . . 7
    
       
 DProd 
    |
32 | 27, 31 | eqsstr3d 3453 |
. . . . . 6
    
       DProd      |
33 | | dmdprdsplit2.3 |
. . . . . . . 8
  DProd        DProd       |
34 | 33 | ad2antrr 740 |
. . . . . . 7
    
   DProd       
DProd       |
35 | | eqid 2471 |
. . . . . . . . 9
         |
36 | 35 | dprdssv 17727 |
. . . . . . . 8
 DProd   
     |
37 | | fvres 5893 |
. . . . . . . . . 10
             |
38 | 37 | ad2antrl 742 |
. . . . . . . . 9
    
              |
39 | | dmdprdsplit2.2 |
. . . . . . . . . . 11
  DProd
    |
40 | 39 | ad2antrr 740 |
. . . . . . . . . 10
    
   DProd     |
41 | | ssun2 3589 |
. . . . . . . . . . . . . 14

  |
42 | 41, 1 | syl5sseqr 3467 |
. . . . . . . . . . . . 13

  |
43 | 8, 42 | fssresd 5762 |
. . . . . . . . . . . 12
       SubGrp    |
44 | | fdm 5745 |
. . . . . . . . . . . 12
 
     SubGrp      |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
     |
46 | 45 | ad2antrr 740 |
. . . . . . . . . 10
    
 
    |
47 | | simprl 772 |
. . . . . . . . . 10
    
    |
48 | 40, 46, 47 | dprdub 17736 |
. . . . . . . . 9
    
       
 DProd 
    |
49 | 38, 48 | eqsstr3d 3453 |
. . . . . . . 8
    
       DProd      |
50 | 35, 18 | cntz2ss 17064 |
. . . . . . . 8
   DProd           
 DProd 
       DProd 
             |
51 | 36, 49, 50 | sylancr 676 |
. . . . . . 7
    
     
DProd               |
52 | 34, 51 | sstrd 3428 |
. . . . . 6
    
   DProd              |
53 | 32, 52 | sstrd 3428 |
. . . . 5
    
                |
54 | 53 | exp32 616 |
. . . 4
 
 
    
            |
55 | 26, 54 | jaod 387 |
. . 3
 
  


                |
56 | 5, 55 | sylbid 223 |
. 2
 
 
    
            |
57 | | dprdgrp 17715 |
. . . . . . . 8
  DProd     |
58 | 6, 57 | syl 17 |
. . . . . . 7
   |
59 | 58 | adantr 472 |
. . . . . 6
 
   |
60 | 35 | subgacs 16930 |
. . . . . 6
 SubGrp  ACS        |
61 | | acsmre 15636 |
. . . . . 6
 SubGrp  ACS      SubGrp  Moore        |
62 | 59, 60, 61 | 3syl 18 |
. . . . 5
 
 SubGrp  Moore        |
63 | | difundir 3687 |
. . . . . . . . . . 11
                 |
64 | 2 | difeq1d 3539 |
. . . . . . . . . . 11
 
 
     
     |
65 | | simpr 468 |
. . . . . . . . . . . . . . . 16
 
   |
66 | 65 | snssd 4108 |
. . . . . . . . . . . . . . 15
 
     |
67 | | sslin 3649 |
. . . . . . . . . . . . . . 15
           |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . 14
 
    
    |
69 | | incom 3616 |
. . . . . . . . . . . . . . 15
     |
70 | | dprdsplit.i |
. . . . . . . . . . . . . . . 16
     |
71 | 70 | adantr 472 |
. . . . . . . . . . . . . . 15
 
     |
72 | 69, 71 | syl5eqr 2519 |
. . . . . . . . . . . . . 14
 
     |
73 | | sseq0 3769 |
. . . . . . . . . . . . . 14
        
        |
74 | 68, 72, 73 | syl2anc 673 |
. . . . . . . . . . . . 13
 
       |
75 | | disj3 3813 |
. . . . . . . . . . . . 13
           |
76 | 74, 75 | sylib 201 |
. . . . . . . . . . . 12
 
       |
77 | 76 | uneq2d 3579 |
. . . . . . . . . . 11
 
                   |
78 | 63, 64, 77 | 3eqtr4a 2531 |
. . . . . . . . . 10
 
 
           |
79 | 78 | imaeq2d 5174 |
. . . . . . . . 9
 
                     |
80 | | imaundi 5254 |
. . . . . . . . 9
                         |
81 | 79, 80 | syl6eq 2521 |
. . . . . . . 8
 
                         |
82 | 81 | unieqd 4200 |
. . . . . . 7
 
                           |
83 | | uniun 4209 |
. . . . . . 7
                                |
84 | 82, 83 | syl6eq 2521 |
. . . . . 6
 
                            |
85 | | dmdprdsplit2lem.k |
. . . . . . . . 9
mrCls SubGrp    |
86 | | difss 3549 |
. . . . . . . . . . 11
   
 |
87 | | imass2 5210 |
. . . . . . . . . . 11
                   |
88 | | uniss 4211 |
. . . . . . . . . . 11
                             |
89 | 86, 87, 88 | mp2b 10 |
. . . . . . . . . 10
               |
90 | | imassrn 5185 |
. . . . . . . . . . . 12
     |
91 | | frn 5747 |
. . . . . . . . . . . . . . 15
     SubGrp  SubGrp    |
92 | 8, 91 | syl 17 |
. . . . . . . . . . . . . 14
 SubGrp    |
93 | 92 | adantr 472 |
. . . . . . . . . . . . 13
 
 SubGrp    |
94 | | mresspw 15576 |
. . . . . . . . . . . . . 14
 SubGrp  Moore      SubGrp         |
95 | 62, 94 | syl 17 |
. . . . . . . . . . . . 13
 
 SubGrp         |
96 | 93, 95 | sstrd 3428 |
. . . . . . . . . . . 12
 
        |
97 | 90, 96 | syl5ss 3429 |
. . . . . . . . . . 11
 
            |
98 | | sspwuni 4360 |
. . . . . . . . . . 11
                     |
99 | 97, 98 | sylib 201 |
. . . . . . . . . 10
 
            |
100 | 89, 99 | syl5ss 3429 |
. . . . . . . . 9
 
                |
101 | 62, 85, 100 | mrcssidd 15609 |
. . . . . . . 8
 
                         |
102 | | imassrn 5185 |
. . . . . . . . . . . 12
     |
103 | 102, 96 | syl5ss 3429 |
. . . . . . . . . . 11
 
            |
104 | | sspwuni 4360 |
. . . . . . . . . . 11
                     |
105 | 103, 104 | sylib 201 |
. . . . . . . . . 10
 
            |
106 | 62, 85, 105 | mrcssidd 15609 |
. . . . . . . . 9
 
                 |
107 | 85 | dprdspan 17738 |
. . . . . . . . . . . 12
  DProd    DProd             |
108 | 39, 107 | syl 17 |
. . . . . . . . . . 11
  DProd             |
109 | | df-ima 4852 |
. . . . . . . . . . . . 13
       |
110 | 109 | unieqi 4199 |
. . . . . . . . . . . 12
     
   |
111 | 110 | fveq2i 5882 |
. . . . . . . . . . 11
                 |
112 | 108, 111 | syl6eqr 2523 |
. . . . . . . . . 10
  DProd               |
113 | 112 | adantr 472 |
. . . . . . . . 9
 
  DProd               |
114 | 106, 113 | sseqtr4d 3455 |
. . . . . . . 8
 
      
DProd      |
115 | | unss12 3597 |
. . . . . . . 8
                             
DProd                                    DProd       |
116 | 101, 114,
115 | syl2anc 673 |
. . . . . . 7
 
                
               DProd       |
117 | 85 | mrccl 15595 |
. . . . . . . . 9
  SubGrp  Moore                                 SubGrp    |
118 | 62, 100, 117 | syl2anc 673 |
. . . . . . . 8
 
              SubGrp    |
119 | | dprdsubg 17735 |
. . . . . . . . . 10
  DProd    DProd    SubGrp    |
120 | 39, 119 | syl 17 |
. . . . . . . . 9
  DProd    SubGrp    |
121 | 120 | adantr 472 |
. . . . . . . 8
 
  DProd    SubGrp    |
122 | | eqid 2471 |
. . . . . . . . 9
         |
123 | 122 | lsmunss 17388 |
. . . . . . . 8
               SubGrp   DProd    SubGrp  
               DProd                          DProd       |
124 | 118, 121,
123 | syl2anc 673 |
. . . . . . 7
 
                DProd                          DProd       |
125 | 116, 124 | sstrd 3428 |
. . . . . 6
 
                
                     DProd       |
126 | 84, 125 | eqsstrd 3452 |
. . . . 5
 
                               DProd       |
127 | 89 | a1i 11 |
. . . . . . . . 9
 
                 |
128 | 62, 85, 127, 99 | mrcssd 15608 |
. . . . . . . 8
 
             
           |
129 | 85 | dprdspan 17738 |
. . . . . . . . . . 11
  DProd    DProd             |
130 | 6, 129 | syl 17 |
. . . . . . . . . 10
  DProd             |
131 | | df-ima 4852 |
. . . . . . . . . . . 12
       |
132 | 131 | unieqi 4199 |
. . . . . . . . . . 11
     
   |
133 | 132 | fveq2i 5882 |
. . . . . . . . . 10
                 |
134 | 130, 133 | syl6eqr 2523 |
. . . . . . . . 9
  DProd               |
135 | 134 | adantr 472 |
. . . . . . . 8
 
  DProd               |
136 | 128, 135 | sseqtr4d 3455 |
. . . . . . 7
 
             
 DProd 
    |
137 | 33 | adantr 472 |
. . . . . . 7
 
  DProd   
    DProd       |
138 | 136, 137 | sstrd 3428 |
. . . . . 6
 
             
    DProd       |
139 | 122, 18 | lsmsubg 17384 |
. . . . . 6
               SubGrp   DProd    SubGrp                   DProd                           DProd     SubGrp    |
140 | 118, 121,
138, 139 | syl3anc 1292 |
. . . . 5
 
                      DProd     SubGrp    |
141 | 85 | mrcsscl 15604 |
. . . . 5
  SubGrp  Moore          
                         DProd                          DProd     SubGrp                                     DProd       |
142 | 62, 126, 140, 141 | syl3anc 1292 |
. . . 4
 
             
                     DProd       |
143 | | sslin 3649 |
. . . 4
             
                     DProd    
                                             DProd        |
144 | 142, 143 | syl 17 |
. . 3
 
     
             
                          DProd        |
145 | 10 | sselda 3418 |
. . . . 5
 
   |
146 | 8 | ffvelrnda 6037 |
. . . . 5
 
     SubGrp    |
147 | 145, 146 | syldan 478 |
. . . 4
 
     SubGrp    |
148 | | dmdprdsplit.0 |
. . . 4
     |
149 | 20 | adantl 473 |
. . . . . . . . 9
 
             |
150 | 6 | adantr 472 |
. . . . . . . . . 10
 
  DProd     |
151 | 13 | adantr 472 |
. . . . . . . . . 10
 
 
   |
152 | 150, 151,
65 | dprdub 17736 |
. . . . . . . . 9
 
       
DProd      |
153 | 149, 152 | eqsstr3d 3453 |
. . . . . . . 8
 
      DProd      |
154 | | dprdsubg 17735 |
. . . . . . . . . . 11
  DProd    DProd    SubGrp    |
155 | 6, 154 | syl 17 |
. . . . . . . . . 10
  DProd    SubGrp    |
156 | 155 | adantr 472 |
. . . . . . . . 9
 
  DProd    SubGrp    |
157 | 122 | lsmlub 17393 |
. . . . . . . . 9
      SubGrp               SubGrp   DProd    SubGrp         
DProd                
 DProd 
  
                          DProd       |
158 | 147, 118,
156, 157 | syl3anc 1292 |
. . . . . . . 8
 
        DProd                
 DProd 
  
                          DProd       |
159 | 153, 136,
158 | mpbi2and 935 |
. . . . . . 7
 
                           DProd      |
160 | | ssrin 3648 |
. . . . . . 7
                           DProd                               DProd    
  DProd     DProd       |
161 | 159, 160 | syl 17 |
. . . . . 6
 
                            DProd       DProd
    DProd       |
162 | | dmdprdsplit2.4 |
. . . . . . 7
   DProd     DProd       |
163 | 162 | adantr 472 |
. . . . . 6
 
   DProd
    DProd       |
164 | 161, 163 | sseqtrd 3454 |
. . . . 5
 
                            DProd       |
165 | 122 | lsmub1 17386 |
. . . . . . . . 9
      SubGrp               SubGrp      
                           |
166 | 147, 118,
165 | syl2anc 673 |
. . . . . . . 8
 
                                |
167 | 148 | subg0cl 16903 |
. . . . . . . . 9
     SubGrp 
      |
168 | 147, 167 | syl 17 |
. . . . . . . 8
 
       |
169 | 166, 168 | sseldd 3419 |
. . . . . . 7
 
                            |
170 | 148 | subg0cl 16903 |
. . . . . . . 8
  DProd    SubGrp   DProd      |
171 | 121, 170 | syl 17 |
. . . . . . 7
 
  DProd      |
172 | 169, 171 | elind 3609 |
. . . . . 6
 
                            DProd       |
173 | 172 | snssd 4108 |
. . . . 5
 
                            DProd       |
174 | 164, 173 | eqssd 3435 |
. . . 4
 
                            DProd       |
175 | | resima2 5144 |
. . . . . . . . 9
                         |
176 | 86, 175 | mp1i 13 |
. . . . . . . 8
 
                     |
177 | 176 | unieqd 4200 |
. . . . . . 7
 
                       |
178 | 177 | fveq2d 5883 |
. . . . . 6
 
      
                        |
179 | 149, 178 | ineq12d 3626 |
. . . . 5
 
       
                                     |
180 | 150, 151,
65, 148, 85 | dprddisj 17719 |
. . . . 5
 
       
                  |
181 | 179, 180 | eqtr3d 2507 |
. . . 4
 
     
                |
182 | 8 | adantr 472 |
. . . . . . . 8
 
     SubGrp    |
183 | | ffun 5742 |
. . . . . . . 8
     SubGrp    |
184 | | funiunfv 6171 |
. . . . . . . 8

                     |
185 | 182, 183,
184 | 3syl 18 |
. . . . . . 7
 
                      |
186 | 6 | ad2antrr 740 |
. . . . . . . . . . 11
          DProd     |
187 | 13 | ad2antrr 740 |
. . . . . . . . . . 11
             |
188 | | eldifi 3544 |
. . . . . . . . . . . 12
       |
189 | 188 | adantl 473 |
. . . . . . . . . . 11
           |
190 | | simplr 770 |
. . . . . . . . . . 11
        
  |
191 | | eldifsni 4089 |
. . . . . . . . . . . 12
       |
192 | 191 | adantl 473 |
. . . . . . . . . . 11
           |
193 | 186, 187,
189, 190, 192, 18 | dprdcntz 17718 |
. . . . . . . . . 10
              
            |
194 | | fvres 5893 |
. . . . . . . . . . 11
             |
195 | 189, 194 | syl 17 |
. . . . . . . . . 10
                     |
196 | 20 | ad2antlr 741 |
. . . . . . . . . . 11
                     |
197 | 196 | fveq2d 5883 |
. . . . . . . . . 10
                             |
198 | 193, 195,
197 | 3sstr3d 3460 |
. . . . . . . . 9
            
          |
199 | 198 | ralrimiva 2809 |
. . . . . . . 8
 
                     |
200 | | iunss 4310 |
. . . . . . . 8
 
        
       
                    |
201 | 199, 200 | sylibr 217 |
. . . . . . 7
 
                     |
202 | 185, 201 | eqsstr3d 3453 |
. . . . . 6
 
                    |
203 | 35 | subgss 16896 |
. . . . . . . 8
     SubGrp 
          |
204 | 147, 203 | syl 17 |
. . . . . . 7
 
           |
205 | 35, 18 | cntzsubg 17068 |
. . . . . . 7
                   SubGrp    |
206 | 59, 204, 205 | syl2anc 673 |
. . . . . 6
 
         SubGrp    |
207 | 85 | mrcsscl 15604 |
. . . . . 6
  SubGrp  Moore                               SubGrp               
          |
208 | 62, 202, 206, 207 | syl3anc 1292 |
. . . . 5
 
             
          |
209 | 18, 118, 147, 208 | cntzrecd 17406 |
. . . 4
 
                        |
210 | 122, 147,
118, 121, 148, 174, 181, 18, 209 | lsmdisj3 17411 |
. . 3
 
     
                     DProd        |
211 | 144, 210 | sseqtrd 3454 |
. 2
 
     
             
  |
212 | 56, 211 | jca 541 |
1
 
       
                            
   |