Step | Hyp | Ref
| Expression |
1 | | wrdf 12683 |
. . . . . . . 8
 Word    ..^         |
2 | 1 | ad2antlr 734 |
. . . . . . 7
   Word    DProd  DProd       ..^         |
3 | | fdm 5738 |
. . . . . . 7
    ..^      
 ..^       |
4 | 2, 3 | syl 17 |
. . . . . 6
   Word    DProd  DProd   
 ..^       |
5 | | fzofi 12194 |
. . . . . 6
 ..^      |
6 | 4, 5 | syl6eqel 2539 |
. . . . 5
   Word    DProd  DProd   
  |
7 | 4 | feq2d 5720 |
. . . . . . . . . . 11
   Word    DProd  DProd            ..^          |
8 | 2, 7 | mpbird 236 |
. . . . . . . . . 10
   Word    DProd  DProd          |
9 | 8 | ffvelrnda 6027 |
. . . . . . . . 9
   
Word    DProd 
DProd   
       |
10 | | oveq2 6303 |
. . . . . . . . . . . 12
      ↾s   ↾s        |
11 | 10 | eleq1d 2515 |
. . . . . . . . . . 11
      
↾s  CycGrp
pGrp
 ↾s      CycGrp pGrp    |
12 | | ablfac.c |
. . . . . . . . . . 11
 SubGrp   ↾s  CycGrp pGrp   |
13 | 11, 12 | elrab2 3200 |
. . . . . . . . . 10
    
     SubGrp  
↾s      CycGrp
pGrp    |
14 | 13 | simplbi 462 |
. . . . . . . . 9
         SubGrp    |
15 | 9, 14 | syl 17 |
. . . . . . . 8
   
Word    DProd 
DProd   
     SubGrp    |
16 | | ablfac.b |
. . . . . . . . 9
     |
17 | 16 | subgss 16830 |
. . . . . . . 8
     SubGrp 
      |
18 | 15, 17 | syl 17 |
. . . . . . 7
   
Word    DProd 
DProd   
       |
19 | | inss1 3654 |
. . . . . . . . . . 11
CycGrp pGrp CycGrp |
20 | 13 | simprbi 466 |
. . . . . . . . . . . 12
      ↾s      CycGrp pGrp   |
21 | 9, 20 | syl 17 |
. . . . . . . . . . 11
   
Word    DProd 
DProd   
  ↾s      CycGrp pGrp   |
22 | 19, 21 | sseldi 3432 |
. . . . . . . . . 10
   
Word    DProd 
DProd   
  ↾s      CycGrp |
23 | | eqid 2453 |
. . . . . . . . . . . 12
   
↾s           ↾s        |
24 | | eqid 2453 |
. . . . . . . . . . . 12
.g  ↾s       .g  ↾s        |
25 | 23, 24 | iscyg 17526 |
. . . . . . . . . . 11
  ↾s      CycGrp
  ↾s           ↾s           .g  ↾s              ↾s          |
26 | 25 | simprbi 466 |
. . . . . . . . . 10
  ↾s      CycGrp     
↾s           .g 
↾s              ↾s         |
27 | 22, 26 | syl 17 |
. . . . . . . . 9
   
Word    DProd 
DProd   
      ↾s           .g  ↾s              ↾s         |
28 | | eqid 2453 |
. . . . . . . . . . . 12
 ↾s       ↾s       |
29 | 28 | subgbas 16833 |
. . . . . . . . . . 11
     SubGrp 
        ↾s         |
30 | 15, 29 | syl 17 |
. . . . . . . . . 10
   
Word    DProd 
DProd   
         ↾s         |
31 | 30 | rexeqdv 2996 |
. . . . . . . . 9
   
Word    DProd 
DProd   
       
   .g 
↾s              ↾s      
     ↾s           .g  ↾s              ↾s          |
32 | 27, 31 | mpbird 236 |
. . . . . . . 8
   
Word    DProd 
DProd   
          .g 
↾s              ↾s         |
33 | 15 | ad2antrr 733 |
. . . . . . . . . . . . 13
     
Word    DProd  DProd    
    
     SubGrp    |
34 | | simpr 463 |
. . . . . . . . . . . . 13
     
Word    DProd  DProd    
    
   |
35 | | simplr 763 |
. . . . . . . . . . . . 13
     
Word    DProd  DProd    
    
       |
