Step | Hyp | Ref
| Expression |
1 | | fzfid 11913 |
. . . 4
           |
2 | | ablfac.a |
. . . . 5
       |
3 | | prmnn 13885 |
. . . . . . . 8

  |
4 | 3 | 3ad2ant2 1010 |
. . . . . . 7
 
       |
5 | | prmz 13886 |
. . . . . . . . 9

  |
6 | | ablfac.1 |
. . . . . . . . . . 11
   |
7 | | ablgrp 16404 |
. . . . . . . . . . 11

  |
8 | | ablfac.b |
. . . . . . . . . . . 12
     |
9 | 8 | grpbn0 15687 |
. . . . . . . . . . 11
   |
10 | 6, 7, 9 | 3syl 20 |
. . . . . . . . . 10
   |
11 | | ablfac.2 |
. . . . . . . . . . 11
   |
12 | | hashnncl 12252 |
. . . . . . . . . . 11
     
   |
13 | 11, 12 | syl 16 |
. . . . . . . . . 10
     
   |
14 | 10, 13 | mpbird 232 |
. . . . . . . . 9
       |
15 | | dvdsle 13697 |
. . . . . . . . 9
                   |
16 | 5, 14, 15 | syl2anr 478 |
. . . . . . . 8
 

    
       |
17 | 16 | 3impia 1185 |
. . . . . . 7
 
           |
18 | 14 | nnzd 10858 |
. . . . . . . . 9
       |
19 | 18 | 3ad2ant1 1009 |
. . . . . . . 8
 
           |
20 | | fznn 11644 |
. . . . . . . 8
    
         
        |
21 | 19, 20 | syl 16 |
. . . . . . 7
 
              
        |
22 | 4, 17, 21 | mpbir2and 913 |
. . . . . 6
 
               |
23 | 22 | rabssdv 3541 |
. . . . 5
                 |
24 | 2, 23 | syl5eqss 3509 |
. . . 4

          |
25 | | ssfi 7645 |
. . . 4
                  
  |
26 | 1, 24, 25 | syl2anc 661 |
. . 3
   |
27 | | dfin5 3445 |
. . . . . . . 8
Word           Word
          |
28 | | ablfac.o |
. . . . . . . . . . . . . 14
     |
29 | | ablfac.s |
. . . . . . . . . . . . . 14
                   |
30 | | ssrab2 3546 |
. . . . . . . . . . . . . . . 16
     
 |
31 | 2, 30 | eqsstri 3495 |
. . . . . . . . . . . . . . 15
 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14

  |
33 | 8, 28, 29, 6, 11, 32 | ablfac1b 16694 |
. . . . . . . . . . . . 13
  DProd
  |
34 | | fvex 5810 |
. . . . . . . . . . . . . . . . 17
     |
35 | 8, 34 | eqeltri 2538 |
. . . . . . . . . . . . . . . 16
 |
36 | 35 | rabex 4552 |
. . . . . . . . . . . . . . 15

       
        |
37 | 36, 29 | dmmpti 5649 |
. . . . . . . . . . . . . 14
 |
38 | 37 | a1i 11 |
. . . . . . . . . . . . 13
   |
39 | 33, 38 | dprdf2 16614 |
. . . . . . . . . . . 12
     SubGrp    |
40 | 39 | ffvelrnda 5953 |
. . . . . . . . . . 11
 
     SubGrp    |
41 | | ablfac.c |
. . . . . . . . . . . 12
 SubGrp   ↾s  CycGrp pGrp   |
42 | | ablfac.w |
. . . . . . . . . . . 12
 SubGrp   Word   DProd

DProd      |
43 | 8, 41, 6, 11, 28, 2, 29, 42 | ablfaclem1 16709 |
. . . . . . . . . . 11
     SubGrp 
         Word
  DProd 
DProd          |
44 | 40, 43 | syl 16 |
. . . . . . . . . 10
 
          Word   DProd  DProd          |
45 | | ssrab2 3546 |
. . . . . . . . . 10
 Word   DProd

DProd        Word  |
46 | 44, 45 | syl6eqss 3515 |
. . . . . . . . 9
 
         Word   |
47 | | dfss1 3664 |
. . . . . . . . 9
         Word
Word
                   |
48 | 46, 47 | sylib 196 |
. . . . . . . 8
 
 Word                    |
49 | 27, 48 | syl5eqr 2509 |
. . . . . . 7
 
  Word                    |
50 | 49, 44 | eqtrd 2495 |
. . . . . 6
 
  Word           Word
  DProd 
