Step | Hyp | Ref
| Expression |
1 | | dprdres.1 |
. . . 4
  DProd
  |
2 | | dprdgrp 17630 |
. . . 4
  DProd
  |
3 | 1, 2 | syl 17 |
. . 3
   |
4 | | dprdres.2 |
. . . . 5
   |
5 | 1, 4 | dprdf2 17632 |
. . . 4
     SubGrp    |
6 | | dprdres.3 |
. . . 4

  |
7 | 5, 6 | fssresd 5748 |
. . 3
       SubGrp    |
8 | 1 | ad2antrr 731 |
. . . . . . . 8
          DProd   |
9 | 4 | ad2antrr 731 |
. . . . . . . 8
        
  |
10 | 6 | ad2antrr 731 |
. . . . . . . . 9
           |
11 | | simplr 761 |
. . . . . . . . 9
           |
12 | 10, 11 | sseldd 3432 |
. . . . . . . 8
           |
13 | | eldifi 3554 |
. . . . . . . . . 10
       |
14 | 13 | adantl 468 |
. . . . . . . . 9
           |
15 | 10, 14 | sseldd 3432 |
. . . . . . . 8
           |
16 | | eldifsni 4097 |
. . . . . . . . . 10
       |
17 | 16 | adantl 468 |
. . . . . . . . 9
           |
18 | 17 | necomd 2678 |
. . . . . . . 8
           |
19 | | eqid 2450 |
. . . . . . . 8
Cntz  Cntz   |
20 | 8, 9, 12, 15, 18, 19 | dprdcntz 17633 |
. . . . . . 7
              Cntz           |
21 | | fvres 5877 |
. . . . . . . 8
             |
22 | 11, 21 | syl 17 |
. . . . . . 7
                     |
23 | | fvres 5877 |
. . . . . . . . 9
             |
24 | 14, 23 | syl 17 |
. . . . . . . 8
                     |
25 | 24 | fveq2d 5867 |
. . . . . . 7
          Cntz            Cntz           |
26 | 20, 22, 25 | 3sstr4d 3474 |
. . . . . 6
              
 Cntz             |
27 | 26 | ralrimiva 2801 |
. . . . 5
 
              Cntz             |
28 | 21 | adantl 468 |
. . . . . . 7
 
             |
29 | 28 | ineq1d 3632 |
. . . . . 6
 
       
 mrCls SubGrp       
                mrCls SubGrp                    |
30 | | eqid 2450 |
. . . . . . . . . . . . 13
         |
31 | 30 | subgacs 16845 |
. . . . . . . . . . . 12
 SubGrp  ACS        |
32 | | acsmre 15551 |
. . . . . . . . . . . 12
 SubGrp  ACS      SubGrp  Moore        |
33 | 3, 31, 32 | 3syl 18 |
. . . . . . . . . . 11
 SubGrp  Moore        |
34 | 33 | adantr 467 |
. . . . . . . . . 10
 
 SubGrp  Moore        |
35 | | eqid 2450 |
. . . . . . . . . 10
mrCls SubGrp   mrCls SubGrp    |
36 | | resss 5127 |
. . . . . . . . . . . . 13
   |
37 | | imass1 5202 |
. . . . . . . . . . . . 13
 

                    |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . . . . 12
 
       
         |
39 | 6 | adantr 467 |
. . . . . . . . . . . . 13
 
   |
40 | | ssdif 3567 |
. . . . . . . . . . . . 13
    
      |
41 | | imass2 5203 |
. . . . . . . . . . . . 13
     
          
          |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . . . 12
 
        
          |
43 | 38, 42 | syl5ss 3442 |
. . . . . . . . . . 11
 
          
          |
44 | 43 | unissd 4221 |
. . . . . . . . . 10
 
           
           |
45 | | imassrn 5178 |
. . . . . . . . . . . 12
       
 |
46 | | frn 5733 |
. . . . . . . . . . . . . . 15
     SubGrp  SubGrp    |
47 | 5, 46 | syl 17 |
. . . . . . . . . . . . . 14
 SubGrp    |
48 | 30 | subgss 16811 |
. . . . . . . . . . . . . . . 16
 SubGrp 
      |
49 | | selpw 3957 |
. . . . . . . . . . . . . . . 16
     
      |
50 | 48, 49 | sylibr 216 |
. . . . . . . . . . . . . . 15
 SubGrp 
       |
51 | 50 | ssriv 3435 |
. . . . . . . . . . . . . 14
SubGrp        |
52 | 47, 51 | syl6ss 3443 |
. . . . . . . . . . . . 13
        |
53 | 52 | adantr 467 |
. . . . . . . . . . . 12
 
        |
54 | 45, 53 | syl5ss 3442 |
. . . . . . . . . . 11
 
        
       |
55 | | sspwuni 4366 |
. . . . . . . . . . 11
                  
          |