36 | | ablfac2.m |
. . . . . . . . . . . . . 14
.g   |
37 | 36, 28, 24 | subgmulg 16843 |
. . . . . . . . . . . . 13
      SubGrp       
   .g 
↾s           |
38 | 33, 34, 35, 37 | syl3anc 1269 |
. . . . . . . . . . . 12
     
Word    DProd  DProd    
    
     .g  ↾s           |
39 | 38 | mpteq2dva 4492 |
. . . . . . . . . . 11
     Word    DProd  DProd    
      
     .g  ↾s            |
40 | 39 | rneqd 5065 |
. . . . . . . . . 10
     Word    DProd  DProd    
      
     .g  ↾s            |
41 | 30 | adantr 467 |
. . . . . . . . . 10
     Word    DProd  DProd    
            
↾s         |
42 | 40, 41 | eqeq12d 2468 |
. . . . . . . . 9
     Word    DProd  DProd    
     
           .g 
↾s              ↾s          |
43 | 42 | rexbidva 2900 |
. . . . . . . 8
   
Word    DProd 
DProd   
       
                 .g 
↾s              ↾s          |
44 | 32, 43 | mpbird 236 |
. . . . . . 7
   
Word    DProd 
DProd   
                 |
45 | | ssrexv 3496 |
. . . . . . 7
      
      
      
 
         |
46 | 18, 44, 45 | sylc 62 |
. . . . . 6
   
Word    DProd 
DProd   
   
        |
47 | 46 | ralrimiva 2804 |
. . . . 5
   Word    DProd  DProd      
          |
48 | | oveq2 6303 |
. . . . . . . . 9
     
         |
49 | 48 | mpteq2dv 4493 |
. . . . . . . 8
                   |
50 | 49 | rneqd 5065 |
. . . . . . 7
     

            |
51 | 50 | eqeq1d 2455 |
. . . . . 6
       
     
               |
52 | 51 | ac6sfi 7820 |
. . . . 5
      
                               |
53 | 6, 47, 52 | syl2anc 667 |
. . . 4
   Word    DProd  DProd                            |
54 | | simprl 765 |
. . . . . . . . 9
   
Word    DProd 
DProd                        
      |
55 | 4 | adantr 467 |
. . . . . . . . . 10
   
Word    DProd 
DProd                        
 ..^       |
56 | 55 | feq2d 5720 |
. . . . . . . . 9
   
Word    DProd 
DProd                        
    
   ..^          |
57 | 54, 56 | mpbid 214 |
. . . . . . . 8
   
Word    DProd 
DProd                        
   ..^         |
58 | | iswrdi 12682 |
. . . . . . . 8
    ..^       Word   |
59 | 57, 58 | syl 17 |
. . . . . . 7
   
Word    DProd 
DProd                        
Word   |
60 | | fdm 5738 |
. . . . . . . . . . . . . 14
    ..^      
 ..^       |
61 | 57, 60 | syl 17 |
. . . . . . . . . . . . 13
   
Word    DProd 
DProd                        
 ..^       |
62 | 61, 55 | eqtr4d 2490 |
. . . . . . . . . . . 12
   
Word    DProd 
DProd                        
  |
63 | 62 | eleq2d 2516 |
. . . . . . . . . . 11
   
Word    DProd 
DProd                        

   |
64 | 63 | biimpa 487 |
. . . . . . . . . 10
     Word    DProd  DProd                            |
65 | | simprr 767 |
. . . . . . . . . . . 12
   
Word    DProd 
DProd                        
                |
66 | | simpl 459 |
. . . . . . . . . . . . . . . . . 18
 
   |
67 | 66 | fveq2d 5874 |
. . . . . . . . . . . . . . . . 17
 
           |
68 | 67 | oveq2d 6311 |
. . . . . . . . . . . . . . . 16
 
               |
69 | 68 | mpteq2dva 4492 |
. . . . . . . . . . . . . . 15
                   |
70 | 69 | rneqd 5065 |
. . . . . . . . . . . . . 14
 

                |
71 | | fveq2 5870 |
. . . . . . . . . . . . . 14
           |
72 | 70, 71 | eqeq12d 2468 |
. . . . . . . . . . . . 13
   
         
               |
73 | 72 | rspccva 3151 |
. . . . . . . . . . . 12
               
 

            |
74 | 65, 73 | sylan 474 |
. . . . . . . . . . 11
     Word    DProd  DProd                           
            |