DProd          |
51 | | eqid 2454 |
. . . . . . . . 9
   
↾s           ↾s        |
52 | | eqid 2454 |
. . . . . . . . 9
 SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp   SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp   |
53 | 6 | adantr 465 |
. . . . . . . . . 10
 
   |
54 | | eqid 2454 |
. . . . . . . . . . 11
 ↾s       ↾s       |
55 | 54 | subgabl 16442 |
. . . . . . . . . 10
      SubGrp  
 ↾s        |
56 | 53, 40, 55 | syl2anc 661 |
. . . . . . . . 9
 
  ↾s        |
57 | 32 | sselda 3465 |
. . . . . . . . . 10
 
   |
58 | 54 | subgbas 15805 |
. . . . . . . . . . . . . 14
     SubGrp 
        ↾s         |
59 | 40, 58 | syl 16 |
. . . . . . . . . . . . 13
 
         ↾s         |
60 | 59 | fveq2d 5804 |
. . . . . . . . . . . 12
 
                ↾s          |
61 | 8, 28, 29, 6, 11, 32 | ablfac1a 16693 |
. . . . . . . . . . . 12
 
            
        |
62 | 60, 61 | eqtr3d 2497 |
. . . . . . . . . . 11
 
        ↾s           
        |
63 | 62 | oveq2d 6217 |
. . . . . . . . . . . . 13
 
 
       ↾s                       |
64 | 14 | adantr 465 |
. . . . . . . . . . . . . . . 16
 
       |
65 | 57, 64 | pccld 14036 |
. . . . . . . . . . . . . . 15
 
 
       |
66 | 65 | nn0zd 10857 |
. . . . . . . . . . . . . 14
 
 
       |
67 | | pcid 14058 |
. . . . . . . . . . . . . 14
  
                          |
68 | 57, 66, 67 | syl2anc 661 |
. . . . . . . . . . . . 13
 
 
                   |
69 | 63, 68 | eqtrd 2495 |
. . . . . . . . . . . 12
 
 
       ↾s                 |
70 | 69 | oveq2d 6217 |
. . . . . . . . . . 11
 
            ↾s                      |
71 | 62, 70 | eqtr4d 2498 |
. . . . . . . . . 10
 
        ↾s           
       ↾s            |
72 | 54 | subggrp 15804 |
. . . . . . . . . . . 12
     SubGrp 
 ↾s        |
73 | 40, 72 | syl 16 |
. . . . . . . . . . 11
 
  ↾s        |
74 | 11 | adantr 465 |
. . . . . . . . . . . . 13
 
   |
75 | 8 | subgss 15802 |
. . . . . . . . . . . . . 14
     SubGrp 
      |
76 | 40, 75 | syl 16 |
. . . . . . . . . . . . 13
 
       |
77 | | ssfi 7645 |
. . . . . . . . . . . . 13
             |
78 | 74, 76, 77 | syl2anc 661 |
. . . . . . . . . . . 12
 
       |
79 | 59, 78 | eqeltrrd 2543 |
. . . . . . . . . . 11
 
     ↾s         |
80 | 51 | pgpfi2 16227 |
. . . . . . . . . . 11
  
↾s     
   
↾s         pGrp  ↾s              ↾s                   ↾s              |
81 | 73, 79, 80 | syl2anc 661 |
. . . . . . . . . 10
 
  pGrp  ↾s              ↾s                   ↾s              |
82 | 57, 71, 81 | mpbir2and 913 |
. . . . . . . . 9
 
 pGrp 
↾s        |
83 | 51, 52, 56, 82, 79 | pgpfac 16708 |
. . . . . . . 8
 
  Word  SubGrp 
↾s         ↾s      ↾s  CycGrp pGrp   
↾s       DProd   ↾s      DProd      ↾s          |
84 | | ssrab2 3546 |
. . . . . . . . . . . . . 14
 SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
SubGrp  ↾s        |
85 | | sswrd 12361 |
. . . . . . . . . . . . . 14
  SubGrp 
↾s         ↾s      ↾s  CycGrp pGrp  SubGrp  ↾s      
Word  SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
Word SubGrp  ↾s         |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . . . . 13
Word  SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
Word SubGrp  ↾s        |
87 | 86 | sseli 3461 |
. . . . . . . . . . . 12
 Word  SubGrp 
↾s         ↾s      ↾s  CycGrp pGrp  Word SubGrp  ↾s         |
88 | 40 | adantr 465 |
. . . . . . . . . . . . . . . . . 18
    Word SubGrp  ↾s            SubGrp    |