56 | 54, 55 | sylib 200 |
. . . . . . . . . 10
 
         
      |
57 | 34, 35, 44, 56 | mrcssd 15523 |
. . . . . . . . 9
 
  mrCls SubGrp                  mrCls SubGrp                 |
58 | | sslin 3657 |
. . . . . . . . 9
  mrCls SubGrp                  mrCls SubGrp                     mrCls SubGrp                        mrCls SubGrp         
        |
59 | 57, 58 | syl 17 |
. . . . . . . 8
 
     
 mrCls SubGrp       
                mrCls SubGrp                  |
60 | 1 | adantr 467 |
. . . . . . . . 9
 
  DProd   |
61 | 4 | adantr 467 |
. . . . . . . . 9
 
   |
62 | 6 | sselda 3431 |
. . . . . . . . 9
 
   |
63 | | eqid 2450 |
. . . . . . . . 9
         |
64 | 60, 61, 62, 63, 35 | dprddisj 17634 |
. . . . . . . 8
 
     
 mrCls SubGrp                        |
65 | 59, 64 | sseqtrd 3467 |
. . . . . . 7
 
     
 mrCls SubGrp       
                  |
66 | 5 | ffvelrnda 6020 |
. . . . . . . . . . 11
 
     SubGrp    |
67 | 62, 66 | syldan 473 |
. . . . . . . . . 10
 
     SubGrp    |
68 | 63 | subg0cl 16818 |
. . . . . . . . . 10
     SubGrp 
          |
69 | 67, 68 | syl 17 |
. . . . . . . . 9
 
           |
70 | 44, 56 | sstrd 3441 |
. . . . . . . . . . 11
 
           
      |
71 | 35 | mrccl 15510 |
. . . . . . . . . . 11
  SubGrp  Moore                       mrCls SubGrp       
         SubGrp    |
72 | 34, 70, 71 | syl2anc 666 |
. . . . . . . . . 10
 
  mrCls SubGrp                 SubGrp    |
73 | 63 | subg0cl 16818 |
. . . . . . . . . 10
  mrCls SubGrp                 SubGrp       mrCls SubGrp       
           |
74 | 72, 73 | syl 17 |
. . . . . . . . 9
 
      mrCls SubGrp                   |
75 | 69, 74 | elind 3617 |
. . . . . . . 8
 
           mrCls SubGrp                    |
76 | 75 | snssd 4116 |
. . . . . . 7
 
      
      mrCls SubGrp                    |
77 | 65, 76 | eqssd 3448 |
. . . . . 6
 
     
 mrCls SubGrp       
                  |
78 | 29, 77 | eqtrd 2484 |
. . . . 5
 
       
 mrCls SubGrp       
                  |
79 | 27, 78 | jca 535 |
. . . 4
 
  
          
 Cntz             
     mrCls SubGrp                           |
80 | 79 | ralrimiva 2801 |
. . 3
          
     Cntz                 
 mrCls SubGrp       
                   |
81 | 1, 4 | dprddomcld 17626 |
. . . . 5
   |
82 | 81, 6 | ssexd 4549 |
. . . 4
   |
83 | | fdm 5731 |
. . . . 5
 
     SubGrp      |
84 | 7, 83 | syl 17 |
. . . 4
     |
85 | 19, 63, 35 | dmdprd 17623 |
. . . 4
       DProd  
       SubGrp           
     Cntz                 
 mrCls SubGrp       
                     |
86 | 82, 84, 85 | syl2anc 666 |
. . 3
   DProd  
       SubGrp           
     Cntz                 
 mrCls SubGrp       
                     |
87 | 3, 7, 80, 86 | mpbir3and 1190 |
. 2
  DProd
    |
88 | | rnss 5062 |
. . . . . 6
 

    |
89 | | uniss 4218 |
. . . . . 6
  
      |
90 | 36, 88, 89 | mp2b 10 |
. . . . 5
 
   |
91 | 90 | a1i 11 |
. . . 4
       |
92 | | sspwuni 4366 |
. . . . 5

    
       |
93 | 52, 92 | sylib 200 |
. . . 4
        |
94 | 33, 35, 91, 93 | mrcssd 15523 |
. . 3
  mrCls SubGrp          mrCls SubGrp         |
95 | 35 | dprdspan 17653 |
. . . 4
  DProd    DProd     mrCls SubGrp           |
96 | 87, 95 | syl 17 |
. . 3
  DProd     mrCls SubGrp           |
97 | 35 | dprdspan 17653 |
. . . 4
  DProd
 DProd   mrCls SubGrp         |
98 | 1, 97 | syl 17 |
. . 3
  DProd   mrCls SubGrp         |
99 | 94, 96, 98 | 3sstr4d 3474 |
. 2
  DProd    
DProd    |
100 | 87, 99 | jca 535 |
1
   DProd    DProd   
 DProd     |