75 | 8 | adantr 467 |
. . . . . . . . . . . 12
   
Word    DProd 
DProd                        
      |
76 | 75 | ffvelrnda 6027 |
. . . . . . . . . . 11
     Word    DProd  DProd                                |
77 | 74, 76 | eqeltrd 2531 |
. . . . . . . . . 10
     Word    DProd  DProd                           
        |
78 | 64, 77 | syldan 473 |
. . . . . . . . 9
     Word    DProd  DProd                           
        |
79 | | ablfac2.s |
. . . . . . . . . 10

          |
80 | | fveq2 5870 |
. . . . . . . . . . . . . 14
           |
81 | 80 | oveq2d 6311 |
. . . . . . . . . . . . 13
 
             |
82 | 81 | mpteq2dv 4493 |
. . . . . . . . . . . 12
                   |
83 | 82 | rneqd 5065 |
. . . . . . . . . . 11
 

                |
84 | 83 | cbvmptv 4498 |
. . . . . . . . . 10
  
                  |
85 | 79, 84 | eqtri 2475 |
. . . . . . . . 9

          |
86 | 78, 85 | fmptd 6051 |
. . . . . . . 8
   
Word    DProd 
DProd                        
      |
87 | | simprl 765 |
. . . . . . . . . 10
   Word    DProd  DProd     DProd   |
88 | 87 | adantr 467 |
. . . . . . . . 9
   
Word    DProd 
DProd                        
 DProd   |
89 | 62 | raleqdv 2995 |
. . . . . . . . . . . . 13
   
Word    DProd 
DProd                        
 
  
         
                 |
90 | 65, 89 | mpbird 236 |
. . . . . . . . . . . 12
   
Word    DProd 
DProd                        
                |
91 | | mpteq12 4485 |
. . . . . . . . . . . 12
                                   |
92 | 62, 90, 91 | syl2anc 667 |
. . . . . . . . . . 11
   
Word    DProd 
DProd                        
                  |
93 | 79, 92 | syl5eq 2499 |
. . . . . . . . . 10
   
Word    DProd 
DProd                        
        |
94 | | dprdf 17650 |
. . . . . . . . . . . 12
  DProd     SubGrp    |
95 | 88, 94 | syl 17 |
. . . . . . . . . . 11
   
Word    DProd 
DProd                        
    SubGrp    |
96 | 95 | feqmptd 5923 |
. . . . . . . . . 10
   
Word    DProd 
DProd                        
        |
97 | 93, 96 | eqtr4d 2490 |
. . . . . . . . 9
   
Word    DProd 
DProd                        
  |
98 | 88, 97 | breqtrrd 4432 |
. . . . . . . 8
   
Word    DProd 
DProd                        
 DProd   |
99 | 97 | oveq2d 6311 |
. . . . . . . . 9
   
Word    DProd 
DProd                        
 DProd   DProd    |
100 | | simplrr 772 |
. . . . . . . . 9
   
Word    DProd 
DProd                        
 DProd    |
101 | 99, 100 | eqtrd 2487 |
. . . . . . . 8
   
Word    DProd 
DProd                        
 DProd    |
102 | 86, 98, 101 | 3jca 1189 |
. . . . . . 7
   
Word    DProd 
DProd                        
      DProd
 DProd     |
103 | 59, 102 | jca 535 |
. . . . . 6
   
Word    DProd 
DProd                        
 Word       DProd
 DProd      |
104 | 103 | ex 436 |
. . . . 5
   Word    DProd  DProd                          Word       DProd  DProd       |
105 | 104 | eximdv 1766 |
. . . 4
   Word    DProd  DProd               
              Word       DProd
 DProd       |
106 | 53, 105 | mpd 15 |
. . 3
   Word    DProd  DProd       Word       DProd  DProd      |
107 | | df-rex 2745 |
. . 3
  Word        DProd 
DProd  
   Word       DProd  DProd      |
108 | 106, 107 | sylibr 216 |
. 2
   Word    DProd  DProd     Word        DProd  DProd     |
109 | | ablfac.1 |
. . 3
   |
110 | | ablfac.2 |
. . 3
   |
111 | 16, 12, 109, 110 | ablfac 17733 |
. 2
  Word    DProd 
DProd     |
112 | 108, 111 | r19.29a 2934 |
1
  Word        DProd  DProd     |