89 | 88 | adantr 465 |
. . . . . . . . . . . . . . . . 17
   

Word SubGrp 
↾s         ↾s       DProd
     SubGrp    |
90 | 54 | subgdmdprd 16654 |
. . . . . . . . . . . . . . . . . . 19
     SubGrp 
  ↾s       DProd
  DProd          |
91 | 88, 90 | syl 16 |
. . . . . . . . . . . . . . . . . 18
    Word SubGrp  ↾s          ↾s       DProd
  DProd          |
92 | 91 | simprbda 623 |
. . . . . . . . . . . . . . . . 17
   

Word SubGrp 
↾s         ↾s       DProd
  DProd
  |
93 | 91 | simplbda 624 |
. . . . . . . . . . . . . . . . 17
   

Word SubGrp 
↾s         ↾s       DProd
        |
94 | 54, 89, 92, 93 | subgdprd 16655 |
. . . . . . . . . . . . . . . 16
   

Word SubGrp 
↾s         ↾s       DProd
   ↾s      DProd   DProd    |
95 | 59 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
   

Word SubGrp 
↾s         ↾s       DProd
        
↾s         |
96 | 95 | eqcomd 2462 |
. . . . . . . . . . . . . . . 16
   

Word SubGrp 
↾s         ↾s       DProd
     ↾s             |
97 | 94, 96 | eqeq12d 2476 |
. . . . . . . . . . . . . . 15
   

Word SubGrp 
↾s         ↾s       DProd
    ↾s      DProd      ↾s      
 DProd         |
98 | 97 | biimpd 207 |
. . . . . . . . . . . . . 14
   

Word SubGrp 
↾s         ↾s       DProd
    ↾s      DProd      ↾s        DProd         |
99 | 98, 92 | jctild 543 |
. . . . . . . . . . . . 13
   

Word SubGrp 
↾s         ↾s       DProd
    ↾s      DProd      ↾s         DProd  DProd          |
100 | 99 | expimpd 603 |
. . . . . . . . . . . 12
    Word SubGrp  ↾s           ↾s       DProd
  ↾s      DProd      ↾s          DProd 
DProd          |
101 | 87, 100 | sylan2 474 |
. . . . . . . . . . 11
    Word  SubGrp 
↾s         ↾s      ↾s  CycGrp pGrp      ↾s       DProd   ↾s      DProd      ↾s          DProd 
DProd          |
102 | | oveq2 6209 |
. . . . . . . . . . . . . . . 16
  
↾s      ↾s    ↾s      ↾s    |
103 | 102 | eleq1d 2523 |
. . . . . . . . . . . . . . 15
    ↾s      ↾s  CycGrp pGrp   ↾s      ↾s  CycGrp pGrp    |
104 | 103 | cbvrabv 3077 |
. . . . . . . . . . . . . 14
 SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp   SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp   |
105 | 54 | subsubg 15824 |
. . . . . . . . . . . . . . . . . . 19
     SubGrp 
 SubGrp  ↾s      
 SubGrp 
        |
106 | 40, 105 | syl 16 |
. . . . . . . . . . . . . . . . . 18
 
  SubGrp 
↾s        SubGrp          |
107 | 106 | simprbda 623 |
. . . . . . . . . . . . . . . . 17
    SubGrp  ↾s        SubGrp    |
108 | 107 | 3adant3 1008 |
. . . . . . . . . . . . . . . 16
    SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
SubGrp    |
109 | 40 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . . . . 18
    SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
    SubGrp    |
110 | 106 | simplbda 624 |
. . . . . . . . . . . . . . . . . . 19
    SubGrp  ↾s       
      |
111 | 110 | 3adant3 1008 |
. . . . . . . . . . . . . . . . . 18
    SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
      |
112 | | ressabs 14356 |
. . . . . . . . . . . . . . . . . 18
      SubGrp        
↾s      ↾s   ↾s    |
113 | 109, 111,
112 | syl2anc 661 |
. . . . . . . . . . . . . . . . 17
    SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
  ↾s      ↾s   ↾s    |
114 | | simp3 990 |
. . . . . . . . . . . . . . . . 17
    SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
  ↾s      ↾s  CycGrp pGrp   |
115 | 113, 114 | eqeltrrd 2543 |
. . . . . . . . . . . . . . . 16
    SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
 ↾s  CycGrp pGrp   |
116 | | oveq2 6209 |
. . . . . . . . . . . . . . . . . 18
  ↾s   ↾s    |
117 | 116 | eleq1d 2523 |
. . . . . . . . . . . . . . . . 17
  
↾s  CycGrp
pGrp
 ↾s  CycGrp pGrp    |
118 | 117, 41 | elrab2 3226 |
. . . . . . . . . . . . . . . 16

 SubGrp  
↾s  CycGrp
pGrp    |
119 | 108, 115,
118 | sylanbrc 664 |
. . . . . . . . . . . . . . 15
    SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
  |
120 | 119 | rabssdv 3541 |
. . . . . . . . . . . . . 14
 
  SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
  |
121 | 104, 120 | syl5eqss 3509 |
. . . . . . . . . . . . 13
 
  SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
  |
122 | | sswrd 12361 |
. . . . . . . . . . . . 13
  SubGrp 
↾s         ↾s      ↾s  CycGrp pGrp  Word  SubGrp 
↾s         ↾s      ↾s  CycGrp pGrp  Word   |
123 | 121, 122 | syl 16 |
. . . . . . . . . . . 12
 
 Word  SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp 
Word   |
124 | 123 | sselda 3465 |
. . . . . . . . . . 11
    Word  SubGrp 
↾s         ↾s      ↾s  CycGrp pGrp   Word   |
125 | 101, 124 | jctild 543 |
. . . . . . . . . 10
    Word  SubGrp 
↾s         ↾s      ↾s  CycGrp pGrp      ↾s       DProd   ↾s      DProd      ↾s         Word   DProd 
DProd           |
126 | 125 | expimpd 603 |
. . . . . . . . 9
 
   Word  SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp    ↾s       DProd   ↾s      DProd      ↾s          Word   DProd  DProd           |
127 | 126 | reximdv2 2931 |
. . . . . . . 8
 
  
Word  SubGrp  ↾s        
↾s      ↾s  CycGrp pGrp    ↾s       DProd
  ↾s      DProd      ↾s        
Word    DProd

DProd          |
128 | 83, 127 | mpd 15 |
. . . . . . 7
 
  Word    DProd  DProd         |
129 | | rabn0 3766 |
. . . . . . 7
  Word   DProd 
DProd         Word    DProd 
DProd         |
130 | 128, 129 | sylibr 212 |
. . . . . 6
 
  Word   DProd

DProd          |
131 | 50, 130 | eqnetrd 2745 |
. . . . 5
 
  Word            |
132 | | rabn0 3766 |
. . . . 5
  Word           Word            |
133 | 131, 132 | sylib 196 |
. . . 4
 
  Word            |
134 | 133 | ralrimiva 2830 |
. . 3
  
Word            |
135 | | eleq1 2526 |
. . . 4
             
               |
136 | 135 | ac6sfi 7668 |
. . 3
   
Word                 Word                 |
137 | 26, 134, 136 | syl2anc 661 |
. 2
       Word
                |
138 | | sneq 3996 |
. . . . . . . . 9
       |
139 | | fveq2 5800 |
. . . . . . . . . 10
           |
140 | 139 | dmeqd 5151 |
. . . . . . . . 9
           |
141 | 138, 140 | xpeq12d 4974 |
. . . . . . . 8
                   |
142 | 141 | cbviunv 4318 |
. . . . . . 7

        
         |
143 | 26 | adantr 465 |
. . . . . . . 8
 
    Word

                |
144 | | snfi 7501 |
. . . . . . . . . 10
   |
145 | | simprl 755 |
. . . . . . . . . . . . 13
 
    Word

                 Word   |
146 | 145 | ffvelrnda 5953 |
. . . . . . . . . . . 12
       Word
              
     Word
  |
147 | | wrdf 12359 |
. . . . . . . . . . . 12
     Word        ..^             |
148 | | fdm 5672 |
. . . . . . . . . . . 12
        ..^          
     ..^           |
149 | 146, 147,
148 | 3syl 20 |
. . . . . . . . . . 11
       Word
              
      ..^           |
150 | | fzofi 11914 |
. . . . . . . . . . 11
 ..^          |
151 | 149, 150 | syl6eqel 2550 |
. . . . . . . . . 10
       Word
              
       |
152 | | xpfi 7695 |
. . . . . . . . . 10
                   |
153 | 144, 151,
152 | sylancr 663 |
. . . . . . . . 9
       Word
              
           |
154 | 153 | ralrimiva 2830 |
. . . . . . . 8
 
    Word

              
          |
155 | | iunfi 7711 |
. . . . . . . 8
                       |
156 | 143, 154,
155 | syl2anc 661 |
. . . . . . 7
 
    Word

              
          |
157 | 142, 156 | syl5eqel 2546 |
. . . . . 6
 
    Word

              
          |
158 | | hashcl 12244 |
. . . . . 6
 
           
           |
159 | | hashfzo0 12310 |
. . . . . 6
                  ..^   
                          |
160 | 157, 158,
159 | 3syl 20 |
. . . . 5
 
    Word

                  ..^                  
           |
161 | | fzofi 11914 |
. . . . . 6
 ..^   
           |
162 | | hashen 12236 |
. . . . . 6
   ..^              
              ..^                           
 ..^   
                      |
163 | 161, 157,
162 | sylancr 663 |
. . . . 5
 
    Word

                   ..^   
                       
 ..^   
                      |
164 | 160, 163 | mpbid 210 |
. . . 4
 
    Word

               ..^   
                     |
165 | | bren 7430 |
. . . 4
  ..^   
                  
    ..^                
          |
166 | 164, 165 | sylib 196 |
. . 3
 
    Word

                  ..^                
          |
167 | 6 | adantr 465 |
. . . . . 6
 
     Word
                 ..^                
            |
168 | 11 | adantr 465 |
. . . . . 6
 
     Word
                 ..^                
            |
169 | | breq1 4404 |
. . . . . . . 8
 
           |
170 | 169 | cbvrabv 3077 |
. . . . . . 7
      
      |
171 | 2, 170 | eqtri 2483 |
. . . . . 6
       |
172 | | fveq2 5800 |
. . . . . . . . . . 11
           |
173 | 172 | breq1d 4411 |
. . . . . . . . . 10
     
         
                 |
174 | 173 | cbvrabv 3077 |
. . . . . . . . 9

       
               
        |
175 | | id 22 |
. . . . . . . . . . . 12
   |
176 | | oveq1 6208 |
. . . . . . . . . . . 12
 
     
       |
177 | 175, 176 | oveq12d 6219 |
. . . . . . . . . . 11
              
        |
178 | 177 | breq2d 4413 |
. . . . . . . . . 10
     
         
                 |
179 | 178 | rabbidv 3070 |
. . . . . . . . 9
                     
             |
180 | 174, 179 | syl5eq 2507 |
. . . . . . . 8
 
       
               
         |
181 | 180 | cbvmptv 4492 |
. . . . . . 7
 
       
                           |
182 | 29, 181 | eqtri 2483 |
. . . . . 6
                   |
183 | | breq2 4405 |
. . . . . . . . . 10
   DProd
 DProd    |
184 | | oveq2 6209 |
. . . . . . . . . . 11
  DProd   DProd    |
185 | 184 | eqeq1d 2456 |
. . . . . . . . . 10
   DProd

 DProd     |
186 | 183, 185 | anbi12d 710 |
. . . . . . . . 9
    DProd 
DProd  
  DProd  DProd      |
187 | 186 | cbvrabv 3077 |
. . . . . . . 8
 Word   DProd

DProd     Word
  DProd  DProd     |
188 | 187 | mpteq2i 4484 |
. . . . . . 7
 SubGrp   Word
  DProd  DProd      SubGrp   Word   DProd

DProd      |
189 | 42, 188 | eqtri 2483 |
. . . . . 6
 SubGrp   Word   DProd

DProd      |
190 | | simprll 761 |
. . . . . 6
 
     Word
                 ..^                
             Word   |
191 | | simprlr 762 |
. . . . . . 7
 
     Word
                 ..^                
                         |
192 | | fveq2 5800 |
. . . . . . . . . 10
           |
193 | 192 | fveq2d 5804 |
. . . . . . . . 9
                   |
194 | 139, 193 | eleq12d 2536 |
. . . . . . . 8
             
               |
195 | 194 | cbvralv 3053 |
. . . . . . 7
 
                           |
196 | 191, 195 | sylib 196 |
. . . . . 6
 
     Word
                 ..^                
                         |
197 | | simprr 756 |
. . . . . 6
 
     Word
                 ..^                
             ..^   
                       |
198 | 8, 41, 167, 168, 28, 171, 182, 189, 190, 196, 142, 197 | ablfaclem2 16710 |
. . . . 5
 
     Word
                 ..^                
                |
199 | 198 | expr 615 |
. . . 4
 
    Word

                  ..^   
                            |
200 | 199 | exlimdv 1691 |
. . 3
 
    Word

               
   ..^                                |
201 | 166, 200 | mpd 15 |
. 2
 
    Word

                    |
202 | 137, 201 | exlimddv 1693 |
1
       |